[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: |
Mon, 18 Nov 2002 11:51:11 +1000 |
Hi all.
> One of us (J Moore) has recently built a more recent version of ACL2 on
WIndows
> 2000 without incident, so perhaps the problem won't be easy to reproduce.
Unfortunately it occurs here too. As you have described, the GCL garbage
collector goes into an "infinite" loop trying to allocate 28 fixnum pages.
The ensuing stack overflow sends my just-in-time debugger into an infinite
loop. I'll try and get closer to the problem as the week progresses.
Cheers
Mike Thomas.
>
> We expect to release a new version soon. A pre-release is at
> ftp://ftp.cs.utexas.edu:/pub/moore/acl2/v2-7/acl2.tar.gz (we hope this
will
> become the actual release in a few days), with home page at
> www.cs.utexas.edu/usres/moore/acl2/v2-7/.
>
> Thanks --
> -- Matt
> Reply-To: "Mike Thomas" <address@hidden>
> From: "Mike Thomas" <address@hidden>
> Cc: <address@hidden>, <address@hidden>, <address@hidden>,
> "Billinghurst, David \(CRTS\)" <address@hidden>
> Date: Thu, 14 Nov 2002 15:29:32 +1000
> Content-Type: text/plain;
> charset="iso-8859-1"
> X-Priority: 3
> X-MSMail-Priority: Normal
> X-Mimeole: Produced By Microsoft MimeOLE V6.00.2600.0000
>
> 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
itizens." --
> 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
> >
>