[Bug-openmcl] OpenMCL 0.14.1-pl1 breaks ACL 2.7

[Gregory Wright]

Hi Gary,

Thank you for the explanation. I've found a place to patch one of 
ACL2's Makefiles
to fix the package issue. I'll send the patch to the ACL2 maintainers.

The regressions are about half working now. However, I've found a new 
problem.
(I said at the start that the regression tests are good at stressing 
the system!)
The regressions all run, except when they have to include another file 
using the
'include-book' macro. (In ACL2, a 'book' is a bunch of theorems 
expressed in the
functional subset of lisp that is ACL2's language.)

The trouble is simple: under 0.13.7, when the makefile was processing 
the directory

	$(TOP)/books/arithmetic

and invoked

	(include-book "../cowles/acl2-crg" :load-compiled-file nil)

it searched for the file $(TOP)/book/cowles/acl2-crg.lisp and found it. 
Under
0.14.1-pl1, I get error messages saying that the file

	$(TOP)/books/arithmetic/cowles/acl2-crg.lisp

aren't found. And indeed they are not, since it looks as if the '..' 
part of the
path has been ignored.

FWIW, here's the include-book macro (from acl2-2.7/axioms.lisp). Maybe 
something
obviously dangerouos is being done.


(defparameter *connected-book-directory* nil)

(defmacro include-book (user-book-name
                         &key
                         (load-compiled-file ':warn)
                         uncertified-okp
                         defaxioms-okp
                         skip-proofs-okp
                         doc)
   (declare (ignore uncertified-okp defaxioms-okp skip-proofs-okp doc))
   `(mv-let (full-book-name directory-name short-book-name)
            (parse-book-name
             (cond (*connected-book-directory* 
*connected-book-directory*)
                   (t (f-get-global 'connected-book-directory
                                    *the-live-state*)))
             ',user-book-name
             ".lisp"
             (os *the-live-state*))
            (declare (ignore short-book-name))
            (cond
             ((assoc-equal full-book-name
                           (global-val 'include-book-alist
                                       (w *the-live-state*)))
              t)
             (t
              (let ((*connected-book-directory* directory-name)
                    (os-full-book-name
                     (pathname-unix-to-os full-book-name
                                          *the-live-state*)))
                (prog1
                    (or (load-compiled-file-if-more-recent
                         (cons 'include-book ',user-book-name)
                         ',load-compiled-file
                         full-book-name
                         os-full-book-name)
                        (load os-full-book-name))
                  (proclaim-file os-full-book-name)))))))

; Include-book is the only event that is sensitive to
; *connected-book-directory*.  The variable is virtually always to have 
the
; value of (@ connected-book-directory).  The 
*connected-book-directory* is
; always nil at the top of the system.  This means we should grab the 
value in
; the state, which is generally "" but may be odd if the user assigned 
to it.
; Thereafter (in recursive include-books) it is bound to the same value 
that
; include-book sets connected-book-directory.


Having thought about this a bit while writing, this looks like another 
case of
state being explicitly wired into the image file, and not being 
propagated to the
thread that actually does the work. Does that sound right?

Thanks for the help!

Best Wishes,
Greg



On Feb 26, 2004, at 2:30 PM, Gary Byers wrote:

>
> The different behavior between 0.13.x and 0.14.x has to do both with
> how threads work in general and with how special variables are bound
> and referenced (as well as with how SAVE-APPLICATION works.)
>
> In 0.13.x, the initial thread (the one created by the OS) ran the
> initial REPL, having first processed --eval and --load and other
> command-line args.  The value of special variables like *PACKAGE* in
> that thread is just their global value (the thread typically hasn't 
> done
> something like
>
>   (let* ((*package ...))
>    ...)
>
> so there's no dynamic binding of *PACKAGE* in effect in the initial
> thread; assignments to *PACKAGE* will just affect the static, global
> value.  A change to that static, global value persists across
> SAVE-APPLICATION.
>
> In 0.14.x, the initial thread typically creates a listener thread to
> do command-line processing and run the REPL.  The initial thread then
> spends most of the rest of its life asleep, waking up every now and
> then to perform periodic "housekeeping" tasks (forcing output from
> terminal streams, checking for external process I/O, etc.).  The
> listener thread does:
>
>  (let* ((*package* *package*))
>    ...
>
> on startup, so any assignments to *PACKAGE* in that thread affect the
> process-specific binding -only-.  That's a good thing (we don't want
> changes in *PACKAGE* in thread A to affect the value of *PACKAGE* in
> thread B), but it explains why changing the package in a listener
> thread before SAVE-APPLICATION doesn't have the effect that it used to.
>
> There -are- crufty, low-level ways of getting at the static/global
> value of a special variable even if there are intervening dynamic
> bindings, but if you can arrange to ensure that your image establishes
> the package itself (rather than relying on SAVE-APPLICATION to do so)
> it sounds like it'd be more robust.
>