質問

I would like to understand nqthm-1992 code, this is an archaic theorem prover.

I use ECL as a lisp interpreter and was advised to use the slime package for figuring out common lisp definitions and explanations. It does good on common lisp declarations but fails on nqthm declarations. How can I configure it so that it finds all the declarations if I load events.lisp of nqthm into my emacs buffer?

update: upon advice I reconfigured emacs-slime to use sbcl. Trying to look up the definition for ITERATE it gave the following message:

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") 

How can I make this work?

役に立ちましたか?

解決

It looks a lot like SLIME can't find the code you want because it's looking in the wrong package: the error that you show is SBCL saying "I looked in :cl-user and couldn't find anything called ITERATE".

When you say "Trying to look up the definition for ITERATE", I guess you mean you typed M-. on something like (iterate ...) in a buffer. The problem is that SLIME and Emacs don't know that you mean the one defined in nqthm.lisp. I just downloaded a copy of nqthm and it looks reasonably archaic, but it looks like it defines the iterate macro in the USER package. You can check this by typing (apropos "ITERATE") at the repl. In SBCL, you'll see a couple of SBCL-specific symbols but (assuming you've successfully loaded nqthm.lisp, you should also see something like USER:ITERATE.

From your question, I assume you're reasonably new to lisp, so I won't go into technical details about packages. If you just want to be able to type stuff in a buffer and have Emacs and SLIME do the right thing to use the nqthm stuff, I think you should be able to put

(in-package "USER")

at the top of your buffer and be done with it. If you want the repl to work too, either copy and paste that string into it or use C-c M-p in the repl's buffer.

他のヒント

My final answer contains some obvious things for the experienced lisp and emacs/slime user, but these were not trivial for me:

  • I had to set the current directory to the nqthm root dir:

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

  • I had to add the nqthm load code into the top:

    (load "nqthm.lisp") (in-package "USER") (load-nqthm) (boot-strap nqthm)

  • Then selecting the above code and using M-x slime-eval-region the system bootstraps nqthm and the M-. finds the definition of the sought identifier as expected.

Now comes the interesting part: if I load the above modified file upon startup and tell slime C-c C-k to compile it, it gives me the following error messages:

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.

Could anybody explain this? Is there a semantic difference between evaluating and compiling?

ライセンス: CC-BY-SA帰属
所属していません StackOverflow
scroll top