Page 1 of 1

Package locking problem with old code from nqthm

Posted: Wed Aug 03, 2016 3:55 pm
by nagle
I'm trying to revive the original Boyer-Moore theorem prover, last updated in 1992. I'm using clisp on Ubuntu 14.04 LTS. Source is at ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/nqthm-1992. It almost works; there's only one small problem. I'm getting what seems to be a name clash during loading, on the name "EXECUTE".

Following directions from ftp://ftp.cs.utexas.edu/pub/boyer/nqthm ... 992/README I get the following error:

Code: Select all

 (load-nqthm)
;; Loading file /home/john/projects/nqthm/nqthm-1992/sloop.fas ...
...
;; Loading file /home/john/projects/nqthm/nqthm-1992/code-e-m.fas ...
** - Continuable Error
DEFUN/DEFMACRO(EXECUTE): #<PACKAGE EXT> is locked
If you continue (by typing 'continue'): Ignore the lock and proceed
The following restarts are also available:
SKIP           :R1      skip 675 683 (DEFUN EXECUTE (PROCESS CL HIST ...) ...)-25
RETRY          :R2      retry 675 683 (DEFUN EXECUTE (PROCESS CL HIST ...) ...)-25
STOP           :R3      stop loading file /home/john/projects/nqthm/nqthm-1992/code-e-m.fas
ABORT          :R4      Abort main loop
Break 1 [6]> 
This seems to indicate that there's an attempt to redefine the function EXECUTE in package EXT, and because that package is locked, this is an error. But the source code in ftp://ftp.cs.utexas.edu/pub/boyer/nqthm ... e-e-m.lisp starts with

(IN-PACKAGE "USER")

so there should not be a name clash with package EXT. I think.

If I just type "continue", everything works, but I'd like to fix this properly.

I used to write a lot of LISP, but it's been years.