gcl-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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


From: Camm Maguire
Subject: Re: [Gcl-devel] Re: gcl/acl2
Date: 10 Nov 2002 00:06:46 -0500

Greetings!  I'm happy to report progress on this front!

Executive summary -- I have a working gcl/acl2 build sequence using
GCL's 'alternate link' procedure, which should clear up (at least the
bulk of)  the remaining gcl/acl2 portability issues on the Debian
architectures.  

As of right now, the Debian acl2 package builds successfully
everywhere, but fails to correctly save its image on the architectures
using dlopen for relocations, as well as two of those using BFD.  The
build *and save* succeeds, and the binary passes all tests, on i386,
s390, arm and sparc.

The dlopen issues are obvious and well known, and are the reason for
the BFD effort in the first place.  On ppc and m68k, the current build
procedure produces an executable which will occasionally fail to flush
object code from the data cache, (where it does reside as the objects
are in the lisp core in the data section of the binary when using
BFD).  What this means is that we overlooked the need to do a cache
flush not only when the object is first loaded and relocated, which we
do now, but also either when the data pages are garbage collected, or
even when compiled functions therein are called.  Some solution of
this nature should be straightforward, though the best option is not
yet clear.  I have not yet implemented this.

Even when the above is fixed, we still need a solution for the dlopen
machines, at least until we find time to tackle bfd there.  So with
Matt's guidance, the following sequence is working for me, which
produces a binary that has been successfully tested on i386 and
alpha(!).  I'm reasonably confident that this will add mips, mipsel,
ia64, and hppa too.

To minimize edits to acl2 files, I've made a few modifications to GCL
which should handle this alternate build procedure transparently. 

1) In the new GCL version, loading a binary object first checks a
compiled-in list to see if the object has already been linked into the
image via ld, in which case it foregoes the load process and merely
runs the initialization sequence in the modules' 'data vector'.

2) Further, as acl2 modules require access to the compiler directly,
and therefore need to be initialized after system-init is called, I've
taken the user-init call out of system-init and provided a separate
lisp handle for it.  user-init can either be called to load and
initialize all user files at once, or can be ignored by relying on the
system 'load' function to do the initialization at the normal time in
the conventional build sequence.

3) Lastly, I've provided the following variables in the compiler
package to allow setting things like system-p without changing user
code:

*default-system-p*
*default-c-file*
*default-h-file*
*default-data-file*

So the sequence looks like this:

1) mv init.lsp init.lsp.ori
2) echo (setq compiler::*default-system-p* t) >foo.lsp
3) cat init.lsp.ori >>foo.lsp
4) echo '(load "foo.lsp")(in-package "acl2")(compile-acl2)' | gcl
5) echo '(load "foo.lsp")(in-package "acl2")(load-acl2)
        (initialize-acl2 (quote include-book) *acl2-pass-2-files* t t)' | gcl
6) echo '(compiler::link (list  
                "acl2-fns.o" 
                "axioms.o" 
                "basis.o"
                "translate.o"
                "type-set-a.o"
                "type-set-b.o"
                "rewrite.o" 
                "simplify.o"
                "bdd.o" 
                "other-processes.o" 
                "induct.o" 
                "history-management.o"
                "prove.o" 
                "defuns.o" 
                "proof-checker-a.o" 
                "defthm.o" 
                "other-events.o"
                "ld.o" 
                "proof-checker-b.o" 
                "tutorial.o" 
                "interface-raw.o" 
                "TMP1.o")
                "saved_acl2" 
                "(load \"foo.lsp\")(in-package \"acl2\")(save-acl2
                        (quote (initialize-acl2 (quote include-book) 
*acl2-pass-2-files* t))
                        \"saved_acl2\")" )' | gcl

A few comments:
1) Matt you referred to objects with the name "..linear.." -- I can't
        find these.

2) The .lsp packages (e.g. proof-checker-package.lsp, etc.) are
        omitted from the list above, but could be included. There is
        currently a double use for this list, a) they specify a
        sequence of files/objects that will be loaded by user-init,
        and b) the 'binary' members with a .o extension are put into
        the load override list.  We should clear up the syntax at some
        point, and suggestions are welcome here.  

        The problem here is that all binary objects must appear in
        this list if the load override is to keep them out of the lisp
        core, but on the other hand acl2 does not explicitly load
        acl2-fns.o nor TMP1.o as separate user steps.  Rather these
        are loaded by other files.  So if we include these other files
        in a sequence that is to be executed via user-init, they would
        be processed twice, with consequences uncertain to me at
        least. So currently acl2 is not even calling user-init, but is
        rather relying on the 'post' code listed at the bottom of the
        form to initialize the objects in the list as they would be
        loaded in the normal procedure.

It sure would be nice to either a) get BFD working everywhere and
forego these more complicated steps, or b) come up with a way to
simplify and generalize the above, perhaps by even automating it
completely.  One idea is to "record" all user input, make a list of
the binaries loaded, and redirect save-system to a call to
compiler::link like the above.  Might not be too hard actually.

Take care,

Matt Kaufmann <address@hidden> writes:

> 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
> 
> 
> _______________________________________________
> 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




reply via email to

[Prev in Thread] Current Thread [Next in Thread]