[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Gcl-devel] Re: gcl/acl2
|
From: |
Matt Kaufmann |
|
Subject: |
[Gcl-devel] Re: gcl/acl2 |
|
Date: |
Sun, 3 Nov 2002 10:34:53 -0600 (CST) |
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] gcl/acl2, Camm Maguire, 2002/11/01
- Re: [Gcl-devel] gcl/acl2, C Y, 2002/11/01
- [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/01
- [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/01
- [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/02
- [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/02
- [Gcl-devel] Re: gcl/acl2,
Matt Kaufmann <=
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/10
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/12
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/13
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/14
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/14
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/12
- Message not available
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/14
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/15
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/15
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/17