[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Gcl-devel] address@hidden: Re: gcl/acl2]
|
From: |
Camm Maguire |
|
Subject: |
Re: [Gcl-devel] address@hidden: Re: gcl/acl2] |
|
Date: |
10 Nov 2002 23:56:51 -0500 |
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] address@hidden: Re: gcl/acl2], Matt Kaufmann, 2002/11/03
- Re: [Gcl-devel] address@hidden: Re: gcl/acl2],
Camm Maguire <=
- Re: [Gcl-devel] address@hidden: Re: gcl/acl2], Mike Thomas, 2002/11/14
- 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