gcl-devel
[Top][All Lists]
Advanced

[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: Fri, 15 Nov 2002 18:06:11 -0600 (CST)

Hi --

Comments/replies are interspersed.

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

  As I see it, the issues are broadly three:

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

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

I think your proposal will work for most users.  But some may take the option
you mention of copying the tree elsewhere (not necessarily the top of the home
directory, though).  I'll add a list of all book filenames at the end of this
email, in case that's helpful to you.

At this point, I imagine that some users will want to add their own _books_
(ACL2 input files) to the books/ directory.  That is because ACL2 does not have
a notion of a "home directory" or the like, and it is useful in a book to put a
form such as (include-book ".../other-book"), where _include-book_ is an ACL2
analogue of load, and ".../other-book" is a relative path name.  Also, some
users may want to download the workshop books (see the discussion in
http://www.cs.utexas.edu/users/moore/acl2/v2-7/installation.html#Certifying)
into a subdirectory of books; similarly for "nonstd" books.

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

No, ACL2 doesn't know anything about *load-path*.

Which .o files are you referring to?  If you mean the distributed books, it's
just luck that there is no name conflict; books in distinct directories are
allowed to have the same name.  Also, in case this fact is relevant: the ACL2
include-book command processes the .lisp file in addition to loading the .o
file.

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

Let's see if I understand the question.  I think you're saying that when
compiler::link is used, it's not enough to ship a saved image; one also needs
the .o files.  So perhaps you are asking whether users typically want to
download ACL2 without building GCL.  I don't know the answer to that question,
but I think it would be reasonable to do what's easiest and wait for someone to
complain.

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

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

  So we could do something like this:

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

I guess that would work OK.  The main concern I have is that neither J Moore
nor I know much about Debian package stuff, and we both have limited time to
spend on ACL2 -- so we have kept system-level stuff simple and pretty constant
over time.  (For example, there is no notion of uninstalling ACL2 other than
deleting it.)  If unforeseen problems arise, I'll continue to answer your
emails, but I doubt I'll be of much use other than that.  I'm torn between
gratitude that you're doing all this work to build a package, and a concern
that ACL2 is being complicated.

  Comments most appreciated!

  A few other points:

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

OK -- though as I may have pointed out, most users will not want the emacs
stuff, so it should be autoloaded or at least not always loaded.

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

I have no idea -- we haven't looked at the infix stuff in a long time.  I'd
just leave it and wait until someone complains.  (I don't mean to suggest that
I have a completely lazy attitude about ACL2!  We work really hard on the core
system.  It's just that the infix stuff is peripheral and currently of very low
priority, but not yet so irrelevant that we care to delete it.)

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

I don't know enough about packages to know what "helpful" means in this
context.  What is the value in splitting the package?

  Take care,

Thanks again for all your efforts!

-- Matt [I have included a listing of books/ below; search for +++]
  Matt Kaufmann <address@hidden> writes:

  > Hi, and thank YOU again for all your great GCL work --
  > 
  > As you requested, I have taken a look at the Debian ACL2 package that you
  > constructed.  Thanks for your work!  Here are some comments.
  > 
  > I downloaded 
http://ftp.debian.org/debian/pool/main/a/acl2/acl2_2.6-6_i386.deb
  > to my RedHat 7.3 laptop and then followed the instructions in
  > http://ftp.gnu.org/gnu/gcl/cvs/HOWTO-UNPACK-DEBS.  (By the way, I had to 
become
  > root to do that; perhaps you could mention that in HOWTO-UNPACK-DEBS.)  I 
then
  > issued the command "acl2" at the shell and it seemed to work perfectly!  In
  > order to run ACL2 proof trees (meta-x proof-tree) in emacs, though, I 
needed to
  > execute the following forms in emacs (which I have added to my .emacs file).
  > 
  > (defvar *acl2-interface-dir* "/usr/share/emacs/site-lisp/acl2/")
  > 
  > (autoload 'start-proof-tree
  >   (concat *acl2-interface-dir* "top-start-shell-acl2")
  >   "Enable proof tree logging in a prooftree buffer."
  >   t)
  > 
  > But then they worked great; thanks.
  > 
  > Also, a file was missing in /usr/share/emacs/site-lisp/acl2/:
  > load-shell-acl2.el.  (That directory comes from the ACL2 interface/emacs/
  > directory.)  I went ahead and copied it over manually (as root).  File
  > load-inferior-acl2.el was also missing, as were README, README.doc, 
README.mss,
  > and README.ps.
  > 
  > More importantly, several ACL2 directories (and their subdirectories) were
  > missing from the extraction.  In order of importance (most to least), they 
are
  > as follows, where acl2-sources is the top-level ACL2 source directory:
  > 
  > acl2-sources/        [users need to be able to browse the sources]
  > acl2-sources/books/  [these are like "libraries" -- pre-proved theorems 
etc.]
  > acl2-sources/doc/    [HTML, Emacs info, and Postscript documentation]
  > acl2-sources/emacs/  [Some emacs utilities]
  > acl2-sources/interface/infix/
  > 
  > I don't know enough about traditional file organization to suggest where 
these
  > should go in a Debian package.  Our method has been to allow ACL2 users to
  > download ACL2 and put the acl2-sources directory anywhere they want,
  > maintaining the structure that we provide under acl2-sources/.  Under that
  > method, one of the first things to do is to run the "make certify-books"
  > command from acl2-sources/, in order to "certify" the many .lisp files under
  > acl2-sources/books/ (i.e., run them through ACL2).  This process compiles 
files
  > and, more importantly, writes out .cert files that have absolute pathnames. 
 I
  > don't know how that would fit into a Debian installation process.
  > 
  > >> > By the way, I'm hoping that we will release the next version (2.7) of 
ACL2
  > >> > later this month.  (It's been a year since we released ACL2 2.6.)
  > >> > 
  > >> 
  > >> Great!  Any surprises?
  > 
  > I don't think so.  The set of files has changed slightly, and of course the
  > contents of files have changed somewhat, but the basic structure is the 
same.
  > 
  > Thanks --
  > -- Matt
  >    Cc: address@hidden, address@hidden
  >    From: Camm Maguire <address@hidden>
  >    Date: 01 Nov 2002 19:41:24 -0500
  > 
  >    Greetings, and thanks for your reply!
  > 
  >    Matt Kaufmann <address@hidden> writes:
  > 
  >    > Hi, Camm --
  >    > 
  >    > That's really great that GCL is in such good shape!
  >    > 
  >    > I've added two targets to the top-level ACL2 Makefile for you, so that 
you can
  >    > easily run short tests.  In both cases, the exit status should be 0 if 
the test
  >    > succeeded and non-zero otherwise.  Two files need to be edited: 
Makefile and
  >    > books/Makefile.  At the end below are editing instructions, but if 
you'd rather
  >    > I just email you the entire files, let me know.
  >    > 
  > 
  >    Many thanks!  I've added these.  BTW, Debian's autobuilders expect
  >    *some* output from the build at least every 15 minutes.  For
  >    potentially long running tests with redirected standard output, I
  >    usually use this trick:
  > 
  >        $(MAKE) short-test-aux > short-test.log 2> short-test.log & j=$$! ; \
  >        tail -f --pid=$$j --retry short-test.log & wait $$j
  > 
  > 
  >    > >> Lastly, I'd be most appreciate if you or some other knowledgeable 
acl2
  >    > >> user could look at the package and comment as to whether everything 
is
  >    > >> available and in the right place.
  >    > 
  >    > Sure.  Please point me to where it is.  I don't know anything about 
Debian
  >    > packages but I'll try to find someone who does.  Or would it suffice 
to follow
  >    > the instructions at http://ftp.gnu.org/gnu/gcl/cvs/HOWTO-UNPACK-DEBS 
and build
  >    > it on my Redhat 7.3 laptop?
  >    > 
  > 
  >    http://ftp.debian.org/debian/pool/main/a/acl2/
  > 
  >    > By the way, I'm hoping that we will release the next version (2.7) of 
ACL2
  >    > later this month.  (It's been a year since we released ACL2 2.6.)
  >    > 
  > 
  >    Great!  Any surprises?
  > 
  >    > Finally, regarding your emacs point:
  >    > 
  >    > >> Also, a Debian user has already brought up a minor issue in the 
emacs
  >    > >> lisp interface regarding differences between xemacs and GNU emacs.  
He
  >    > >> is suggesting the following:
  >    > >> 
  >    > >> 
=============================================================================
  >    > >> (defun acl2-shared-lisp-mode-map ()
  >    > >>   "Return the shared lisp-mode-map, independent of Emacs version."
  >    > >>   (if (boundp 'shared-lisp-mode-map)
  >    > >>       shared-lisp-mode-map
  >    > >>     lisp-mode-shared-map))
  >    > >> 
  >    > >> and replacing references to shared-lisp-mode-map with
  >    > >> (acl2-shared-lisp-mode-map) ought to work.  (I actually even tested
  >    > >> the approach with GNU Emacs 20, GNU Emacs 21, and XEmacs 21 this
  >    > >> time; I get byte-compiler warnings, but that's all. ;-))
  >    > >> 
=============================================================================
  >    > >> 
  >    > >> Do you have any thoughts here?
  >    > 
  >    > Thanks very much.  I guess you're referring to directory 
interface/emacs/ in
  >    > the ACL2 distribution; is that right?  Your solution looks reasonable 
to me.
  >    > 
  > 
  >    OK, its in.
  > 
  > 
  >    Thanks again!
  > 
  > 
  >    -- 
  >    Camm Maguire                                             address@hidden
  >    
==========================================================================
  >    "The earth is but one country, and mankind its citizens."  --  
Baha'u'llah
  > 
  > 
  > _______________________________________________
  > Gcl-devel mailing list
  > address@hidden
  > http://mail.gnu.org/mailman/listinfo/gcl-devel
  > 
  > 

  -- 
  Camm Maguire                                          address@hidden
  ==========================================================================
  "The earth is but one country, and mankind its citizens."  --  Baha'u'llah

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

Here is a list, as promised above, of all book filenames.  A make target
analogous to "copy-distribution" could take advantage of this list; I'll
explain if you want more info.

books:
Makefile
Makefile-generic
Makefile-subdirs
README
README.html
arithmetic
arithmetic-2
bdd
certify-numbers.lisp
cli-misc
cowles
data-structures
finite-set-theory
ihs
meta
misc
# nonstd -- distributed separately
ordinals
powerlists
rtl
textbook
# workshops -- distributed separately

books/arithmetic:
Makefile
README
abs.lisp
binomial.lisp
certify.lsp
equalities.acl2
equalities.lisp
factorial.lisp
idiv.lisp
inequalities.lisp
mod-gcd.lisp
rational-listp.lisp
rationals.lisp
sumlist.lisp
top-with-meta.lisp
top.lisp

books/arithmetic-2:
Makefile
README
floor-mod
meta
pass1

books/arithmetic-2/floor-mod:
Makefile
floor-mod-helper.lisp
floor-mod.lisp

books/arithmetic-2/meta:
Makefile
README
cancel-terms-helper.lisp
cancel-terms-meta.lisp
collect-terms-meta.lisp
common-meta.lisp
expt-helper.lisp
expt.lisp
integerp-meta.lisp
integerp.lisp
mini-theories.lisp
non-linear.lisp
numerator-and-denominator.lisp
post.lisp
pre.lisp
top.lisp

books/arithmetic-2/pass1:
Makefile
arithmetic-axioms.txt
basic-arithmetic-helper.lisp
basic-arithmetic.lisp
expt-helper.lisp
expt.lisp
inequalities.lisp
mini-theories.lisp
numerator-and-denominator-helper.lisp
numerator-and-denominator.lisp
prefer-times.lisp
top.lisp

books/bdd:
Makefile
README
alu-proofs.lisp
alu.lisp
bdd-primitives.lisp
be
benchmarks.acl2
# benchmarks.lisp -- generated file
bit-vector-reader.lsp
bool-ops.lisp
cbf.lisp
certify.lsp
hamming.lisp
# init.lsp -- optionally user-generated, as explained in the README above
pg-theory.lisp

books/bdd/be:
cath
ex

books/bdd/be/cath:
add1.be
add2.be
add3.be
add4.be
addsub.be

books/bdd/be/ex:
mul03.be
mul04.be
mul05.be
mul06.be
mul07.be
mul08.be
rip02.be
rip04.be
rip06.be
rip08.be
transp.be
ztwaalf1.be
ztwaalf2.be

books/cli-misc:
README

books/cowles:
Makefile
README
acl2-agp.acl2
acl2-agp.lisp
acl2-asg.acl2
acl2-asg.lisp
acl2-crg.acl2
acl2-crg.lisp
certify.lsp

books/data-structures:
Makefile
README
alist-defthms.lisp
alist-defuns.lisp
alist-theory.lisp
array1.lisp
certify.lsp
defalist.acl2
defalist.lisp
define-structures-package.lisp
define-u-package.lisp
deflist.acl2
deflist.lisp
list-defthms.lisp
list-defuns.lisp
list-theory.lisp
number-list-defthms.lisp
number-list-defuns.lisp
number-list-theory.lisp
set-defthms.lisp
set-defuns.lisp
set-theory.lisp
structures.acl2
structures.lisp
utilities.acl2
utilities.lisp

books/finite-set-theory:
Makefile
certify.lsp
set-theory.acl2
set-theory.lisp
total-ordering.lisp

books/ihs:
@logops.lisp
Makefile
README
certify.lsp
ihs-definitions.lisp
ihs-init.acl2
ihs-init.lisp
ihs-lemmas.lisp
ihs-theories.lisp
logops-definitions.lisp
logops-lemmas.lisp
math-lemmas.lisp
quotient-remainder-lemmas.lisp

books/meta:
Makefile
README
certify.lsp
meta-plus-equal.lisp
meta-plus-lessp.lisp
meta-times-equal.lisp
meta.lisp
pseudo-termp-lemmas.lisp
term-defuns.lisp
term-lemmas.lisp

books/misc:
Makefile
README
certify.lsp
computed-hint.lisp
csort.lisp
dft-ex.acl2
dft-ex.lisp
dft.lisp
dump-events.lisp
expander.lisp
fibonacci.lisp
file-io.lisp
grcd.lisp
int-division.lisp
meta-lemmas.lisp
mult.lisp
priorities.lisp
problem13.lisp
records.lisp
records0.lisp
simplify-defuns.lisp
simplify-defuns.txt
sin-cos.lisp
symbol-btree.lisp
total-order.lisp

books/ordinals:
Makefile
README
basic-definitions-thms.lisp
certify.lsp
copyright
limits.lisp
ordinal-addition.lisp
ordinal-counter-examples.lisp
ordinal-definitions.lisp
ordinal-exponentiation.lisp
ordinal-isomorphism.lisp
ordinal-multiplication.lisp
ordinal-total-order.lisp
top-with-meta.lisp

books/powerlists:
Makefile
README
algebra.acl2
algebra.lisp
batcher-sort.acl2
batcher-sort.lisp
bitonic-sort.acl2
bitonic-sort.lisp
certify.lsp
cla-adder.acl2
cla-adder.lisp
defpkg.lisp
gray-code.acl2
gray-code.lisp
merge-sort.acl2
merge-sort.lisp
prefix-sum.acl2
prefix-sum.lisp
simple.acl2
simple.lisp
sort.acl2
sort.lisp

books/rtl:
Makefile
rel1
rel2
rel3

books/rtl/rel1:
Makefile
README
lib1
lib3
support

books/rtl/rel1/lib1:
Makefile
basic.lisp
bits.lisp
brat.lisp
float.lisp
reps.lisp
round.lisp
top.lisp

books/rtl/rel1/lib3:
Makefile
basic.lisp
bits.lisp
brat.lisp
fadd.lisp
float.lisp
reps.lisp
round.lisp
top.lisp

books/rtl/rel1/support:
Makefile
add.lisp
away.lisp
basic.lisp
divsqrt.lisp
fadd
float.lisp
floor.lisp
fp.lisp
logdefs.lisp
loglemmas.lisp
logxor-def.lisp
logxor-lemmas.lisp
merge.lisp
near.lisp
odd.lisp
proofs.lisp
reps.lisp
rewrite-theory.lisp
rnd.lisp
sticky.lisp
trunc.lisp
x-2xx.lisp

books/rtl/rel1/support/fadd:
Makefile
add3.lisp
lop1.lisp
lop2.lisp
lop3.lisp
stick.lisp
top.lisp

books/rtl/rel2:
Makefile
README
lib
support

books/rtl/rel2/lib:
Makefile
basic.lisp
bits.lisp
brat.lisp
cert.lsp
fadd.lisp
float.lisp
reps.lisp
round.lisp
top.lisp

books/rtl/rel2/support:
Makefile
add.lisp
add3.lisp
away.lisp
basic.lisp
bits-trunc.lisp
bits.lisp
cert.lsp
drnd.lisp
float.lisp
floor.lisp
fp.lisp
irepsproofs.lisp
log.lisp
lop1.lisp
lop2.lisp
lop3.lisp
merge.lisp
merge4.lisp
near+.lisp
near.lisp
odd.lisp
rem.lisp
repsproofs.lisp
rewrite-theory.lisp
rnd.lisp
setbits.lisp
stick.lisp
sticky.lisp
top.lisp
trunc.lisp
x-2xx.lisp

books/rtl/rel3:
Makefile
README
lib
support

books/rtl/rel3/lib:
Makefile
README
basic.lisp
bits.lisp
brat.lisp
cert.lsp
fadd.lisp
float.lisp
reps.lisp
round.lisp
top.lisp
top2.lisp

books/rtl/rel3/support:
Makefile
# README -- not distributed
add.lisp
add3.lisp
arith.lisp
arith2.lisp
ash.lisp
away.lisp
basic.lisp
bitn-proofs.lisp
bitn.lisp
bits-trunc.lisp
bits.lisp
bits2-proofs.lisp
bits2.lisp
bvecp-helpers.lisp
bvecp-lemmas.lisp
bvecp.lisp
cat.lisp
cert.lsp
comp1.lisp
complex-rationalp.lisp
decode.lisp
denominator.lisp
drnd.lisp
encode.lisp
even-odd.lisp
expo.lisp
expo2-proofs.lisp
expo2.lisp
expt.lisp
expt0.lisp
expt2-proofs.lisp
expt2.lisp
fl-expt.lisp
fl2.lisp
float.lisp
floor.lisp
flooreric-proofs.lisp
flooreric.lisp
fp.lisp
fp2.lisp
frac-coeff.lisp
ground-zero.lisp
induct.lisp
integerp.lisp
irepsproofs.lisp
log.lisp
logand-proofs.lisp
logand.lisp
lognot.lisp
logs.lisp
lop1.lisp
lop2.lisp
lop3.lisp
merge.lisp
mod-expt.lisp
mod.lisp
mod2.lisp
model-helpers.lisp
mulcat.lisp
near+.lisp
near.lisp
negative-syntaxp.lisp
nniq.lisp
numerator.lisp
odd.lisp
power2p.lisp
predicate.lisp
product.lisp
rationalp.lisp
rem.lisp
repsproofs.lisp
rewrite-theory.lisp
rnd.lisp
rom-helpers.lisp
rtl.lisp
rtlarr.lisp
setbitn.lisp
setbits.lisp
setbits2.lisp
sgn.lisp
shft.lisp
stick.lisp
stick2.lisp
sticky.lisp
top.lisp
trunc.lisp
type.lisp
unary-divide.lisp
x-2xx.lisp

books/textbook:
Makefile
README
chap10
chap11
chap3
chap4
chap5
chap6
chap7
# create-makefile.csh -- developer file
index.html

books/textbook/chap10:
Makefile
README
ac-example.lisp
adder.lisp
compiler.acl2
compiler.lisp
fact.lisp
insertion-sort.lisp
tree.lisp

books/textbook/chap11:
Makefile
README
compress.lisp
encap.lisp
finite-sets.lisp
how-many-soln1.lisp
how-many-soln2.lisp
mergesort.lisp
perm-append.lisp
perm.lisp
qsort.lisp
starters.lisp
summations-book.lisp
summations.lisp
tautology.lisp
xtr.lisp
xtr2.lisp

books/textbook/chap3:
Makefile
README
programs.lisp
solutions.txt

books/textbook/chap4:
Makefile
README
solutions-logic-mode.lisp
solutions-program-mode.lisp

books/textbook/chap5:
Makefile
README
solutions.lisp

books/textbook/chap6:
Makefile
README
selected-solutions.lisp
solutions.txt

books/textbook/chap7:
README
solutions.txt




reply via email to

[Prev in Thread] Current Thread [Next in Thread]