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.