[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Gcl-devel] Re: gcl/acl2
|
From: |
Camm Maguire |
|
Subject: |
Re: [Gcl-devel] Re: gcl/acl2 |
|
Date: |
13 Nov 2002 16:22:53 -0500 |
Greetings!
Matt Kaufmann <address@hidden> writes:
> 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"].
>
OK
> >> 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.
>
Your example below is reproduced exactly by by newly built acl2 here.
This does not affect anything after the image creation, though the
user could use it at that point should they so desire.
> 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.
>
Well, it is a bit muddled still. Basically, complier::link does two
things with its passed list -- writes a C function which will
initialize all object mentioned therein in order at one time, and
build in functionality to bypass the normal loading procedure when the
argument to load appears in this list and to call the initialization
procedure instead. One had the option of executing the user-init
function thus created, or passing 'ordinary' image build code which
will be identical to the previous behavior except for the load bypass
described above. The acl2 is taking the latter approach, largely
because I could not easily come up with a list of files to be loaded
which would both 1) contain all binary objects in the distribution, and
2) not load any object more than once without editing acl2 files. In
other words, acl2 is being built solely by the effects of the
(save-acl2 ... call you listed in your third pass, with calls to load
binaries being redirected to initialization calls.
We should know shortly if it works ---.
Take care,
> 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
>
>
--
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, 2002/11/12
- Re: [Gcl-devel] Re: gcl/acl2,
Camm Maguire <=
- 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
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/17