gcl-devel
[Top][All Lists]
Advanced

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

Re: [Gcl-devel] address@hidden: Re: gcl/acl2]


From: Camm Maguire
Subject: Re: [Gcl-devel] address@hidden: Re: gcl/acl2]
Date: 18 Nov 2002 23:32:44 -0500

Greetings!  Currently, all cvs binaries show up a few days after I
take a snapshot and release it as a Debian package.  This happens
automatically.  I usually make such a release after a significant
change.  Mike builds the Windows binaries whenever he feels its
appropriate.  

Take care,

Matt Kaufmann <address@hidden> writes:

> Great!  Thank you for the fix and the compliment.  (I don't see a new x86
> distribution on ftp://ftp.gnu.org/gnu/gcl/cvs/, by the way; I guess I just 
> wait
> till it shows up?)
> 
> Thanks --
> -- Matt
>    Reply-To: "Mike Thomas" <address@hidden>
>    From: "Mike Thomas" <address@hidden>
>    Cc: <address@hidden>, <address@hidden>, <address@hidden>,
>       <address@hidden>, <address@hidden>
>    Date: Tue, 19 Nov 2002 13:35:25 +1000
>    Content-Type: text/plain;
>          charset="iso-8859-1"
>    X-Priority: 3
>    X-MSMail-Priority: Normal
>    X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2600.0000
> 
>    Hi Matt et al.
> 
>    That's fixed in CVS now.
> 
>    ACL2 looks like a great piece of work, by the way.
> 
>    Cheers
> 
>    Mike Thomas
> 
>    ----- Original Message -----
>    From: "Mike Thomas" <address@hidden>
>    To: "Matt Kaufmann" <address@hidden>
>    Cc: <address@hidden>; <address@hidden>; <address@hidden>;
>    <address@hidden>; <address@hidden>
>    Sent: Monday, November 18, 2002 11:51 AM
>    Subject: Re: [Gcl-devel] address@hidden: Re: gcl/acl2]
> 
> 
>    > Hi all.
>    >
>    > > One of us (J Moore) has recently built a more recent version of ACL2 on
>    > WIndows
>    > > 2000 without incident, so perhaps the problem won't be easy to
>    reproduce.
>    >
>    > Unfortunately it occurs here too.  As you have described, the GCL garbage
>    > collector goes into an "infinite" loop trying to allocate 28 fixnum 
> pages.
>    > The ensuing stack overflow sends my just-in-time debugger into an 
> infinite
>    > loop.  I'll try and get closer to the problem as the week progresses.
>    >
>    > Cheers
>    >
>    > Mike Thomas.
>    >
>    > >
>    > > We expect to release a new version soon.  A pre-release is at
>    > > ftp://ftp.cs.utexas.edu:/pub/moore/acl2/v2-7/acl2.tar.gz (we hope this
>    > will
>    > > become the actual release in a few days), with home page at
>    > > www.cs.utexas.edu/usres/moore/acl2/v2-7/.
>    > >
>    > > Thanks --
>    > > -- Matt
>    > >    Reply-To: "Mike Thomas" <address@hidden>
>    > >    From: "Mike Thomas" <address@hidden>
>    > >    Cc: <address@hidden>, <address@hidden>,
>    <address@hidden>,
>    > >       "Billinghurst, David \(CRTS\)" <address@hidden>
>    > >    Date: Thu, 14 Nov 2002 15:29:32 +1000
>    > >    Content-Type: text/plain;
>    > >    charset="iso-8859-1"
>    > >    X-Priority: 3
>    > >    X-MSMail-Priority: Normal
>    > >    X-Mimeole: Produced By Microsoft MimeOLE V6.00.2600.0000
>    > >
>    > >    Hi there.
>    > >
>    > >    Sorry about the late reply.  Where do I find the source code for
>    ACL2?
>    > >
>    > >    I won't be able to look at this problem until next week
>    unfortunately.
>    > >
>    > >    Cheers
>    > >
>    > >    Mike Thomas.
>    > >
>    > >
>    > >    ----- Original Message -----
>    > >    From: "Camm Maguire" <address@hidden>
>    > >    To: "Matt Kaufmann" <address@hidden>
>    > >    Cc: <address@hidden>; <address@hidden>;
>    <address@hidden>;
>    > "Mike
>    > >    Thomas" <address@hidden>; "Billinghurst, David
>    (CRTS)"
>    > >    <address@hidden>
>    > >    Sent: Monday, November 11, 2002 2:56 PM
>    > >    Subject: Re: [Gcl-devel] address@hidden: Re: gcl/acl2]
>    > >
>    > >
>    > >    > Greetings, and thanks again for your report!  Our windows and 
> Mingw
>    > >    > experts are Mike Thomas and David Billinghurst.  I'm cc'ing them,
>    as
>    > I
>    > >    > unfortunately do not have access to such a box on which to 
> diagnose
>    > >    > your failure.
>    > >    >
>    > >    > Would either of you have a chance to try to reproduce this, and
>    > figure
>    > >    > out what is going on?  If you can pinpoint in a gdb backtrace, 
> that
>    > >    > would be helpful too.
>    > >    >
>    > >    > Take care,
>    > >    >
>    > >    > Matt Kaufmann <address@hidden> writes:
>    > >    >
>    > >    > > P.S. I've thought of something else possibly relevant since
>    sending
>    > the
>    > >    email
>    > >    > > below.  When the second pass of initialization calls the 
> function
>    > >    > > initialize-acl2, initialize-acl2 causes file TMP1.o (which was
>    > created
>    > >    during
>    > >    > > the first pass) to be loaded.  So perhaps initialize-acl2 needs 
> a
>    > flag
>    > >    that
>    > >    > > avoids that load, the idea being that TMP1.o is included among
>    the
>    > files
>    > >    in the
>    > >    > > first argument to compiler::link.  What do you think?
>    > >    > >
>    > >    > > On another topic, I tried to build ACL2 on GCL/Windows yesterday
>    > using
>    > >    the cvs
>    > >    > > GCL distribution at
>    > >    ftp://ftp.gnu.org/gnu/gcl/cvs/gcl-cvs-20021014-mingw32.zip.
>    > >    > > It worked!  BUT -- during the first pass of initialization, GCL
>    > died
>    > >    while
>    > >    > > doing a FIXNUM gc, while compiling TMP1.lisp.  I was able to
>    start
>    > up
>    > >    GCL again
>    > >    > > and (compile-file "TMP1.lisp"), which got me around the problem.
>    > Below
>    > >    is an
>    > >    > > edited transcript.
>    > >    > >
>    > >    > >
>    > C:\matt\acl2\v2-6>c:\gcl\gcl-cvs-20021014-mingw32\gclm\bin\my-gclm.bat
>    > >    > >   GCL (GNU Common Lisp)  Version(2.5.0) Mon Oct 14 10:50:03 EAST
>    > 2002
>    > >    > >   Licensed under GNU Library General Public License
>    > >    > >   Contains Enhancements by W. Schelter
>    > >    > >   Loading init.lsp
>    > >    > >   Loading acl2-init.lisp
>    > >    > >   Loading acl2.lisp
>    > >    > >   Loading acl2-fns.lisp
>    > >    > >   Finished loading acl2-fns.lisp
>    > >    > >   Compiling acl2-fns.lisp.
>    > >    > >   End of Pass 1.
>    > >    > >
>    > >    > >   ;; Note: Tail-recursive call of GET-TYPE-FROM-DCLS was 
> replaced
>    > by
>    > >    iteration.
>    > >    > >   ;; Note: Tail-recursive call of COLLECT-TYPES was replaced by
>    > >    iteration.
>    > >    > >   ;; Note: Tail-recursive call of REV1@ was replaced by
>    iteration.
>    > >    > >   ;; Note: Tail-recursive call of ACL2-READ-CHARACTER-STRING was
>    > >    replaced by iteration.
>    > >    > >   End of Pass 2.
>    > >    > >   OPTIMIZE levels: Safety=0 (No runtime error checking), 
> Space=0,
>    > >    Speed=3
>    > >    > >   Finished compiling acl2-fns.lisp.
>    > >    > >   Loading acl2-fns.o
>    > >    > >   start address -T 10253000 Finished loading acl2-fns.o
>    > >    > >   Finished loading acl2.lisp
>    > >    > >   Finished loading acl2-init.lisp
>    > >    > >   Loading enable-eval.lisp
>    > >    > >   Disabling evaluation inside breaks.
>    > >    > >   Finished loading enable-eval.lisp
>    > >    > >   Finished loading init.lsp
>    > >    > >
>    > >    > >   >(in-package "ACL2")
>    > >    > >
>    > >    > >   #<"ACL2" package>
>    > >    > >
>    > >    > >   ACL2>(load-acl2)
>    > >    > >   [GC for 50 RELOCATABLE-BLOCKS pages..(T=24).GC finished]
>    > >    > >
>    > >    > >   Loading axioms.o
>    > >    > >   [GC for 6 SFUN pages..(T=8).GC finished]
>    > >    > >   [GC for 6 SFUN pages..(T=8).GC finished]
>    > >    > >   start address -T 1027e000 Finished loading axioms.o
>    > >    > >
>    > >    > > << ... output omitted ... >>
>    > >    > >
>    > >    > >   Loading defpkgs.lisp
>    > >    > >   [GC for 250 CONS pages..(T=16).GC finished]
>    > >    > >   Finished loading defpkgs.lisp
>    > >    > >   "ACL2"
>    > >    > >
>    > >    > >   ACL2>(initialize-acl2 (quote include-book) *acl2-pass-2-files*
>    t
>    > t)
>    > >    > >
>    > >    > > << ... output omitted ... >>
>    > >    > >
>    > >    > >    RESIZE-LIST
>    > >    > >    :REDUNDANT
>    > >    > >
>    > >    > >   Finished loading
>    > >    > >   '((IN-PACKAGE "ACL2")
>    > >    > >     (DEFCONST *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*
>    > >    > >       '(&ALLOW-OTHER-KEYS *PRINT-MISER-WIDTH*
>    > >    > >   &AUX *PRINT-PPRINT-DISPATCH*
>    > >    > >   &BODY *PRINT-PRETTY* &ENVIRONMENT ...))
>    > >    > >     (DEFCONST *ACL2-VERSION* "ACL2 Version 2.6")
>    > >    > >     (DEFCONST
>    > >    > >      *ACL2-FILES*
>    > >    > >      '("axioms" "basis" "translate" "type-set-a"
>    > >    > > "type-set-b" "rewrite" "simplify" ...)
>    > >    > >      "*acl2-files* is the list of all the files necessary to
>    build
>    > >    > >   ACL2 from scratch.")
>    > >    > >     (DEFCONST *COMMON-LISP-SPECIALS-AND-CONSTANTS*
>    > >    > >       '(* ** *** *BREAK-ON-SIGNALS*
>    > >    > >   *COMPILE-FILE-PATHNAME*
>    > >    > >   *COMPILE-FILE-TRUENAME*
>    > >    > >   *COMPILE-PRINT* ...))
>    > >    > >     (DEFLABEL PROGRAMMING)
>    > >    > >     (DEFLABEL MISCELLANEOUS)
>    > >    > >     ...).
>    > >    > >
>    > >    > >
>    > >    > >   ACL2 loading '((COMP-FN :EXEC STATE)).
>    > >    > >   [GC for 108 STRING pages..(T=2648).GC finished]
>    > >    > >   [GC for 108 STRING pages..(T=644664).GC finished]
>    > >    > >   [GC for 260 RELOCATABLE-BLOCKS pages..(T=152).GC finished]
>    > >    > >   [GC for 108 STRING pages..(T=1480).GC finished]
>    > >    > >   [GC for 108 STRING pages..(T=1016).GC finished]
>    > >    > >   [GC for 260 RELOCATABLE-BLOCKS pages..(T=40).GC finished]
>    > >    > >   [GC for 108 STRING pages..(T=1456).GC finished]
>    > >    > >   [GC for 260 RELOCATABLE-BLOCKS pages..(T=1712).GC finished]
>    > >    > >   Compiling C:/matt/acl2/v2-6/TMP1.lisp.
>    > >    > >   [GC for 260 RELOCATABLE-BLOCKS pages..(T=1648).GC finished]
>    > >    > >   [GC for 270 RELOCATABLE-BLOCKS pages..(T=644496).GC finished]
>    > >    > >   [GC for 280 RELOCATABLE-BLOCKS pages..(T=646216).GC finished]
>    > >    > >   [GC for 290 RELOCATABLE-BLOCKS pages..(T=1398192).GC finished]
>    > >    > >   [GC for 300 RELOCATABLE-BLOCKS pages..(T=1760216).GC finished]
>    > >    > >   [GC for 310 RELOCATABLE-BLOCKS pages..(T=2340912).GC finished]
>    > >    > >   [GC for 320 RELOCATABLE-BLOCKS pages..(T=2442008).GC finished]
>    > >    > >   [GC for 330 RELOCATABLE-BLOCKS pages..(T=56).GC finished]
>    > >    > >   [GC for 340 RELOCATABLE-BLOCKS pages..(T=2568).GC finished]
>    > >    > >   [GC for 350 RELOCATABLE-BLOCKS pages..(T=536).GC finished]
>    > >    > >   End of Pass 1.
>    > >    > >   [GC for 360 RELOCATABLE-BLOCKS pages..(T=2416).GC finished]
>    > >    > >   [GC for 28 FIXNUM pages..(T=-69632).GC finished]
>    > >    > >   [GC for 28 FIXNUM pages..[GC for 28 FIXNUM pages..[GC for 28
>    > FIXNUM
>    > >    pages..
>    > >    > >
>    > >    > > and then 8103 more occurrences of "FIXNUM pages", all saying:
>    > >    > >
>    > >    > >   GC for 28 FIXNUM pages
>    > >    > >
>    > >    > > and finally ending by shooting me back to the shell:
>    > >    > >
>    > >    > >   [GC for 28 FIXNUM pages..[GC for 28 FIXNUM pages..
>    > >    > >   C:\matt\acl2\v2-6>
>    > >    > >
>    > >    > > Thanks --
>    > >    > > -- Matt
>    > >    > > ------- Start of forwarded message -------
>    > >    > > Date: 3 Nov 2002 10:34:53 -0600
>    > >    > > From: Matt Kaufmann <address@hidden>
>    > >    > > To: address@hidden
>    > >    > > CC: address@hidden, address@hidden, address@hidden
>    > >    > > In-reply-to: <address@hidden> (message from
>    > Camm
>    > >    Maguire
>    > >    > > on 02 Nov 2002 14:47:46 -0500)
>    > >    > > Subject: Re: gcl/acl2
>    > >    > >
>    > >    > > 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
>    > itizens."  --
>    > >    Baha'u'llah
>    > >    > >    >
>    > >    > >    >
>    > >    > >
>    > >    > >    --
>    > >    > >    Camm Maguire      address@hidden
>    > >    > >
>    > >
>    > 
> ==========================================================================
>    > >    > >    "The earth is but one country, and mankind its citizens."  --
>    > >    Baha'u'llah
>    > >    > > ------- End of forwarded message -------
>    > >    > >
>    > >    > >
>    > >    > > _______________________________________________
>    > >    > > 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
>    > >    >
>    > >    >
>    > >    > _______________________________________________
>    > >    > Gcl-devel mailing list
>    > >    > address@hidden
>    > >    > http://mail.gnu.org/mailman/listinfo/gcl-devel
>    > >    >
>    > >
>    >
>    >
>    >
>    > _______________________________________________
>    > 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]