0

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

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

更新：根据建议，我将 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")

我怎样才能使这项工作？

4

2 回答 2

2

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

当您说“尝试查找 ITERATE 的定义”时，我猜您的意思是您输入M-.了类似(iterate ...)缓冲区的内容。问题是 SLIME 和 Emacs 不知道你的意思是在nqthm.lisp. 我刚刚下载了 nqthm 的副本，它看起来相当陈旧，但看起来它定义了USER包中的 iterate 宏。(apropos "ITERATE")您可以通过在 repl 中键入来检查这一点。在 SBCL 中，您会看到一些特定于 SBCL 的符号，但是（假设您已成功加载nqthm.lisp，您还应该看到类似USER:ITERATE.

根据您的问题，我假设您对 lisp 相当陌生，因此我不会详细介绍有关软件包的技术细节。如果您只想能够在缓冲区中输入内容并让 Emacs 和 SLIME 做正确的事情来使用 nqthm 内容，我认为您应该能够将

(in-package "USER")

在缓冲区的顶部并完成它。如果您希望 repl 也可以工作，请将该字符串复制并粘贴到其中，或者在 repl 的缓冲区中使用 Cc Mp。

于 2014-05-04T17:24:22.983 回答
1

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

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

    (需要'asdf) (uiop/os:chdir "/path/to/nqthm")

  • 我不得不将 nqthm 加载代码添加到顶部：

    （加载“nqthm.lisp”）（包内“USER”）（加载-nqthm）（引导nqthm）

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

现在到了有趣的部分：如果我在启动时加载上述修改过的文件并告诉 slimeC-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.

有人可以解释一下吗？评估和编译之间是否存在语义差异？

于 2014-05-29T14:25:49.730 回答