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

[Camm Maguire]

Greetings!

Dan Stanger <address@hidden> writes:

> There is another way of loading linked objects, which creates a relocatable 
> object, and
> then loads and relocates it.  ECL does this, and I think that code is gpl'd.
> I remember getting that working on elf systems, namely solaris, but it would 
> probably
> work on any elf system.
> Dan
> 

To my understanding, this is the same as our dlopen method, which we
must currently use on alpha, ia64, mips, mipsel, and hppa.  This
method does not play nicely with conventional usage of save-system,
which is why we need to support the alternate link procedure described
earlier.  The complexity of this task is also the main reason driving
the BFD effort, which is now somewhat on the back burner.

Take care,

> Camm Maguire wrote:
> 
> > 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