[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Gcl-devel] address@hidden: Re: gcl/acl2]
|
From: |
Mike Thomas |
|
Subject: |
Re: [Gcl-devel] address@hidden: Re: gcl/acl2] |
|
Date: |
Thu, 14 Nov 2002 15:29:32 +1000 |
Hi there.
Sorry about the late reply. Where do I find the source code for ACL2?
I won't be able to look at this problem until next week unfortunately.
Cheers
Mike Thomas.
----- Original Message -----
From: "Camm Maguire" <address@hidden>
To: "Matt Kaufmann" <address@hidden>
Cc: <address@hidden>; <address@hidden>; <address@hidden>; "Mike
Thomas" <address@hidden>; "Billinghurst, David (CRTS)"
<address@hidden>
Sent: Monday, November 11, 2002 2:56 PM
Subject: Re: [Gcl-devel] address@hidden: Re: gcl/acl2]
> Greetings, and thanks again for your report! Our windows and Mingw
> experts are Mike Thomas and David Billinghurst. I'm cc'ing them, as I
> unfortunately do not have access to such a box on which to diagnose
> your failure.
>
> Would either of you have a chance to try to reproduce this, and figure
> out what is going on? If you can pinpoint in a gdb backtrace, that
> would be helpful too.
>
> Take care,
>
> Matt Kaufmann <address@hidden> writes:
>
> > P.S. I've thought of something else possibly relevant since sending the
email
> > below. When the second pass of initialization calls the function
> > initialize-acl2, initialize-acl2 causes file TMP1.o (which was created
during
> > the first pass) to be loaded. So perhaps initialize-acl2 needs a flag
that
> > avoids that load, the idea being that TMP1.o is included among the files
in the
> > first argument to compiler::link. What do you think?
> >
> > On another topic, I tried to build ACL2 on GCL/Windows yesterday using
the cvs
> > GCL distribution at
ftp://ftp.gnu.org/gnu/gcl/cvs/gcl-cvs-20021014-mingw32.zip.
> > It worked! BUT -- during the first pass of initialization, GCL died
while
> > doing a FIXNUM gc, while compiling TMP1.lisp. I was able to start up
GCL again
> > and (compile-file "TMP1.lisp"), which got me around the problem. Below
is an
> > edited transcript.
> >
> > C:\matt\acl2\v2-6>c:\gcl\gcl-cvs-20021014-mingw32\gclm\bin\my-gclm.bat
> > GCL (GNU Common Lisp) Version(2.5.0) Mon Oct 14 10:50:03 EAST 2002
> > Licensed under GNU Library General Public License
> > Contains Enhancements by W. Schelter
> > Loading init.lsp
> > Loading acl2-init.lisp
> > Loading acl2.lisp
> > Loading acl2-fns.lisp
> > Finished loading acl2-fns.lisp
> > Compiling acl2-fns.lisp.
> > End of Pass 1.
> >
> > ;; Note: Tail-recursive call of GET-TYPE-FROM-DCLS was replaced by
iteration.
> > ;; Note: Tail-recursive call of COLLECT-TYPES was replaced by
iteration.
> > ;; Note: Tail-recursive call of REV1@ was replaced by iteration.
> > ;; Note: Tail-recursive call of ACL2-READ-CHARACTER-STRING was
replaced by iteration.
> > End of Pass 2.
> > OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0,
Speed=3
> > Finished compiling acl2-fns.lisp.
> > Loading acl2-fns.o
> > start address -T 10253000 Finished loading acl2-fns.o
> > Finished loading acl2.lisp
> > Finished loading acl2-init.lisp
> > Loading enable-eval.lisp
> > Disabling evaluation inside breaks.
> > Finished loading enable-eval.lisp
> > Finished loading init.lsp
> >
> > >(in-package "ACL2")
> >
> > #<"ACL2" package>
> >
> > ACL2>(load-acl2)
> > [GC for 50 RELOCATABLE-BLOCKS pages..(T=24).GC finished]
> >
> > Loading axioms.o
> > [GC for 6 SFUN pages..(T=8).GC finished]
> > [GC for 6 SFUN pages..(T=8).GC finished]
> > start address -T 1027e000 Finished loading axioms.o
> >
> > << ... output omitted ... >>
> >
> > Loading defpkgs.lisp
> > [GC for 250 CONS pages..(T=16).GC finished]
> > Finished loading defpkgs.lisp
> > "ACL2"
> >
> > ACL2>(initialize-acl2 (quote include-book) *acl2-pass-2-files* t t)
> >
> > << ... output omitted ... >>
> >
> > RESIZE-LIST
> > :REDUNDANT
> >
> > Finished loading
> > '((IN-PACKAGE "ACL2")
> > (DEFCONST *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*
> > '(&ALLOW-OTHER-KEYS *PRINT-MISER-WIDTH*
> > &AUX *PRINT-PPRINT-DISPATCH*
> > &BODY *PRINT-PRETTY* &ENVIRONMENT ...))
> > (DEFCONST *ACL2-VERSION* "ACL2 Version 2.6")
> > (DEFCONST
> > *ACL2-FILES*
> > '("axioms" "basis" "translate" "type-set-a"
> > "type-set-b" "rewrite" "simplify" ...)
> > "*acl2-files* is the list of all the files necessary to build
> > ACL2 from scratch.")
> > (DEFCONST *COMMON-LISP-SPECIALS-AND-CONSTANTS*
> > '(* ** *** *BREAK-ON-SIGNALS*
> > *COMPILE-FILE-PATHNAME*
> > *COMPILE-FILE-TRUENAME*
> > *COMPILE-PRINT* ...))
> > (DEFLABEL PROGRAMMING)
> > (DEFLABEL MISCELLANEOUS)
> > ...).
> >
> >
> > ACL2 loading '((COMP-FN :EXEC STATE)).
> > [GC for 108 STRING pages..(T=2648).GC finished]
> > [GC for 108 STRING pages..(T=644664).GC finished]
> > [GC for 260 RELOCATABLE-BLOCKS pages..(T=152).GC finished]
> > [GC for 108 STRING pages..(T=1480).GC finished]
> > [GC for 108 STRING pages..(T=1016).GC finished]
> > [GC for 260 RELOCATABLE-BLOCKS pages..(T=40).GC finished]
> > [GC for 108 STRING pages..(T=1456).GC finished]
> > [GC for 260 RELOCATABLE-BLOCKS pages..(T=1712).GC finished]
> > Compiling C:/matt/acl2/v2-6/TMP1.lisp.
> > [GC for 260 RELOCATABLE-BLOCKS pages..(T=1648).GC finished]
> > [GC for 270 RELOCATABLE-BLOCKS pages..(T=644496).GC finished]
> > [GC for 280 RELOCATABLE-BLOCKS pages..(T=646216).GC finished]
> > [GC for 290 RELOCATABLE-BLOCKS pages..(T=1398192).GC finished]
> > [GC for 300 RELOCATABLE-BLOCKS pages..(T=1760216).GC finished]
> > [GC for 310 RELOCATABLE-BLOCKS pages..(T=2340912).GC finished]
> > [GC for 320 RELOCATABLE-BLOCKS pages..(T=2442008).GC finished]
> > [GC for 330 RELOCATABLE-BLOCKS pages..(T=56).GC finished]
> > [GC for 340 RELOCATABLE-BLOCKS pages..(T=2568).GC finished]
> > [GC for 350 RELOCATABLE-BLOCKS pages..(T=536).GC finished]
> > End of Pass 1.
> > [GC for 360 RELOCATABLE-BLOCKS pages..(T=2416).GC finished]
> > [GC for 28 FIXNUM pages..(T=-69632).GC finished]
> > [GC for 28 FIXNUM pages..[GC for 28 FIXNUM pages..[GC for 28 FIXNUM
pages..
> >
> > and then 8103 more occurrences of "FIXNUM pages", all saying:
> >
> > GC for 28 FIXNUM pages
> >
> > and finally ending by shooting me back to the shell:
> >
> > [GC for 28 FIXNUM pages..[GC for 28 FIXNUM pages..
> > C:\matt\acl2\v2-6>
> >
> > Thanks --
> > -- Matt
> > ------- Start of forwarded message -------
> > Date: 3 Nov 2002 10:34:53 -0600
> > From: Matt Kaufmann <address@hidden>
> > To: address@hidden
> > CC: address@hidden, address@hidden, address@hidden
> > In-reply-to: <address@hidden> (message from Camm
Maguire
> > on 02 Nov 2002 14:47:46 -0500)
> > Subject: Re: gcl/acl2
> >
> > Hi --
> >
> > Thanks for the quick reply. First, I'll address your question about
arguments
> > to compiler::link for ACL2. Then I'll address the rest of your email.
> > Finally, I'll make a comment about the upcoming ACL2 release.
> >
> > Below I'll answer your compiler::link question under the assumption that
you
> > can create an installation procedure that takes 3 steps, where an image
is only
> > saved in the third step. Then I'll discuss that assumption.
> >
> > Just a bit of background first: Currently, if one wants to build ACL2
without
> > just executing "make", one goes through the following steps. In each
case
> > below, loading init.lsp causes the loading and compiling of some other
files.
> >
> > load init.lsp
> > load acl2r.lisp
> > load acl2-init.lisp
> > load acl2.lisp
> > load acl2-fns.lisp
> > compile-file acl2-fns.lisp
> > load acl2-fns.o
> > load "enable-eval.lisp
> >
> > Here, then, are the three steps currently taken, where gcl is started
fresh for
> > each step. These are adapted from "Building an Executable Image on a
Non-Unix
> > System" in installation.html. I have commented out (load "init.lsp")
because
> > that is done by GCL automatically.
> >
> > COMPILATION:
> >
> > ;; (load "init.lsp") ; done automatically
> > (in-package "ACL2")
> > ;; Compile source files, in the order shown in
> > ;; (acl2::defconst acl2::*acl2-files* ...), from axioms.lisp, other
than
> > ;; defpkgs.lisp and proof-checker-pkg.lisp:
> > (compile-acl2)
> >
> > INITIALIZATION, FIRST PASS. Basically, we load in the compiled files
produced
> > above, in the same order, and then we run a function that does quite a
lot of
> > work, especially taking the ACL2 source files as input, to define some
> > additional functions and extend property lists.
> >
> > ;; (load "init.lsp") ; done automatically
> > (in-package "ACL2")
> > ;; Load compiled source files, in the order shown in
> > ;; (acl2::defconst acl2::*acl2-files* ...), from axioms.lisp:
> > (load-acl2)
> > ;; ACL2 now processes its own source files.
> > (initialize-acl2 (quote include-book) *acl2-pass-2-files* t t)
> >
> > INITIALIZATION, SECOND PASS, including image save. The reason for the
second
> > pass is that there is some compilation of functions newly defined during
the
> > first pass -- in the second pass we use (si::allocate-growth type 1 10
50 2) to
> > build a reasonably compact image.
> >
> > ;; (load "init.lsp") ; done automatically
> > (in-package "ACL2")
> > (save-acl2 (quote (initialize-acl2 (quote include-book)
*acl2-pass-2-files* t))
> > "saved_acl2")
> >
> > Let us suppose that a file debian-build.lsp has been created with the
> > in-package and save-acl2 forms just above, along with a redefinition of
> > function save-acl2-in-akcl (from file acl2-init.lsp) that comments out
the form
> > (si::save-system sysout-name) at the end. Instead of a redefinition,
Perhaps I
> > should add an optional argument to save-acl2 saying not to perform that
> > save-system, in which case the form would be
> >
> > (save-acl2 (quote (initialize-acl2 (quote include-book)
*acl2-pass-2-files* t))
> > "saved_acl2"
> > t)
> >
> > I've just made that change for the next release. But I have not yet
modified
> > compile-acl2 to take an optional argument to control whether :system-p t
should
> > be passed into compile-file.
> >
> > Anyhow, perhaps the answer to your question is as follows. BUT: This
assumes
> > that the "COMPILATION" and "INITIALIZATION, FIRST PASS" steps above have
> > already been done. I comment further on this below
> >
> > (compiler::link (list
> > "axioms.o"
> > "basis.o"
> > "translate.o"
> > "type-set-a.o"
> > "linear-a.o"
> > "type-set-b.o"
> > "linear-b.o"
> > "non-linear.o"
> > "rewrite.o"
> > "simplify.o"
> > "bdd.o"
> > "other-processes.o"
> > "induct.o"
> > "history-management.o"
> > "prove.o"
> > "defuns.o"
> > "proof-checker-pkg.lisp"
> > "proof-checker-a.o"
> > "defthm.o"
> > "other-events.o"
> > "ld.o"
> > "proof-checker-b.o"
> > "tutorial.o"
> > "interface-raw.o"
> > "defpkgs.lisp"
> > )
> > "nsaved_acl2"
> > "(load \"debian-build.lsp\")" )
> >
> > Alternatively, it may be possible to do everything in a single pass,
which
> > however would result in a larger image. It would probably be better to
do all
> > three passes as described above: Is there a way that your Debian
installation
> > procedure could take three steps, where an image is saved only on the
third
> > step?
> >
> > ======================================================================
> >
> > Now I'll address the rest of your email.
> >
> > >> OK, in Debian systems, site-wide emacs initialization code is kept in
> > >> /etc/emacs/site-start.d. Here is what the package has there now:
> > >> ....
> > >> I can run M-x start-proof-tree immediately on emacs startup, (but not
> > >> M-x proof-tree). Is this correct? M-x run-acl2 works too -- is
there
> > >> anything else which might be needed here?
> > >> .....
> > >> OK, as you can see I've stuck these in the site-wide startup file.
> > >> the problem was that I could not byte compile these files, which
> > >> Debian emacs expects to be able to do. (I could try to work around
> > >> this if you think it would be better.) Will everything work if these
> > >> are in the site-wide startup file?
> >
> > That's probably fine. It does seems preferable to me to leave the file
> > structure unchanged, just for uniformity's sake, in which case
> > /etc/emacs/site-start.d would only have:
> >
> > (setq load-path (nconc load-path (list (concat "/usr/share/"
> > (symbol-name
debian-emacs-flavor)
> > "/site-lisp/acl2"))))
> >
> > (autoload 'run-acl2
> > "top-start-inferior-acl2"
> > "Open communication between acl2 running in shell and prooftree." t)
> >
> > I wonder if you could just tell Debian emacs not to byte-compile
anything; is
> > byte compilation so important? Anyhow, this probably isn't a big deal,
so if
> > things seem to work then perhaps you should leave things as you have
them. If
> > someone complains then we can investigate.
> >
> > >> as were README, README.doc, README.mss,
> > >> > and README.ps.
> > >>
> > >> Thanks! Will add these. the standard place is /usr/share/doc/acl2/.
> >
> > Thanks. I should probably rename these README-mouse*; they are very
minor bits
> > of documentation.
> >
> > >> 1) Must 'books' be certified before use? I.e. will every acl2 user
> > >> basically have to do this before getting any useful work done? If
so,
> > >> perhaps I should reverse my earlier opinion and do a 'make
certify-books' as
> > >> part of the build, even if it does take time.
> >
> > Good question. We certainly intend that ACL2 users consider using the
> > distributed books, in which case it makes sense to certify them all.
However,
> > it's easy to imagine someone downloading ACL2 just to try it out a bit,
in
> > which case they don't really need the books, or they can just play with
the
> > relatively few that are certified with the certify-books-short target
that I
> > recently created for you.
> >
> > If I had to choose, I guess I'd say "make certify-books" is the way to
go. If
> > there is an easy way to provide a "quick install" option that only calls
> > "make certify-books-short", great.
> >
> > >> 2) Can I make the doc and emacs directories symbolic links to their
> > >> standard locations on a Debian system?
> >
> > That seems fine to me. I should add that the emacs/ directory (as
opposed to
> > interface/emacs/) is kind of peripheral/optional, as suggested by the
README
> > there. So maybe it would be better to leave it in place.
> >
> > ======================================================================
> >
> > About the next ACL2 release:
> >
> > I believe that we will release ACL2 Version 2.7 this month, perhaps
within the
> > next week or two. I'm thinking of putting a link in the installation
> > instructions to our "What's new" page (currently
> > http://www.cs.utexas.edu/users/moore/acl2/v2-6/new.html, but v2-6 will
become
> > v2-7) for information about Debian packages. The idea would be to let
you know
> > when we've made the release (or, you could join the ACL2 mailing list if
you
> > like, by going to
> > http://www.cs.utexas.edu/users/moore/acl2/admin/forms/email.html).
Then, if
> > you decide to make Debian package for ACL2 2.7 (which I think would be
great),
> > we'll put an appropriate link on the above new.html page when you tell
us
> > you're ready.
> >
> > Does that make sense?
> >
> > Thanks --
> > - -- Matt
> > Cc: address@hidden, address@hidden, address@hidden
> > From: Camm Maguire <address@hidden>
> > Date: 02 Nov 2002 14:47:46 -0500
> >
> > Greetings, and thank so much for checking this out!
> >
> > Before I comment on your reply below, another issue has arisen with
> > which I would greatly appreciate your suggestions. Even though this
> > really isn't that difficult, please allow me to describe this in a
bit
> > of detail for the purpose of clarity.
> >
> >
============================================================================
=
> > Dr. Schelter had designed GCL to link object files in basically two
> > ways, one by loading the .o into the lisp core, and the other to open
> > it via dlopen as a shared library. Only the former method supports
> > saving the system image via save-system, i.e. when using dlopen, one
> > won't find the shared objects in the right places when executing a
> > saved image made with save-system. And unfortunately as of right
now,
> > we can use the former method only on about half of the Debian
> > architectures, though we hope to extend this support universally in
> > the future.
> >
> > To deal with this, Dr. Schelter designed an alternate method of
making
> > saved system images when the former loading procedure was not
> > available. It basically consists of 1) first compiling all object
> > files with 'compile-file', passing the keyword ':system-p t' in each
> > case, 2) linking the .o files with the gcl object files via the
system
> > linker, 3) initializing the objects in the same order as they
> > would have been loaded when using the former method, and 4) executing
> > save-system. In addition to being universally portable, this method
> > should have a slight performance advantage, as the .o files are not
in
> > the lisp core (and therefore do not take up pages needing garbage
> > collection), but are permanently linked in the text section of the
> > executable itself.
> >
> > GCL has since implemented a way to automate this somewhat -- the
> > 'link' function. Maxima cvs supports this, and it is the default
> > method in which the maxima binary is built and tested on all 11
Debian
> > architectures. 'link' takes two required arguments, and two optional
> > arguments. The first argument is an ordered list of files which
would
> > normally be loaded into a running image, either .lisp or .o. The
> > second argument is a string naming the saved image to produce. The
> > optional arguments are a string containing any lisp code which needs
> > to be run after loading, and a string listing any extra system
> > libraries which might be required.
> >
> > For example, after maxima compiles all its .o files, here is the link
> > command used to make the final executable (this is produced via
> > defsystem, not explicitly typed in!):
> >
> > (compiler::link (list
> > "./maxima-package.lisp"
> > "./binary-gcl/sloop.o"
> > "./binary-gcl/lmdcls.o"
> > "./binary-gcl/letmac.o"
> > "./binary-gcl/kclmac.o"
> > "./binary-gcl/clmacs.o"
> > "./binary-gcl/commac.o"
> > "./binary-gcl/mormac.o"
> > "./binary-gcl/compat.o"
> > "./binary-gcl/defopt.o"
> > "./binary-gcl/defcal.o"
> > "./binary-gcl/maxmac.o"
> > "./binary-gcl/mopers.o"
> > "./binary-gcl/mforma.o"
> > "./binary-gcl/mrgmac.o"
> > "./binary-gcl/procs.o"
> > "./binary-gcl/rzmac.o"
> > "./binary-gcl/strmac.o"
> > "./binary-gcl/displm.o"
> > "./binary-gcl/ratmac.o"
> > "./binary-gcl/mhayat.o"
> > "./binary-gcl/numerm.o"
> > "./binary-gcl/optimize.o"
> > "./SYS-PROCLAIM.lisp"
> > "./binary-gcl/opers.o"
> > "./binary-gcl/utils.o"
> > "./binary-gcl/sumcon.o"
> > "./binary-gcl/sublis.o"
> > "./binary-gcl/runtim.o"
> > "./binary-gcl/merror.o"
> > "./binary-gcl/mformt.o"
> > "./binary-gcl/mutils.o"
> > "./binary-gcl/outmis.o"
> > "./binary-gcl/ar.o"
> > "./binary-gcl/misc.o"
> > "./binary-gcl/comm.o"
> > "./binary-gcl/comm2.o"
> > "./binary-gcl/mlisp.o"
> > "./binary-gcl/mmacro.o"
> > "./binary-gcl/buildq.o"
> > "./binary-gcl/numerical/f2cl-package.o"
> > "./binary-gcl/numerical/slatec.o"
> > "./binary-gcl/numerical/f2cl-lib.o"
> > "./binary-gcl/numerical/slatec/fdump.o"
> > "./binary-gcl/numerical/slatec/j4save.o"
> > "./binary-gcl/numerical/slatec/xercnt.o"
> > "./binary-gcl/numerical/slatec/xerhlt.o"
> > "./binary-gcl/numerical/slatec/xgetua.o"
> > "./binary-gcl/numerical/slatec/xerprn.o"
> > "./binary-gcl/numerical/slatec/xersve.o"
> > "./binary-gcl/numerical/slatec/xermsg.o"
> > "./binary-gcl/numerical/slatec/initds.o"
> > "./binary-gcl/numerical/slatec/dcsevl.o"
> > "./binary-gcl/numerical/slatec/d9lgmc.o"
> > "./binary-gcl/numerical/slatec/dgamlm.o"
> > "./binary-gcl/numerical/slatec/dgamma.o"
> > "./binary-gcl/numerical/slatec/dgamln.o"
> > "./binary-gcl/numerical/slatec/dlngam.o"
> > "./binary-gcl/numerical/slatec/d9b0mp.o"
> > "./binary-gcl/numerical/slatec/d9b1mp.o"
> > "./binary-gcl/numerical/slatec/dbesj0.o"
> > "./binary-gcl/numerical/slatec/dbesj1.o"
> > "./binary-gcl/numerical/slatec/djairy.o"
> > "./binary-gcl/numerical/slatec/dasyjy.o"
> > "./binary-gcl/numerical/slatec/dbesj.o"
> > "./binary-gcl/numerical/slatec/dbsi0e.o"
> > "./binary-gcl/numerical/slatec/dbsi1e.o"
> > "./binary-gcl/numerical/slatec/dbesi0.o"
> > "./binary-gcl/numerical/slatec/dbesi1.o"
> > "./binary-gcl/numerical/slatec/dasyik.o"
> > "./binary-gcl/numerical/slatec/dbesi.o"
> > "./binary-gcl/numerical/slatec/zabs.o"
> > "./binary-gcl/numerical/slatec/zdiv.o"
> > "./binary-gcl/numerical/slatec/zexp.o"
> > "./binary-gcl/numerical/slatec/zmlt.o"
> > "./binary-gcl/numerical/slatec/zsqrt.o"
> > "./binary-gcl/numerical/slatec/zasyi.o"
> > "./binary-gcl/numerical/slatec/zuchk.o"
> > "./binary-gcl/numerical/slatec/zlog.o"
> > "./binary-gcl/numerical/slatec/zunik.o"
> > "./binary-gcl/numerical/slatec/zunhj.o"
> > "./binary-gcl/numerical/slatec/zuoik.o"
> > "./binary-gcl/numerical/slatec/zuni1.o"
> > "./binary-gcl/numerical/slatec/zkscl.o"
> > "./binary-gcl/numerical/slatec/zshch.o"
> > "./binary-gcl/numerical/slatec/zbknu.o"
> > "./binary-gcl/numerical/slatec/zmlri.o"
> > "./binary-gcl/numerical/slatec/zs1s2.o"
> > "./binary-gcl/numerical/slatec/zseri.o"
> > "./binary-gcl/numerical/slatec/zacai.o"
> > "./binary-gcl/numerical/slatec/zairy.o"
> > "./binary-gcl/numerical/slatec/zuni2.o"
> > "./binary-gcl/numerical/slatec/zbuni.o"
> > "./binary-gcl/numerical/slatec/zrati.o"
> > "./binary-gcl/numerical/slatec/zwrsk.o"
> > "./binary-gcl/numerical/slatec/zbinu.o"
> > "./binary-gcl/numerical/slatec/zbesi.o"
> > "./binary-gcl/numerical/slatec/zbesj.o"
> > "./binary-gcl/numerical/slatec/dbesy0.o"
> > "./binary-gcl/numerical/slatec/dbesy1.o"
> > "./binary-gcl/numerical/slatec/dbsynu.o"
> > "./binary-gcl/numerical/slatec/dyairy.o"
> > "./binary-gcl/numerical/slatec/dbesy.o"
> > "./binary-gcl/numerical/slatec/zacon.o"
> > "./binary-gcl/numerical/slatec/zunk1.o"
> > "./binary-gcl/numerical/slatec/zunk2.o"
> > "./binary-gcl/numerical/slatec/zbunk.o"
> > "./binary-gcl/numerical/slatec/zbesh.o"
> > "./binary-gcl/numerical/slatec/zbesy.o"
> > "./binary-gcl/numerical/slatec/dbsk0e.o"
> > "./binary-gcl/numerical/slatec/dbesk0.o"
> > "./binary-gcl/numerical/slatec/dbsk1e.o"
> > "./binary-gcl/numerical/slatec/dbesk1.o"
> > "./binary-gcl/numerical/slatec/dbsknu.o"
> > "./binary-gcl/numerical/slatec/dbesk.o"
> > "./binary-gcl/numerical/slatec/zbesk.o"
> > "./binary-gcl/numerical/slatec/d9aimp.o"
> > "./binary-gcl/numerical/slatec/daie.o"
> > "./binary-gcl/numerical/slatec/dai.o"
> > "./binary-gcl/numerical/slatec/derfc.o"
> > "./binary-gcl/numerical/slatec/derf.o"
> > "./binary-gcl/numerical/slatec/de1.o"
> > "./binary-gcl/numerical/slatec/dei.o"
> > "./binary-gcl/simp.o"
> > "./binary-gcl/float.o"
> > "./binary-gcl/csimp.o"
> > "./binary-gcl/csimp2.o"
> > "./binary-gcl/zero.o"
> > "./binary-gcl/logarc.o"
> > "./binary-gcl/rpart.o"
> > "./binary-gcl/macsys.o"
> > "./binary-gcl/mload.o"
> > "./binary-gcl/suprv1.o"
> > "./binary-gcl/dskfn.o"
> > "./binary-gcl/lesfac.o"
> > "./binary-gcl/factor.o"
> > "./binary-gcl/algfac.o"
> > "./binary-gcl/nalgfa.o"
> > "./binary-gcl/ufact.o"
> > "./binary-gcl/result.o"
> > "./binary-gcl/rat3a.o"
> > "./binary-gcl/rat3b.o"
> > "./binary-gcl/rat3d.o"
> > "./binary-gcl/rat3c.o"
> > "./binary-gcl/rat3e.o"
> > "./binary-gcl/nrat4.o"
> > "./binary-gcl/ratout.o"
> > "./binary-gcl/transm.o"
> > "./binary-gcl/transl.o"
> > "./binary-gcl/transs.o"
> > "./binary-gcl/trans1.o"
> > "./binary-gcl/trans2.o"
> > "./binary-gcl/trans3.o"
> > "./binary-gcl/trans4.o"
> > "./binary-gcl/trans5.o"
> > "./binary-gcl/transf.o"
> > "./binary-gcl/troper.o"
> > "./binary-gcl/trutil.o"
> > "./binary-gcl/trmode.o"
> > "./binary-gcl/trdata.o"
> > "./binary-gcl/trpred.o"
> > "./binary-gcl/transq.o"
> > "./binary-gcl/acall.o"
> > "./binary-gcl/fcall.o"
> > "./binary-gcl/evalw.o"
> > "./binary-gcl/trprop.o"
> > "./binary-gcl/mdefun.o"
> > "./binary-gcl/bessel.o"
> > "./binary-gcl/ellipt.o"
> > "./binary-gcl/numer.o"
> > "./binary-gcl/intpol.o"
> > "./binary-gcl/rombrg.o"
> > "./binary-gcl/nparse.o"
> > "./binary-gcl/displa.o"
> > "./binary-gcl/nforma.o"
> > "./binary-gcl/ldisp.o"
> > "./binary-gcl/grind.o"
> > "./binary-gcl/spgcd.o"
> > "./binary-gcl/ezgcd.o"
> > "./binary-gcl/option.o"
> > "./binary-gcl/macdes.o"
> > "./binary-gcl/inmis.o"
> > "./binary-gcl/db.o"
> > "./binary-gcl/compar.o"
> > "./binary-gcl/askp.o"
> > "./binary-gcl/sinint.o"
> > "./binary-gcl/sin.o"
> > "./binary-gcl/risch.o"
> > "./binary-gcl/hayat.o"
> > "./binary-gcl/defint.o"
> > "./binary-gcl/residu.o"
> > "./binary-gcl/trigi.o"
> > "./binary-gcl/trigo.o"
> > "./binary-gcl/trgred.o"
> > "./binary-gcl/specfn.o"
> > "./binary-gcl/mat.o"
> > "./binary-gcl/matrix.o"
> > "./binary-gcl/sprdet.o"
> > "./binary-gcl/newinv.o"
> > "./binary-gcl/linnew.o"
> > "./binary-gcl/newdet.o"
> > "./binary-gcl/schatc.o"
> > "./binary-gcl/matcom.o"
> > "./binary-gcl/matrun.o"
> > "./binary-gcl/nisimp.o"
> > "./binary-gcl/tlimit.o"
> > "./binary-gcl/limit.o"
> > "./binary-gcl/solve.o"
> > "./binary-gcl/psolve.o"
> > "./binary-gcl/algsys.o"
> > "./binary-gcl/polyrz.o"
> > "./binary-gcl/cpoly.o"
> > "./binary-gcl/mtrace.o"
> > "./binary-gcl/mdebug.o"
> > "./binary-gcl/scs.o"
> > "./binary-gcl/asum.o"
> > "./binary-gcl/fortra.o"
> > "./binary-gcl/optim.o"
> > "./binary-gcl/marray.o"
> > "./binary-gcl/mdot.o"
> > "./binary-gcl/irinte.o"
> > "./binary-gcl/series.o"
> > "./binary-gcl/numth.o"
> > "./binary-gcl/laplac.o"
> > "./binary-gcl/pade.o"
> > "./binary-gcl/homog.o"
> > "./binary-gcl/combin.o"
> > "./binary-gcl/mstuff.o"
> > "./binary-gcl/ratpoi.o"
> > "./binary-gcl/pois2.o"
> > "./binary-gcl/pois3.o"
> > "./binary-gcl/nusum.o"
> > "./binary-gcl/desoln.o"
> > "./binary-gcl/elim.o"
> > "./binary-gcl/trgsmp.o"
> > "./binary-gcl/ode2.o"
> > "./binary-gcl/invert.o"
> > "./binary-gcl/hypgeo.o"
> > "./binary-gcl/hyp.o"
> > "./binary-gcl/todd-coxeter.o"
> > "./binary-gcl/mactex.o"
> > "./binary-gcl/plot.o"
> > "./autol.lisp"
> > "./max_ext.lisp"
> > "./autoconf-variables.lisp"
> > "./init-cl.lisp")
> > "saved_maxima"
> > "(provide \"maxima\")" )
> >
> >
> > What I would greatly appreciate is some help in producing the
> > analogous command for acl2, which is bound to be much simpler, I'd
> > think. I've been looking at complie-acl2 and load-acl2, and have
made
> > a start, but am getting various dependency errors, as acl2-fns, for
> > example, appears to be being loaded multiple times.
> >
> > Any suggestions most appreciated!
> >
============================================================================
=
> >
> >
> >
> > Matt Kaufmann <address@hidden> writes:
> >
> > > Hi, and thank YOU again for all your great GCL work --
> > >
> > > As you requested, I have taken a look at the Debian ACL2 package
that you
> > > constructed. Thanks for your work! Here are some comments.
> > >
> > > I downloaded
http://ftp.debian.org/debian/pool/main/a/acl2/acl2_2.6-6_i386.deb
> > > to my RedHat 7.3 laptop and then followed the instructions in
> > > http://ftp.gnu.org/gnu/gcl/cvs/HOWTO-UNPACK-DEBS. (By the way, I
had to become
> > > root to do that; perhaps you could mention that in
HOWTO-UNPACK-DEBS.) I then
> >
> > Thanks for the tip! Will do.
> >
> > > issued the command "acl2" at the shell and it seemed to work
perfectly! In
> > > order to run ACL2 proof trees (meta-x proof-tree) in emacs, though,
I needed to
> > > execute the following forms in emacs (which I have added to my
.emacs file).
> > >
> > > (defvar *acl2-interface-dir* "/usr/share/emacs/site-lisp/acl2/")
> > >
> > > (autoload 'start-proof-tree
> > > (concat *acl2-interface-dir* "top-start-shell-acl2")
> > > "Enable proof tree logging in a prooftree buffer."
> > > t)
> > >
> >
> > OK, in Debian systems, site-wide emacs initialization code is kept in
> > /etc/emacs/site-start.d. Here is what the package has there now:
> >
============================================================================
=
> > ;; -*-emacs-lisp-*-
> > ;;
> > ;; Emacs startup file for the Debian GNU/Linux acl2 package
> > ;;
> > ;; Originally contributed by Nils Naumann <address@hidden>
> > ;; Modified by Dirk Eddelbuettel <address@hidden>
> > ;; Adapted for dh-make by Jim Van Zandt <address@hidden>
> >
> > ;; The acl2 package follows the Debian/GNU Linux 'emacsen' policy and
> > ;; byte-compiles its elisp files for each 'emacs flavor' (emacs19,
> > ;; xemacs19, emacs20, xemacs20...). The compiled code is then
> > ;; installed in a subdirectory of the respective site-lisp directory.
> > ;; We have to add this to the load-path:
> > (setq load-path (nconc load-path (list (concat "/usr/share/"
> > (symbol-name debian-emacs-flavor)
> > "/site-lisp/acl2"))))
> >
> >
> > ;; Load the emacs interface for acl2 and start it running in an
> > ;; inferior-acl2 buffer.
> >
> > ;; May 13 94 Kaufmann & MKSmith
> > ;; Sep 25 94 MKSmith
> >
> > ;; THIS GOES IN THE USER'S .emacs FILE,
> > ;; after loadpath is set to include this dir.
> >
> > ; BEGIN INSERT after this line
> > ;
> > ; (autoload 'run-acl2
> > ; "top-start-inferior-acl2"
> > ; "Open communication between acl2 running in shell and prooftree."
t)
> > ;
> > ; END INSERT before this line
> >
> > (require 'acl2-interface) ;loads everything else
> >
> > (defun initialize-mfm-buffer-variables ()
> > (setq *mfm-buffer* inferior-acl2-buffer))
> >
> > (setq inferior-acl2-mode-hook
> > (extend-hook inferior-acl2-mode-hook
'initialize-mfm-buffer-variables))
> >
> > (defun load-inferior-acl2 ()
> > (interactive)
> > (run-acl2 inferior-acl2-program))
> >
> >
> > ;; Load the emacs interface for acl2 when it is running in a
> > ;; shell buffer in shell-mode.
> > ;; May 13 94 Kaufmann & MKSmith
> >
> > ;; ASSUMPTION: load path contains the directory this file resides in.
> >
> > (defvar *acl2-user-map-interface*
> > '((prooftree-mode-map keys)))
> >
> > (require 'key-interface)
> >
> > ;; (defvar *selected-mode-map*)
> > (defvar inferior-acl2-buffer)
> >
> > (defun initialize-mfm-buffer-variables ()
> > (setq *mfm-buffer* "*shell*")
> > ;; (setq *selected-mode-map* shell-mode-map)
> > (setq inferior-acl2-buffer *mfm-buffer*))
> >
> > (defvar shell-mode-hook nil)
> > (setq shell-mode-hook
> > (extend-hook shell-mode-hook 'initialize-mfm-buffer-variables))
> >
> > (defun start-shell-acl2 ()
> > (interactive)
> > (require 'shell)
> > ;; Looks redundant.
> > ;;(setq shell-mode-hook
> > ;;(extend-hook 'initialize-mfm-buffer-variables shell-mode-hook))
> > (shell))
> >
> >
> > (autoload 'run-acl2
> > "top-start-inferior-acl2"
> > "Open communication between acl2 running in shell and prooftree."
t)
> >
============================================================================
=
> >
> > I can run M-x start-proof-tree immediately on emacs startup, (but not
> > M-x proof-tree). Is this correct? M-x run-acl2 works too -- is
there
> > anything else which might be needed here?
> >
> >
> > > But then they worked great; thanks.
> > >
> > > Also, a file was missing in /usr/share/emacs/site-lisp/acl2/:
> > > load-shell-acl2.el. (That directory comes from the ACL2
interface/emacs/
> > > directory.) I went ahead and copied it over manually (as root).
File
> > > load-inferior-acl2.el was also missing,
> >
> > OK, as you can see I've stuck these in the site-wide startup file.
> > the problem was that I could not byte compile these files, which
> > Debian emacs expects to be able to do. (I could try to work around
> > this if you think it would be better.) Will everything work if these
> > are in the site-wide startup file?
> >
> > as were README, README.doc, README.mss,
> > > and README.ps.
> >
> > Thanks! Will add these. the standard place is /usr/share/doc/acl2/.
> >
> >
> > >
> > > More importantly, several ACL2 directories (and their
subdirectories) were
> > > missing from the extraction. In order of importance (most to
least), they are
> > > as follows, where acl2-sources is the top-level ACL2 source
directory:
> > >
> > > acl2-sources/ [users need to be able to browse the sources]
> > > acl2-sources/books/ [these are like "libraries" -- pre-proved
theorems etc.]
> > > acl2-sources/doc/ [HTML, Emacs info, and Postscript
documentation]
> > > acl2-sources/emacs/ [Some emacs utilities]
> > > acl2-sources/interface/infix/
> > >
> >
> > Thanks for pointing this out! Two questions:
> > 1) Must 'books' be certified before use? I.e. will every acl2 user
> > basically have to do this before getting any useful work done? If
so,
> > perhaps I should reverse my earlier opinion and do a 'make
certify-books' as
> > part of the build, even if it does take time.
> >
> > 2) Can I make the doc and emacs directories symbolic links to their
> > standard locations on a Debian system?
> >
> > Thanks again,
> >
> >
> >
> >
> >
> > > I don't know enough about traditional file organization to suggest
where these
> > > should go in a Debian package. Our method has been to allow ACL2
users to
> > > download ACL2 and put the acl2-sources directory anywhere they
want,
> > > maintaining the structure that we provide under acl2-sources/.
Under that
> > > method, one of the first things to do is to run the "make
certify-books"
> > > command from acl2-sources/, in order to "certify" the many .lisp
files under
> > > acl2-sources/books/ (i.e., run them through ACL2). This process
compiles files
> > > and, more importantly, writes out .cert files that have absolute
pathnames. I
> > > don't know how that would fit into a Debian installation process.
> > >
> > > >> > By the way, I'm hoping that we will release the next version
(2.7) of ACL2
> > > >> > later this month. (It's been a year since we released ACL2
2.6.)
> > > >> >
> > > >>
> > > >> Great! Any surprises?
> > >
> > > I don't think so. The set of files has changed slightly, and of
course the
> > > contents of files have changed somewhat, but the basic structure is
the same.
> > >
> > > Thanks --
> > > -- Matt
> > > Cc: address@hidden, address@hidden
> > > From: Camm Maguire <address@hidden>
> > > Date: 01 Nov 2002 19:41:24 -0500
> > >
> > > Greetings, and thanks for your reply!
> > >
> > > Matt Kaufmann <address@hidden> writes:
> > >
> > > > Hi, Camm --
> > > >
> > > > That's really great that GCL is in such good shape!
> > > >
> > > > I've added two targets to the top-level ACL2 Makefile for you,
so that you can
> > > > easily run short tests. In both cases, the exit status should
be 0 if the test
> > > > succeeded and non-zero otherwise. Two files need to be
edited: Makefile and
> > > > books/Makefile. At the end below are editing instructions,
but if you'd rather
> > > > I just email you the entire files, let me know.
> > > >
> > >
> > > Many thanks! I've added these. BTW, Debian's autobuilders
expect
> > > *some* output from the build at least every 15 minutes. For
> > > potentially long running tests with redirected standard output,
I
> > > usually use this trick:
> > >
> > > $(MAKE) short-test-aux > short-test.log 2> short-test.log &
j=$$! ; \
> > > tail -f --pid=$$j --retry short-test.log & wait $$j
> > >
> > >
> > > > >> Lastly, I'd be most appreciate if you or some other
knowledgeable acl2
> > > > >> user could look at the package and comment as to whether
everything is
> > > > >> available and in the right place.
> > > >
> > > > Sure. Please point me to where it is. I don't know anything
about Debian
> > > > packages but I'll try to find someone who does. Or would it
suffice to follow
> > > > the instructions at
http://ftp.gnu.org/gnu/gcl/cvs/HOWTO-UNPACK-DEBS and build
> > > > it on my Redhat 7.3 laptop?
> > > >
> > >
> > > http://ftp.debian.org/debian/pool/main/a/acl2/
> > >
> > > > By the way, I'm hoping that we will release the next version
(2.7) of ACL2
> > > > later this month. (It's been a year since we released ACL2
2.6.)
> > > >
> > >
> > > Great! Any surprises?
> > >
> > > > Finally, regarding your emacs point:
> > > >
> > > > >> Also, a Debian user has already brought up a minor issue in
the emacs
> > > > >> lisp interface regarding differences between xemacs and GNU
emacs. He
> > > > >> is suggesting the following:
> > > > >>
> > > > >>
============================================================================
=
> > > > >> (defun acl2-shared-lisp-mode-map ()
> > > > >> "Return the shared lisp-mode-map, independent of Emacs
version."
> > > > >> (if (boundp 'shared-lisp-mode-map)
> > > > >> shared-lisp-mode-map
> > > > >> lisp-mode-shared-map))
> > > > >>
> > > > >> and replacing references to shared-lisp-mode-map with
> > > > >> (acl2-shared-lisp-mode-map) ought to work. (I actually
even tested
> > > > >> the approach with GNU Emacs 20, GNU Emacs 21, and XEmacs 21
this
> > > > >> time; I get byte-compiler warnings, but that's all. ;-))
> > > > >>
============================================================================
=
> > > > >>
> > > > >> Do you have any thoughts here?
> > > >
> > > > Thanks very much. I guess you're referring to directory
interface/emacs/ in
> > > > the ACL2 distribution; is that right? Your solution looks
reasonable to me.
> > > >
> > >
> > > OK, its in.
> > >
> > >
> > > Thanks again!
> > >
> > >
> > > --
> > > Camm Maguire address@hidden
> > >
==========================================================================
> > > "The earth is but one country, and mankind its citizens." --
Baha'u'llah
> > >
> > >
> >
> > --
> > Camm Maguire address@hidden
> >
==========================================================================
> > "The earth is but one country, and mankind its citizens." --
Baha'u'llah
> > ------- End of forwarded message -------
> >
> >
> > _______________________________________________
> > Gcl-devel mailing list
> > address@hidden
> > http://mail.gnu.org/mailman/listinfo/gcl-devel
> >
> >
>
> --
> Camm Maguire address@hidden
> ==========================================================================
> "The earth is but one country, and mankind its citizens." -- Baha'u'llah
>
>
> _______________________________________________
> Gcl-devel mailing list
> address@hidden
> http://mail.gnu.org/mailman/listinfo/gcl-devel
>
- [Gcl-devel] address@hidden: Re: gcl/acl2], Matt Kaufmann, 2002/11/03
- Re: [Gcl-devel] address@hidden: Re: gcl/acl2], Camm Maguire, 2002/11/10
- Re: [Gcl-devel] address@hidden: Re: gcl/acl2],
Mike Thomas <=
- Re: [Gcl-devel] address@hidden: Re: gcl/acl2], Matt Kaufmann, 2002/11/14
- Re: [Gcl-devel] address@hidden: Re: gcl/acl2], Mike Thomas, 2002/11/17
- Re: [Gcl-devel] address@hidden: Re: gcl/acl2], Mike Thomas, 2002/11/18
- Re: [Gcl-devel] address@hidden: Re: gcl/acl2], Matt Kaufmann, 2002/11/18
- Re: [Gcl-devel] address@hidden: Re: gcl/acl2], Camm Maguire, 2002/11/18
- Re: [Gcl-devel] address@hidden: Re: gcl/acl2], Camm Maguire, 2002/11/18
- Re: [Gcl-devel] address@hidden: Re: gcl/acl2], Mike Thomas, 2002/11/18