RE: [Gcl-devel] Re: possible GCL/Windows compiler bug

[Mike Thomas]

Hi Matt.

The short story so far is that with two different builds of GCL 2.6.5 I've
failed to reproduce the bug.  I hope to try out the gcc version you referred
to earlier, later on.

Details and some questions below.

| It doesn't surprise me that you can't get this bug to occur with ACL2 2.8,
| since the bug goes away with something as simple as loading the file
| gazonk520.o for a compilation done during the ACL2 build, or compiling the
| function in question with compile-file instead of compile.
|
| You can get the ACL2 2.9 sources from
| http://www.cs.utexas.edu/users/moore/acl2/; either click on "Obtaining and
| Installing Version 2.9" or else, if you already know how to install (just
| extract and type "make", actually), go straight to
| ftp://ftp.cs.utexas.edu:/pub/moore/acl2/v2-9/acl2.tar.gz.

Got it thanks.

I can't reproduce the bug with my current GCL 2.6.5 (debug
mode)/gcc/binutils setup, which supports the idea that the cause lies with
GCL rather than ACL 2.9.

Trying again with GCL 2.6.5 (not debug) built with gcc 3.3.1 (as distributed
with the standard Windows GCL 2.6.5 distribution packages) I got a strange
error partway through the build:

================================================================
 FIND-REWRITING-EQUIVALENCE
[GC for 82 STRING pages..(T=3).GC finished]
[GC for 82 STRING pages..(T=2).GC finished]
[GC for 82 STRING pages..(T=4).GC finished]
[GC for 82 STRING pages..(T=3).GC finished]
Compiling gazonk0.lsp.
End of Pass 1.
End of Pass 2.
[GC for 82 STRING pages..(T=3).GC finished]
OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
Finished compiling gazonk0.lsp.

Error: Cannot delete the file #p"gazonk0.h".
Fast links are on: do (si::use-fast-links nil) for debugging
Error signalled by UNLESS.
Broken at COND.  Type :H for Help.
ACL2>>
Sorry, execution of top-level forms is disabled inside breaks.
Execute :enable-eval T if you want such evaluation enabled.
NIL
================================================================

but restarting "make" seems to have gone around that problem.  Your bug
failed to manifest.

I'll rebuild gcl and ACL2 with the same gcc you used next.

Just to double check, all I have to do to reproduce this crash should be to
start saved_acl2.exe in the acl2-sources directory and at the prompt type
the following lines:

   (f-put-global 'safe-mode t state)
   :q
   (ACL2_*1*_ACL2::MATCH-CLAUSE 'DCL '(& . &) '(T))

As a matter of interest, as you and Jared are building GCL on one machine
and using it on another, are you sure that your respective versions of
gcc/binutils/libraries all match up?

I'm also curious about why you chose not to use the distributed GCL CLTL1
bundle at http://ftp.gnu.org/gnu/gcl/binaries/stable/ .  Was it deficient in
some way?  Perhaps you could try building ACL2 with that bundle and see what
happens.

As a side note if it's not too late for your impending release, "make clean"
doesn't remove the executable or sh script.

Cheers

Mike Thomas