Re: [Gcl-devel] Re: gcl/acl2

[Matt Kaufmann]

Thanks for the update.  Regarding those two issues:

>> 1) The books/workshops directory needs to exist if make clean-books is to
>>    avoid an infinite recursion, terminated only by make's internal
>>    fork limit.

I believe that this has been fixed in the latest ACL2.  Last night we updated
/u/www/users/moore/acl2/v2-7/ and the corresponding ftp site
/stage/ftp/pub/moore/acl2/v2-7/.  We are doing final tests now, and if all goes
as expected then we will modify /u/www/users/moore/acl2/index.html to point to
/u/www/users/moore/acl2/v2-7/.

So, I wonder if you'd be willing to update what you have done so that it works
with Version 2.7 of ACL2.  (Version 2.6 is about a year old now and we have
made many improvements.)  It may be that the only change you'll need to make is
to add in those two "linear" files:

    "axioms"
    "basis"
    "translate"
    "type-set-a"
    "linear-a"
    "type-set-b"
    "linear-b"
    "non-linear"
    ....

>> 2) One of the books in support has an @ in its name, and this will not
>>    compile cleanly when using :system-p t.

It would be awkward to make a change here at this late date (though we could
perhaps do so for the next release, which might be a year from now).  But isn't
your approach to avoid using systemp in the saved image?

Thanks --
-- Matt
   Cc: address@hidden, address@hidden, address@hidden
   From: Camm Maguire <address@hidden>
   Date: 14 Nov 2002 12:52:48 -0500

   Greetings!  Just a quick note as to the status of Debian gcl/acl2 --
   it appears as if the package build and now passes the short tests on
   all 11 architectures.  There are a few issues remaining with some of
   the autobuilders, but I've verified that the build works as a normal
   user on the machines in question.  The next iteration will include
   expanding the files included as per Matt's prior email, turning off
   *default-system-p* in the final image to avoid the necessity of having
   GCL's cmpinclude.h installed when certifying books, and running the
   full test as part of the package build.  I'll try to summarize the
   results when that is completed.

   A few issues with acl2 have surfaced, though minor:

   1) The books/workshops directory needs to exist if make clean-books is to
      avoid an infinite recursion, terminated only by make's internal
      fork limit.

   2) One of the books in support has an @ in its name, and this will not
      compile cleanly when using :system-p t.

   Here is the relevant part of debian/rules:

   =============================================================================
   init.lsp.ori: 
           [ -e $@ ] || mv init.lsp $@

   foo.lsp: init.lsp.ori
           echo '(setq compiler::*default-system-p* t)' >$@
           cat $< >> $@

   BINARIES:=acl2-fns.o axioms.o basis.o translate.o type-set-a.o type-set-b.o 
rewrite.o simplify.o \
             bdd.o other-processes.o induct.o history-management.o prove.o 
defuns.o proof-checker-a.o\
             defthm.o other-events.o ld.o proof-checker-b.o tutorial.o 
interface-raw.o TMP1.o
   BIN:=$(patsubst %,"%",$(BINARIES))

   INIT:=(initialize-acl2 (quote include-book) *acl2-pass-2-files* t t)
   POST:=(load \"foo.lsp\")\
         (in-package \"acl2\")\
         (save-acl2 (quote (initialize-acl2 (quote include-book) 
*acl2-pass-2-files* t)) \"saved_acl2\"))

   nsaved_acl2: foo.lsp
           echo '(load "foo.lsp")(in-package "acl2")(compile-acl2)' | gcl
           echo '(load "foo.lsp")(in-package "acl2")(load-acl2)$(INIT)' | gcl
           echo '(compiler::link (list $(BIN)) "$@" "$(POST)" "" nil)' |gcl

   saved_acl2: nsaved_acl2
           ln -snf $< $@

   build: build-stamp
   build-stamp: saved_acl2
           dh_testdir

   #    $(MAKE)

           touch build-stamp
   =============================================================================


   Take care,

   -- 
   Camm Maguire                                         address@hidden
   ==========================================================================
   "The earth is but one country, and mankind its citizens."  --  Baha'u'llah