[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Gcl-devel] address@hidden: Re: gcl/acl2]
|
From: |
Mike Thomas |
|
Subject: |
Re: [Gcl-devel] address@hidden: Re: gcl/acl2] |
|
Date: |
Tue, 19 Nov 2002 13:35:25 +1000 |
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
>