0

nqthm-1992 コードを理解したいのですが、これは古風な定理証明です。

私は ECL を Lisp インタープリターとして使用していますが、一般的な Lisp の定義と説明を理解するには、slime パッケージを使用するように勧められました。一般的な Lisp 宣言ではうまくいきますが、nqthm 宣言では失敗します。events.lispnqthm を 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

1

私の最後の回答には、経験豊富な Lisp および emacs/slime ユーザーにとって明らかなことがいくつか含まれていますが、これらは私にとっては些細なことではありませんでした。

  • 現在のディレクトリを nqthm ルート ディレクトリに設定する必要がありました。

    ('asdf が必要です) (uiop/os:chdir "/path/to/nqthm")

  • nqthm ロード コードを一番上に追加する必要がありました。

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

  • 次に、上記のコードを選択しM-x slime-eval-region、システム ブートストラップ nqthmを使用してM-.、期待どおりに検索された識別子の定義を見つけます。

ここで興味深い部分があります。起動時に上記の変更されたファイルをロードし、スライム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.

誰でもこれを説明できますか？評価とコンパイルの間に意味的な違いはありますか?

于 2014-05-29T14:25:49.730 に答える