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

[Matt Kaufmann]

Hi, Mike --

Please see reply below.

   From: "Mike Thomas" <address@hidden>
   Cc: <address@hidden>, <address@hidden>,
           "Jared Davis" <address@hidden>
   Date: Tue, 19 Oct 2004 10:59:54 +1000
   Content-Type: text/plain;
           charset="iso-8859-1"
   X-Priority: 3 (Normal)
   X-MSMail-Priority: Normal
   X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.2180
   Importance: Normal
   X-SpamAssassin-Status: No, hits=-2.6 required=5.0
   X-UTCS-Spam-Status: No, hits=-182 required=180

   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:

Hmmm, seems really odd that there's a problem deleting a temporary .h file
(produced by the compiler); I have no clue about this (it's GCL rather than
ACL2).

   ================================================================
    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.

It seems to be quite slippery.

   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))

Yes, that's right.  I doubt that it matters which directory in which you start
it.  (I'd check right now but I'm in linux and since I'm 99% sure it doesn't
seem to be worth a reboot, especially since nearly half the time that I boot in
Windows it immediately hangs!)

   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 not sure, but Jared was getting the same error as I was getting, and in his
case I believe the build and execution were all on the same machine.  I can
imagine that everything relevant is the same since Jared created an entire
mingw-based distribution (mingw tools and GCL and ACL2 executables), which is
what I downloaded from http://www.cs.utexas.edu/users/jared/acl2/ (except then
I built from the original ACL2 sources -- Jared has since put in a patch I gave
him that eliminates the problem by loading the problematic gazonk520.o file).

   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.

I don't know where Jared got the gcl.

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

Thanks.  We've already done the release (just this past Saturday), but I've
made a note to fix this.  Amazingly, I never use make clean, which is probably
why this hasn't come up.  Our make is non-standard in that it builds a new
image even if the current one is up-to-date.

   Cheers

   Mike Thomas

Thanks for your time on this --
-- Matt