------------------------------------------------------------------------------- Running Nqthm under Allegro in 2002 ... Some correspondence. J Moore has forwarded to me your query about trying to use Nqthm and Shankar's Goedel Theorem proof. > However, nqthm doesn't want to compile under Allegro Lisp on Linux x86. > It keeps finishing the compile, but then the executable won't run. There are several issues here and we can approach them independently. 1. I hardly ever use Allegro, so this was a new problem for me. Some time in the last 7 years (the last Nqthm release was in 1995), Allegro changed the way that the function DUMPLISP works. Using Google to look up documentation for DUMPLISP, I have come up with the following workaround, namely, after doing a "make", make nqthm-1992 LISP=acl rename the dumped file thus: mv saved_nqthm-1992 saved_nqthm-1992.dxl Subsequently, start that saved dxl image with the command acl -I saved_nqthm-1992.dxl 2. It is easy to use Nqthm-1992 without bothering to dump an image. Since dumping is not clearly specified in Common Lisp, (not even possible on the old Lisp machines) this is probably the long term way to go. Below is a transcript that shows how I ran the Goedel events just now under Linux under allegro (acl) without using any dumped image. I am simply following the instructions in the Installation chapter of the user's guide, the book A Computational Logic Handbook, Boyer and Moore, Academic Press, Second Edition, 1998. Let me know if you can't get either of these methods to work for you. But please, if you do, send me some transcripts of what happened for you. It is to me utterly amazing to me that the Goedel proofs still work seven years later in Allegro! Bob Boyer % acl International Allegro CL Enterprise Edition ... noise deleted ... CL-USER(1): (in-package "USER") # CL-USER(2): (load "nqthm.lisp") ; Loading /v/filer1b/v0q027/boyer/nqthm-2nd/tmp/nqthm.lisp T CL-USER(3): (compile-nqthm) ;;; Compiling file sloop.lisp ... compiler commentary deleted ... #p"ppr.fasl" NIL CL-USER(4): (exit) % acl International Allegro CL Enterprise Edition ... noise deleted ... CL-USER(1): (in-package "USER") # CL-USER(2): (load "nqthm.lisp") ; Loading /v/filer1b/v0q027/boyer/nqthm-2nd/tmp/nqthm.lisp T CL-USER(3): (load-nqthm) ; Fast loading /v/filer1b/v0q027/boyer/nqthm-2nd/tmp/sloop.fasl ; Fast loading /v/filer1b/v0q027/boyer/nqthm-2nd/tmp/basis.fasl ; Fast loading /v/filer1b/v0q027/boyer/nqthm-2nd/tmp/genfact.fasl ; Fast loading /v/filer1b/v0q027/boyer/nqthm-2nd/tmp/events.fasl ; Fast loading /v/filer1b/v0q027/boyer/nqthm-2nd/tmp/code-1-a.fasl ; Fast loading /v/filer1b/v0q027/boyer/nqthm-2nd/tmp/code-b-d.fasl ; Fast loading /v/filer1b/v0q027/boyer/nqthm-2nd/tmp/code-e-m.fasl ; Fast loading /v/filer1b/v0q027/boyer/nqthm-2nd/tmp/code-n-r.fasl ; Fast loading /v/filer1b/v0q027/boyer/nqthm-2nd/tmp/code-s-z.fasl ; Fast loading /v/filer1b/v0q027/boyer/nqthm-2nd/tmp/io.fasl ; Fast loading /v/filer1b/v0q027/boyer/nqthm-2nd/tmp/ppr.fasl T CL-USER(4): (prove-file-out "examples/shankar/goedel") ... noise deleted, and waiting about 5 minutes ... T ------------------------------------------------------------------------------- Bug report on using Nqthm in Maxima. I just did this for allegro CL 6.2, (actually, loaded it into maxima..) there is a minor glitch... in compiling, Error: Attempt to make a FUNCTION definition for the name TYPE-ERROR. This name is in the COMMON-LISP package and defining it is a violation for portable programs. The package COMMON-LISP has EXCL:PACKAGE-DEFINITION-LOCK set, which causes the system to signal this violation. [condition type: PACKAGE-LOCKED-ERROR] Restart actions (select using :continue): 0: Set the FUNCTION definition of the name TYPE-ERROR anyway. 1: retry the load of sloop 2: skip loading sloop 3: recompile h:\lisp\nqthm\nqthm-1992\sloop.lisp 4: Return to Top Level (an "abort" restart). 5: Abort entirely from this process. [changing package from "COMMON-LISP-USER" to "SLOOP"] [1c] SLOOP(5): :cont 0 ... and then it worked... Reply: I believe that the problem you hit may have something to do with Sloop being already in Maxima. Sloop, by the way, and as you probably know well, is not Boyer-Moore code. It is the version of LOOP that Schelter wrote for KCL in 1985 or so. I suspect that a later version of Sloop is distributed with the Maxima you have. I believe that a lame work-around for running Nqthm in Maxima is to execute: (SHADOW 'TYPE-ERROR "SLOOP") (SHADOW 'LOOP-FINISH "SLOOP") before trying to compile Nqthm. That's what we do in our startup file nqthm.lisp, but, alas, only if package SLOOP is not already present. But who knows what those SHADOW's might do to Maxima users. P. S. Other possible and possibly better fixes are (1) to edit the version of sloop.lisp that comes with Nqthm-1992 so that it does not define TYPE-ERROR or LOOP-FINISH by changing the names of those functions, or otherwise screw with their collision with the COMMON-LISP package, (2) to avoid compiling and loading sloop.lisp if it is already present by replacing the lines in nqthm.lisp (CF "sloop") (LF "sloop") with (if (not (fboundp 'sloop::sloop)) (CF "sloop")) (if (not (fboundp 'sloop::sloop)) (LF "sloop")) or (3) to change the definition of ITERATE in nqthm.lisp to the following, thus using the now standard Common Lisp LOOP facility instead of Sloop. (DEFMACRO ITERATE (&REST L) `(LOOP ,@ L)) When we last released Nqthm, in 1995 or so, we did not do (1) because we didn't want to touch Bill Schelter's code, (2) we wanted to use the version of Sloop we had rather than an unknown, changed, later version of Sloop, and (3) because we did not want to explore the question of which Common Lisp implementations provided a LOOP that was perfectly compatible with the Sloop we had relied upon for years.