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

[Camm Maguire]

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