[Bug-openmcl] OpenMCL 0.14.1-pl1 breaks ACL 2.7
gwright at comcast.net
Thu Feb 26 14:55:21 MST 2004
Thank you for the explanation. I've found a place to patch one of
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
(I said at the start that the regression tests are good at stressing
The regressions all run, except when they have to include another file
'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
(include-book "../cowles/acl2-crg" :load-compiled-file nil)
it searched for the file $(TOP)/book/cowles/acl2-crg.lisp and found it.
0.14.1-pl1, I get error messages saying that the file
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
obviously dangerouos is being done.
(defparameter *connected-book-directory* nil)
(defmacro include-book (user-book-name
(declare (ignore uncertified-okp defaxioms-okp skip-proofs-okp doc))
`(mv-let (full-book-name directory-name short-book-name)
(t (f-get-global 'connected-book-directory
(declare (ignore short-book-name))
(let ((*connected-book-directory* directory-name)
(cons 'include-book ',user-book-name)
; Include-book is the only event that is sensitive to
; *connected-book-directory*. The variable is virtually always to have
; value of (@ connected-book-directory). The
; always nil at the top of the system. This means we should grab the
; the state, which is generally "" but may be odd if the user assigned
; Thereafter (in recursive include-books) it is bound to the same value
; include-book sets connected-book-directory.
Having thought about this a bit while writing, this looks like another
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!
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
> 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
> 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.
More information about the Bug-openmcl