[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Gcl-devel] Re: gcl/acl2
|
From: |
Matt Kaufmann |
|
Subject: |
Re: [Gcl-devel] Re: gcl/acl2 |
|
Date: |
Tue, 12 Nov 2002 10:51:19 -0600 (CST) |
Hi --
>> 1) Matt you referred to objects with the name "..linear.." -- I can't
>> find these.
Right -- those are in ACL2 Version 2.7, which we will probably release
tomorrow. A pre-release is still available at
ftp://ftp.cs.utexas.edu:/pub/moore/acl2/v2-7/acl2.tar.gz [cf. the email I sent
7 Nov 2002 05:16:43, Subject "apparent GCL 2.5.0 bug on Redhat 7.3"].
>> 1) In the new GCL version, loading a binary object first checks a
>> compiled-in list to see if the object has already been linked into the
>> image via ld, in which case it foregoes the load process and merely
>> runs the initialization sequence in the modules' 'data vector'.
This won't get in the way of redefinition, right? Often ACL2 users will define
a function, compile, "undo" the definition (which leads to a call of
fmakunbound), and then redefine and recompile. A little example is below, in
case you want to try this.
ACL2 !>(defun foo (x) (cons x x))
Since FOO is non-recursive, its admission is trivial. We observe that
the type of FOO is described by the theorem (CONSP (FOO X)). We used
primitive type reasoning.
Summary
Form: ( DEFUN FOO ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FOO
ACL2 !>(comp 'foo)
Compiling gazonk0.lsp.
End of Pass 1.
End of Pass 2.
OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
Finished compiling gazonk0.lsp.
Loading gazonk0.o
start address -T 906cee0 Finished loading gazonk0.o
Compiling gazonk0.lsp.
End of Pass 1.
End of Pass 2.
OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
Finished compiling gazonk0.lsp.
Loading gazonk0.o
start address -T 94a5720 Finished loading gazonk0.o
FOO
ACL2 !>(foo 3)
(3 . 3)
ACL2 !>:u
0:x(EXIT-BOOT-STRAP-MODE)
ACL2 !>(defun foo (x) (1+ x))
Since FOO is non-recursive, its admission is trivial. We observe that
the type of FOO is described by the theorem (ACL2-NUMBERP (FOO X)).
We used primitive type reasoning.
Summary
Form: ( DEFUN FOO ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
FOO
ACL2 !>(foo 3)
4
ACL2 !>(comp 'foo)
Compiling gazonk0.lsp.
End of Pass 1.
End of Pass 2.
OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
Finished compiling gazonk0.lsp.
Loading gazonk0.o
start address -T 94a5660 Finished loading gazonk0.o
Compiling gazonk0.lsp.
End of Pass 1.
End of Pass 2.
OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
Finished compiling gazonk0.lsp.
Loading gazonk0.o
start address -T 94a5dc0 Finished loading gazonk0.o
FOO
ACL2 !>(foo 3)
4
ACL2 !>
>> The problem here is that all binary objects must appear in
>> this list if the load override is to keep them out of the lisp
>> core, but on the other hand acl2 does not explicitly load
>> acl2-fns.o nor TMP1.o as separate user steps. Rather these
>> are loaded by other files. So if we include these other files
>> in a sequence that is to be executed via user-init, they would
>> be processed twice, with consequences uncertain to me at
>> least. So currently acl2 is not even calling user-init, but is
>> rather relying on the 'post' code listed at the bottom of the
>> form to initialize the objects in the list as they would be
>> loaded in the normal procedure.
I'm a little surprised that you can specify proof-checker-b.lisp without
preceding it with proof-checker-pkg.lisp, since the latter defines the
"ACL2-PC" package and the former refers to it, e.g.:
(defmacro query-on-exit (&optional (val 'toggle))
`(set-query-val 'acl2-pc::exit ',val state))
Perhaps that means I don't yet understand the initialization approach you're
using.
Thanks --
-- Matt
Cc: address@hidden, address@hidden, address@hidden
From: Camm Maguire <address@hidden>
Date: 10 Nov 2002 00:06:46 -0500
Greetings! I'm happy to report progress on this front!
Executive summary -- I have a working gcl/acl2 build sequence using
GCL's 'alternate link' procedure, which should clear up (at least the
bulk of) the remaining gcl/acl2 portability issues on the Debian
architectures.
As of right now, the Debian acl2 package builds successfully
everywhere, but fails to correctly save its image on the architectures
using dlopen for relocations, as well as two of those using BFD. The
build *and save* succeeds, and the binary passes all tests, on i386,
s390, arm and sparc.
The dlopen issues are obvious and well known, and are the reason for
the BFD effort in the first place. On ppc and m68k, the current build
procedure produces an executable which will occasionally fail to flush
object code from the data cache, (where it does reside as the objects
are in the lisp core in the data section of the binary when using
BFD). What this means is that we overlooked the need to do a cache
flush not only when the object is first loaded and relocated, which we
do now, but also either when the data pages are garbage collected, or
even when compiled functions therein are called. Some solution of
this nature should be straightforward, though the best option is not
yet clear. I have not yet implemented this.
Even when the above is fixed, we still need a solution for the dlopen
machines, at least until we find time to tackle bfd there. So with
Matt's guidance, the following sequence is working for me, which
produces a binary that has been successfully tested on i386 and
alpha(!). I'm reasonably confident that this will add mips, mipsel,
ia64, and hppa too.
To minimize edits to acl2 files, I've made a few modifications to GCL
which should handle this alternate build procedure transparently.
1) In the new GCL version, loading a binary object first checks a
compiled-in list to see if the object has already been linked into the
image via ld, in which case it foregoes the load process and merely
runs the initialization sequence in the modules' 'data vector'.
2) Further, as acl2 modules require access to the compiler directly,
and therefore need to be initialized after system-init is called, I've
taken the user-init call out of system-init and provided a separate
lisp handle for it. user-init can either be called to load and
initialize all user files at once, or can be ignored by relying on the
system 'load' function to do the initialization at the normal time in
the conventional build sequence.
3) Lastly, I've provided the following variables in the compiler
package to allow setting things like system-p without changing user
code:
*default-system-p*
*default-c-file*
*default-h-file*
*default-data-file*
So the sequence looks like this:
1) mv init.lsp init.lsp.ori
2) echo (setq compiler::*default-system-p* t) >foo.lsp
3) cat init.lsp.ori >>foo.lsp
4) echo '(load "foo.lsp")(in-package "acl2")(compile-acl2)' | gcl
5) echo '(load "foo.lsp")(in-package "acl2")(load-acl2)
(initialize-acl2 (quote include-book) *acl2-pass-2-files* t t)' | gcl
6) echo '(compiler::link (list
"acl2-fns.o"
"axioms.o"
"basis.o"
"translate.o"
"type-set-a.o"
"type-set-b.o"
"rewrite.o"
"simplify.o"
"bdd.o"
"other-processes.o"
"induct.o"
"history-management.o"
"prove.o"
"defuns.o"
"proof-checker-a.o"
"defthm.o"
"other-events.o"
"ld.o"
"proof-checker-b.o"
"tutorial.o"
"interface-raw.o"
"TMP1.o")
"saved_acl2"
"(load \"foo.lsp\")(in-package \"acl2\")(save-acl2
(quote (initialize-acl2 (quote include-book)
*acl2-pass-2-files* t))
\"saved_acl2\")" )' | gcl
A few comments:
1) Matt you referred to objects with the name "..linear.." -- I can't
find these.
2) The .lsp packages (e.g. proof-checker-package.lsp, etc.) are
omitted from the list above, but could be included. There is
currently a double use for this list, a) they specify a
sequence of files/objects that will be loaded by user-init,
and b) the 'binary' members with a .o extension are put into
the load override list. We should clear up the syntax at some
point, and suggestions are welcome here.
The problem here is that all binary objects must appear in
this list if the load override is to keep them out of the lisp
core, but on the other hand acl2 does not explicitly load
acl2-fns.o nor TMP1.o as separate user steps. Rather these
are loaded by other files. So if we include these other files
in a sequence that is to be executed via user-init, they would
be processed twice, with consequences uncertain to me at
least. So currently acl2 is not even calling user-init, but is
rather relying on the 'post' code listed at the bottom of the
form to initialize the objects in the list as they would be
loaded in the normal procedure.
It sure would be nice to either a) get BFD working everywhere and
forego these more complicated steps, or b) come up with a way to
simplify and generalize the above, perhaps by even automating it
completely. One idea is to "record" all user input, make a list of
the binaries loaded, and redirect save-system to a call to
compiler::link like the above. Might not be too hard actually.
Take care,
Matt Kaufmann <address@hidden> writes:
> 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 citizens." --
Baha'u'llah
> >
> >
>
> --
> Camm Maguire address@hidden
>
==========================================================================
> "The earth is but one country, and mankind its citizens." --
Baha'u'llah
>
>
> _______________________________________________
> Gcl-devel mailing list
> address@hidden
> http://mail.gnu.org/mailman/listinfo/gcl-devel
>
>
--
Camm Maguire address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
- Re: [Gcl-devel] gcl/acl2, (continued)
- [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/01
- [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/01
- [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/02
- [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/02
- [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/03
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/10
- Re: [Gcl-devel] Re: gcl/acl2,
Matt Kaufmann <=
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/13
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/14
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/14
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/12
- Message not available
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/14
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/15
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/15
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/17
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/17
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/17