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

[Camm Maguire]

Greetings!  I'm trying to augment the Debian ACL2 package as Matt had
mentioned earlier.

As I see it, the issues are broadly three:

1) emacs interface and docs
2) sources and books.
3) library modules.

Regarding 2), the issue is of course that all the files will be
installed as root, and cannot be modified by an ordinary user running
'make certify-books' in place.  One can of course download the source
package and build as an ordinary user.  Likewise, I'm planning on
running the full certify-books as part of the package build, so all
the certs and modules should be available to the package at install
time.  So perhaps this is enough, but we could go the extra step and
ship the src, and provide  a little script to copy the tree to the
user's home directory and certify the books there.  I'd appreciate
your advice here.

3) is related.  Does ACL2 respect GCL's *load-path*?  If we include
   the .o files in a single directory (as there appears to be no
   namespace conflict), can the user load or autoload as needed?  

   Separately, any package built on top of gcl can of course save
   their own system image.  On i386, ppc, arm, m68k, sparc, and s390,
   GCL is not needed to be present for this operation, whereas on
   alpha, mips, mipsel, ia64, and hppa (at present), one can only do
   this via compiler::link, in which case GCL is required to be
   installed.  In addition, in the latter case, the base ACL2 .o files
   are required.  My question then is whether this is a
   typical/important usage of ACL2, and whether the .o files and .lisp
   files needed by 'save-acl2' should be shipped together with a
   script and/or doc explaining how to do this.  This would only
   required until we get universal BFD support, which could be some
   time.

Both 2) and 3) are affected by the requirement on a compliant FSB
system to separate arch-specific binaries from shareable source
files.  Here are the standard locations:

info                           /usr/share/info
emacs                          /usr/share/emacs
emacs startup                  /etc/emacs
config                         /etc/acl2-2.6
app-specific shareable         /usr/share/acl2-2.6
app-specific binary            /usr/lib/acl2-2.6
general user executable        /usr/bin
app docs                       /usr/share/doc/acl2-2.6/....

So we could do something like this:

/usr/lib/acl2-2.6/bin/saved_acl2
/usr/lib/acl2-2.6/lib/*.o
/usr/lib/acl2-2.6/src --> /usr/share/acl2-2.6/src
/usr/lib/acl2-2.6/emacs --> /usr/share/emacs/acl2-2.6
/usr/lib/acl2-2.6/doc --> /usr/share/doc/acl2-2.6/

Comments most appreciated!

A few other points:

To minimize changes to the conventional acl2 setup, I'll try placing
the load***.el files in non-byte-compiled form in the emacs acl2
directory, and calling them from the startup script in /etc/emacs/...

Should the infix contents be compiled and included in the src (source)
and lib (binary) trees as outlined above?

Debian often splits packages of this size.  Currently, we have acl2
and acl2-doc.  Other possibilities are acl2-src, acl2-el, and
acl2-books.  Would this be helpful?

Take care,

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
> 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)
> 
> 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, as were README, README.doc, 
> README.mss,
> and README.ps.
> 
> 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/
> 
> 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
> 
> 
> _______________________________________________
> 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