[Gcl-devel] Re: gcl/acl2

[Camm Maguire]

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