遵循lisp代码库中的定义

Question

我想了解一下nqthm-1992的代码，这是一个古老的定理证明程序。

我使用ECL作为lisp解释器，并被建议使用slime包来找出常见的lisp定义和解释。它在常见的lisp声明上做得很好，但在nqthm声明上就失败了。我如何配置它，使它找到所有的声明，如果我加载events.lisp的nqthm到我的emacs缓冲区?

update:根据建议，我重新配置了emacs-slime以使用sbcl。试图查找ITERATE的定义，它给出了以下消息:

Unknown symbol: ITERATE [in #<PACKAGE "COMMON-LISP-USER">] 
   [Condition of type SIMPLE-ERROR] 
Restarts: 
 0: [*ABORT] Return to SLIME's top level. 
 1: [TERMINATE-THREAD] Terminate this thread (#<THREAD "worker" RUNNING {1004942B81}>) 
Backtrace: 
  0: (SWANK::PARSE-SYMBOL-OR-LOSE "ITERATE" #<PACKAGE "COMMON-LISP-USER">) 
  1: ((LAMBDA ())) 
  2: (SWANK::CALL-WITH-BUFFER-SYNTAX NIL #<CLOSURE (LAMBDA #) {1004948CA9}>) 
  3: (SB-INT:SIMPLE-EVAL-IN-LEXENV (SWANK:DESCRIBE-SYMBOL "ITERATE") #<NULL-LEXENV>) 
  4: (SWANK:EVAL-FOR-EMACS (SWANK:DESCRIBE-SYMBOL "ITERATE") ""USER"" 2) 
  5: ((LAMBDA ())) 
  6: (SWANK-BACKEND::CALL-WITH-BREAK-HOOK #<FUNCTION SWANK:SWANK-DEBUGGER-HOOK> #<FUNCTION (LAMBDA #) {1006D4AFF9}>) 
  7: ((FLET SWANK-BACKEND:CALL-WITH-DEBUGGER-HOOK) #<FUNCTION SWANK:SWANK-DEBUGGER-HOOK> #<FUNCTION (LAMBDA #) {1006D4AFF9}>) 
  8: ((LAMBDA ())) 
  9: ((FLET #:WITHOUT-INTERRUPTS-BODY-[BLOCK369]374)) 
 10: ((FLET SB-THREAD::WITH-MUTEX-THUNK)) 
 11: ((FLET #:WITHOUT-INTERRUPTS-BODY-[CALL-WITH-MUTEX]300)) 
 12: (SB-THREAD::CALL-WITH-MUTEX ..) 
 13: (SB-THREAD::INITIAL-THREAD-FUNCTION) 
 14: ("foreign function: #x41E240") 
 15: ("foreign function: #x416117") 

我怎样才能使它工作?

Answer 1

它看起来很像SLIME找不到你想要的代码，因为它在错误的包中查找:你显示的错误是SBCL说"我在:cl-user中查找，找不到任何名为ITERATE的东西"。

当你说"试图查找ITERATE的定义"时，我猜你的意思是你在缓冲区中输入M-.之类的(iterate ...)。问题是SLIME和Emacs不知道您指的是nqthm.lisp中定义的那个。我刚刚下载了一个nqthm的副本，它看起来相当古老，但它看起来像在USER包中定义了迭代宏。您可以通过在repl中输入(apropos "ITERATE")来检查这一点。在SBCL中，您将看到几个特定于SBCL的符号，但是(假设您已经成功加载了nqthm.lisp)您还应该看到类似USER:ITERATE的符号。

从你的问题来看，我认为你对lisp相当陌生，所以我不会深入讨论包的技术细节。如果你只是想在缓冲区中输入东西，并让Emacs和SLIME正确使用nqthm的东西，我认为你应该能够把

(in-package "USER")

放在缓冲区的顶部，然后完成它。如果您希望repl也能工作，要么复制并粘贴该字符串到其中，要么在repl的缓冲区中使用C-c M-p。

Answer 2

对于经验丰富的lisp和emacs/slime用户来说，我的最终答案包含了一些显而易见的东西，但这些对我来说并不是微不足道的:

• 我必须将当前目录设置为nqthm根目录:

  (需要asdf) (uiop/os:目录"/路径//nqthm")

• 我必须在顶部添加nqthm加载代码:

  (负载"nqthm.lisp")(于"用户")(load-nqthm)(开机nqthm)

• 然后选择上述代码并使用M-x slime-eval-region系统引导nqthm, M-.按预期找到所寻标识符的定义

现在有趣的部分来了:如果我在启动时加载上面修改过的文件，并告诉slime C-c C-k编译它，它会给我以下错误消息:

cd /home/gergoe/local/nqthm-1992/
4 compiler notes:
secd.events:29:1:
style-warning: 
Style warning:
  in file secd.events, position 748
  at (BOOT-STRAP NQTHM)
  ! Variable NQTHM was undefined. Compiler assumes it is a global.
secd.events:34:1:
style-warning: 
Style warning:
  in file secd.events, position 824
  at (ADD-SHELL LAMBDA ...)
  ! Variable LAMBDA was undefined. Compiler assumes it is a global.
style-warning: 
Style warning:
  in file secd.events, position 824
  at (ADD-SHELL LAMBDA ...)
  ! Variable LAMBDAP was undefined. Compiler assumes it is a global.
error: 
Error:
  in file secd.events, position 824
  at (ADD-SHELL LAMBDA ...)
  * (LBODY (NONE-OF) ZERO) is not a legal function name.
Compilation failed.

有人能解释一下吗?求值和编译之间有语义上的区别吗?