Следуя определениям в кодовой базе lisp

Я хотел бы понять код nqthm-1992, это архаичный доказатель теорем.

Я использую ECL в качестве интерпретатора lisp, и мне посоветовали использовать пакет slime для выяснения общих определений и объяснений lisp. Это хорошо работает с объявлениями common 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")

Как я могу заставить это работать?


lisp common-lisp slime ecl
person Gergely    schedule 01.05.2014    source источник
comment
Вы говорите о вещах, определенных DEFEVENT? В конечном счете, это макросы, если я правильно понимаю, поэтому я ожидаю, что это просто сработает. Согласно руководству, поддержка ECL в SLIME не самая лучшая. Может быть, попробовать использовать sbcl?   -  person Samuel Edwin Ward    schedule 02.05.2014
comment
@SamuelEdwinWard Я пробовал sbcl, см. выше.   -  person Gergely    schedule 02.05.2014
comment
Похоже, что iterate определено в nqthm.lisp. Вы скомпилировали и загрузили этот файл?   -  person Samuel Edwin Ward    schedule 02.05.2014
comment
@SamuelEdwinWard: я следовал инструкциям в README NQTHM (загрузить nqthm.lisp) (провозгласить '(оптимизировать (скорость 3) (безопасность 0) (пробел 0))) (ПОЛЬЗОВАТЕЛЬ в пакете) (компилировать-nqthm) (пока ). Или вы имели в виду что-то, что я должен делать при каждом запуске emacs?   -  person Gergely    schedule 29.05.2014

Ответы (2)


arrow_upward
2
arrow_downward

Очень похоже, что SLIME не может найти нужный код, потому что он ищет не в том пакете: ошибка, которую вы показываете, это SBCL, говорящая: «Я просмотрел :cl-user и не смог найти ничего под названием ITERATE».

Когда вы говорите «Попытка найти определение для ITERATE», я думаю, вы имеете в виду, что набрали M-. что-то вроде (iterate ...) в буфере. Проблема в том, что SLIME и Emacs не знают, что вы имеете в виду тот, который определен в nqthm.lisp. Я только что скачал копию nqthm, и она выглядит достаточно архаичной, но похоже, что она определяет макрос iterate в пакете USER. Вы можете проверить это, набрав (apropos "ITERATE") в ответе. В SBCL вы увидите пару символов, специфичных для SBCL, но (при условии, что вы успешно загрузили nqthm.lisp, вы также должны увидеть что-то вроде USER:ITERATE.

Судя по вашему вопросу, я предполагаю, что вы новичок в lisp, поэтому я не буду вдаваться в технические подробности о пакетах. Если вы просто хотите иметь возможность вводить что-то в буфер, а Emacs и SLIME делают правильные вещи, чтобы использовать материал nqthm, я думаю, вы должны иметь возможность поместить

(in-package "USER")

в верхней части вашего буфера и покончите с этим. Если вы хотите, чтобы реплика тоже работала, либо скопируйте и вставьте в нее эту строку, либо используйте C-c M-p в буфере реплики.

person Rupert Swarbrick    schedule 04.05.2014
comment
Предлагаемая строка изначально находится в events.lisp, поэтому нет смысла ее добавлять. - person Gergely; 08.05.2014
comment
Гергели: Я не совсем понимаю этот комментарий. Может быть, вы не поняли, что если вы (load "foo.lisp") и foo.lisp содержит (in-package :something), то текущий пакет впоследствии сбрасывается? См. документацию для load для более подробной информации. - person Rupert Swarbrick; 10.05.2014
comment
Я поставил (in-package USER) после всех вызовов загрузки и перед фактическим кодом lisp. Теперь я получаю Неизвестный символ: add-shell [in #‹PACKAGE COMMON-LISP-USER›]. Является ли этот пакет COMMON-LISP-USER таким же, как пакет USER? - person Gergely; 29.05.2014

arrow_upward
1
arrow_downward

Мой окончательный ответ содержит некоторые очевидные вещи для опытного пользователя lisp и emacs/slime, но для меня они не были тривиальными:

  • Мне пришлось установить текущий каталог в корневой каталог nqthm:

    (требуется asdf) (uiop/os:chdir "/path/to/nqthm")

  • Мне пришлось добавить код загрузки nqthm в начало:

    (загрузить "nqthm.lisp") (в пакете "ПОЛЬЗОВАТЕЛЬ") (загрузить-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.

Кто-нибудь может это объяснить? Есть ли семантическая разница между оценкой и компиляцией?

person Gergely    schedule 29.05.2014
comment
Я нашел этот вопросы и ответы о переполнении стека об оценке lisp и компиляции, но это не объяснило мне, почему эта ошибка происходит. M-x slime-eval-buffer проходит через весь файл, но, как следует из названия, это оценка. - person Gergely; 30.05.2014