[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: |
Sun, 17 Nov 2002 10:11:23 -0600 (CST) |
Hi --
Comments/replies are interspersed.
To: Matt Kaufmann <address@hidden>
Cc: address@hidden, address@hidden, address@hidden,
address@hidden
From: Camm Maguire <address@hidden>
Date: 17 Nov 2002 00:28:18 -0500
Greetings!
Matt Kaufmann <address@hidden> writes:
> 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.
>
The approach I've just tried is to basically ship the acl2 source tree
as is, with certs, into /usr/share/acl2-2.6, and then to push the
binaries into /usr/lib/acl2-2.6 and link them to the
/usr/share/acl2-2.6 directory. (include-book ...) works on the
precompiled precertified books without warning. It would seem that as
(include-book ) will take a fixed path, a user could simply create
another books directory in their home, no? That's the way I've left
it at present -- ordinary users cannot write into
/usr/share/acl2-2.6/books.
That will often be OK. But there are times where it is handy to use relative
pathnames. For example, if I create a book "foo.lisp" and I want to include
the top-level arithmetic book, then you're correct that I could use a full
pathname, e.g., (include-book "/usr/share/acl2-2.6/books/arithmetic/top").
However, if I can put foo.lisp in ..../books/my-books/, say, then I could
instead use (include-book "../arithmetic/top"). We encourage users to use
relative pathnames when they submit books for ACL2 workshops -- in fact I think
we tell them exactly where the book will wind up (e.g., in
books/workshops/2002/user-name/support/). That way, when they ship us their
contributions, we do not have to edit pathnames. However, as we discussed
earlier, someone can always copy books/ to their own space (using "cp -r", or
perhaps a script).
The above discussion could be viewed as a deficiency of ACL2. It has come up
previously that it would be nice to have a mechanism within ACL2 for specifying
the main books/ directory. There are potential subtle logical issues here
[I'll elaborate if you're interested], but I think it is possible and a good
idea. I've put this "main books/ directory" issue on the list of things to
consider for ACL2 Version 2.8.
By the way, I can imagine someone wanting to download ACL2 to a computer at
work and try it out, without getting sysadmins involved (hence, without root
priveleges). Of course, in that case they can just download ACL2 and build it
the old-fashioned way.
I'm interested in the advantages of having ACL2 as a Debian package. I can
imagine that one motivation is ease of installation. Perhaps another is that
it is generally a good thing for software packages to follow a common
installation paradigm. Are there others?
> 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.
Thanks for clarifying this.
>
> 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.
>
Agreed. Not shipping the stuff for compiler-link at this time.
> 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.
>
I agree with your concern, and truly do not want to alter the basic
layout of acl2 any more than necessary. I think the approach I've now
taken is more in line with this goal than the one I described above
earlier.
> 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.
>
I believe this is currently the case. The global site-start has:
(setq load-path (cons (concat "/usr/share/"
(symbol-name debian-emacs-flavor)
"/site-lisp/acl2") load-path ))
(autoload 'run-acl2
"top-start-inferior-acl2"
"Open communication between acl2 running in shell and prooftree." t)
(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)
Thanks; looks good.
> 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.)
>
I've compiled this as part of the package and included it in like
manner to the other elements.
> 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?
>
Typically two reasons -- 1) give the user the option of installing
just what she needs, and 2) saved space in the archive, as
binary-independent stuff need not appear 11 times :-).
I thought I'd just post the current diff I'm using to build the
package. I can elaborate on the rationale later if desired. The diff
is very small. The .el changes are to enable compilation under Xemacs
as well as GNU emacs.
Thanks for sending those. I took a quick scan and didn't see anything
problematic. Perhaps we will incorporate some of the changes into Version 2.8
(which we will start on after 2.7 is released).
Thanks again for your efforts.
-- Matt
=============================================================================
--- acl2-2.6.orig/Makefile
+++ acl2-2.6/Makefile
@@ -717,3 +717,18 @@
# target, since move-large will not move the .dxl file (similarly
# for cmulisp and CLISP).
arch: full init move-large small regression-fresh proofs
+
+#
+# added per instructions from Matt Kauffman for autobuilder testing
+#
+
+mini-proveall:
+ @rm -rf mini-proveall.out
+ @echo '(value :q) (lp) (mini-proveall)' | ./${PREFIXsaved_acl2} >
mini-proveall.out
+ @(grep '^ ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR-TEST'
mini-proveall.out > /dev/null) || \
+ (echo 'Mini-proveall failed!' ; exit 1)
+ @echo 'Mini-proveall passed.'
+
+certify-books-short:
+ cd books ; make short-test
+
--- acl2-2.6.orig/doc/EMACS/acl2-doc-emacs.info
+++ acl2-2.6/doc/EMACS/acl2-doc-emacs.info
@@ -26,6 +26,11 @@
Sciences University of Texas at Austin Austin, TX 78712-1188 U.S.A.
+INFO-DIR-SECTION Math
+START-INFO-DIR-ENTRY
+* acl2: (acl2-doc-emacs.info). Applicative Common Lisp
+END-INFO-DIR-ENTRY
+
--- acl2-2.6.orig/books/Makefile
+++ acl2-2.6/books/Makefile
@@ -55,6 +55,16 @@
DIRS3 = data-structures bdd misc ihs rtl finite-set-theory powerlists \
textbook arithmetic-2
+#
+# added per instructions from Matt Kauffman for autobuilder testing
+#
+
+SHORTDIRS2 = data-structures bdd
+
+#
+#
+#
+
.PHONY: $(DIRS1) $(DIRS2) $(DIRS3)
# Same as below, using DIRS3 instead of DIRS2. Much faster!! Omits
@@ -285,3 +295,41 @@
# Tar up books and support, not including workshops or nonstd stuff.
tar:
tar cvf books.tar Makefile Makefile-generic Makefile-subdirs README
README.html certify-numbers.lisp $(DIRS1) $(DIRS3)
+
+#
+# added per instructions from Matt Kauffman for autobuilder testing
+#
+
+short-clean:
+ @rm -f short-test.log
+ @for dir in $(DIRS1) $(SHORTDIRS2) ; \
+ do \
+ (cd $$dir ; \
+ $(MAKE) clean ; \
+ cd ..) ; \
+ done
+
+short-test-aux:
+ @for dir in $(DIRS1) ; \
+ do \
+ (cd $$dir ; \
+ $(MAKE) all ; \
+ cd ..) ; \
+ done
+ @$(MAKE) top-with-meta-cert
+ @for dir in $(SHORTDIRS2) ; \
+ do \
+ (cd $$dir ; \
+ $(MAKE) all ; \
+ cd ..) ; \
+ done
+
+short-test:
+ @rm -f short-test.log
+ $(MAKE) short-clean
+ $(MAKE) short-test-aux > short-test.log 2> short-test.log & j=$$! ; \
+ tail -f --pid=$$j --retry short-test.log & wait $$j
+ @if [ ! -f short-test.log ] || (fgrep '**' short-test.log > /dev/null)
; then \
+ (echo 'Short test failed!' ; exit 1) ; else \
+ echo 'Short test passed.' ; fi
+
--- acl2-2.6.orig/interface/emacs/acl2-interface.el
+++ acl2-2.6/interface/emacs/acl2-interface.el
@@ -28,13 +28,18 @@
;; ----------------------------------------------------------------------
;; Load all of the various acl2-interface files, if necessary.
-(load "inf-acl2.el") ;(require 'inf-acl2)
-(load "mfm-acl2.el") ;(require 'mfm-acl2)
-(load "interface-macros.el") ;(require 'interface-macros)
+;(load "inf-acl2.el") ;(require 'inf-acl2)
+;(load "mfm-acl2.el") ;(require 'mfm-acl2)
+;(load "interface-macros.el") ;(require 'interface-macros)
+
+(require 'inf-acl2)
+(require 'mfm-acl2)
+(require 'interface-macros)
(update-mode-menu-alist *acl2-user-map-interface*)
-(load "acl2-interface-functions.el")
+;(load "acl2-interface-functions.el")
+(load "acl2-interface-functions")
;; ----------------------------------------------------------------------
;; Specials used by functions in interface-macros.el.
--- acl2-2.6.orig/interface/emacs/acl2-mode.el
+++ acl2-2.6/interface/emacs/acl2-mode.el
@@ -45,14 +45,25 @@
(make-local-variable 'lisp-indent-function)
(setq lisp-indent-function 'acl2-indent-function))
+;; To handle differing xemacs/emacs behavior
+;(if (and (boundp 'shared-lisp-mode-map)
+; (not (boundp 'lisp-mode-shared-map)))
+; (defvaralias 'lisp-mode-shared-map 'shared-lisp-mode-map))
+
+(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))
+
(defvar acl2-mode-map nil
"Keymap for ordinary Acl2 mode. All commands in
-`shared-lisp-mode-map' are inherited by this map.")
+`acl2-shared-lisp-mode-map' are inherited by this map.")
-(if acl2-mode-map
- nil
- (setq acl2-mode-map
- (nconc (make-sparse-keymap) shared-lisp-mode-map)))
+(if (not acl2-mode-map)
+ (progn
+ (setq acl2-mode-map (make-sparse-keymap))
+ (set-keymap-parent acl2-mode-map (acl2-shared-lisp-mode-map))))
(defvar acl2-mode-hook nil)
--- acl2-2.6.orig/interface/emacs/inf-acl2.el
+++ acl2-2.6/interface/emacs/inf-acl2.el
@@ -123,7 +123,8 @@
(defvar inferior-acl2-mode-map nil)
(cond ((not inferior-acl2-mode-map)
(setq inferior-acl2-mode-map (copy-keymap comint-mode-map))
- (setq inferior-acl2-mode-map (nconc inferior-acl2-mode-map
shared-lisp-mode-map))))
+; (setq inferior-acl2-mode-map (nconc inferior-acl2-mode-map
shared-lisp-mode-map))))
+ (set-keymap-parent inferior-acl2-mode-map
(acl2-shared-lisp-mode-map))))
;;; This function exists for backwards compatibility.
--- acl2-2.6.orig/interface/emacs/interface-macros.el
+++ acl2-2.6/interface/emacs/interface-macros.el
@@ -223,7 +223,7 @@
(defun define-selection-function (function-name menu-name)
(eval
- (substitute
+ (acl2-substitute
(list (cons '*menu-select* function-name)
(cons '*menu* menu-name))
'(defun *menu-select* (click)
@@ -403,12 +403,12 @@
(let ((x (mouse-position)))
(list (list (car (cdr x)) (cdr (cdr x))) (car x))))
-(defun substitute (alist form)
+(defun acl2-substitute (alist form)
(cond ((not (consp form))
(let ((pair (assoc form alist)))
(if pair (cdr pair) form)))
- (t (cons (substitute alist (car form))
- (substitute alist (cdr form))))))
+ (t (cons (acl2-substitute alist (car form))
+ (acl2-substitute alist (cdr form))))))
(defun subst (new old form)
(cond ((equal form old) new)
@@ -591,7 +591,7 @@
(<mode>-prefix-keys (concat (symbol-name xxx) "-keys-")))
(if (equal <mode>-popup-menu-name popup-menu)
(setq <mode>-popup-menu-name (make-function-name
<mode>-popup-menu-name "-2")))
- (substitute (list (cons '<mode>-map-name mode-map-name)
+ (acl2-substitute (list (cons '<mode>-map-name mode-map-name)
(cons '<mode>-menu-bar menu-bar)
(cons '<mode>-menu-bar-remove menu-bar-remove)
(cons '<mode>-popup-menu popup-menu)
--- acl2-2.6.orig/interface/infix/infix.lisp
+++ acl2-2.6/interface/infix/infix.lisp
@@ -84,7 +84,7 @@
;; Load packages and macros we depend on.
;; Require must be here.
-(require "sloop" "/slocal/src/acl2/v1-8/interface/infix/sloop")
+;(require "sloop" "/acl2/interface/infix/sloop")
(use-package "SLOOP")
--- acl2-2.6.orig/interface/infix/makefile
+++ acl2-2.6/interface/infix/makefile
@@ -16,16 +16,16 @@
# make full ; Clean, compile, create TAGS, and print example in
MODE.
LISP = acl2
-DIR = /slocal/src/acl2/v1-8/interface/infix
+DIR = /acl2/interface/infix
SAVED = ${DIR}/Save
# TEST = ${DIR}/test
TEST = ${DIR}/books
-MODE = "scribe"
-# MODE = "latex"
+# MODE = "scribe"
+MODE = "latex"
LPR = lpr
DVI = dvips
-sources = sloop.lisp infix.lisp scribe-init.lisp latex-init.lisp
+sources = infix.lisp scribe-init.lisp latex-init.lisp #sloop.lisp
# 'make' without a target uses the first one, e.g.
@@ -33,7 +33,7 @@
rm -f workxxx
echo ':q' > workxxx
echo '(in-package "user")' >> workxxx
- echo '(compile-file "sloop.lisp")' >> workxxx
+# echo '(compile-file "sloop.lisp")' >> workxxx
echo '(compile-file "infix.lisp")' >> workxxx
echo '(load "infix")' >> workxxx
echo '(compile-file "scribe-init.lisp")' >> workxxx
@@ -45,7 +45,7 @@
tags: ${sources}
etags *.lisp
-
+
example:
rm -f workxxx
echo ':q' > workxxx
@@ -56,10 +56,10 @@
if [ ${MODE} = "scribe" ] ; then \
scribe infix-examples.mss ; scribe infix-examples.mss ; ${LPR}
infix-examples.ps;\
else \
- rm -f infix-examples.aux ; latex infix-examples ; ${DVI}
infix-examples ; \
+ rm -f infix-examples.aux ; latex infix-examples ; ${DVI} -o
infix-examples.ps infix-examples ; \
fi
-events: clean-doc
+events: #clean-doc
rm -f workxxx
echo ':q' > workxxx
echo '(in-package "user")' >> workxxx
@@ -68,15 +68,15 @@
${LISP} < workxxx
if [ ${MODE} = "scribe" ] ; then \
scribe sample.mss ; else \
- latex sample ; \
+ latex sample && latex sample && ${DVI} -o sample.ps sample ; \
fi
clean-all: clean
rm -f *.o TAGS
clean: clean-doc
- rm -f *~* *#* workxxx
+ rm -f *~* *#* workxxx *.o *.tex *.nqtex TAGS
clean-doc:
rm -f ${DIR}/*.otl ${DIR}/*.err ${DIR}/*.ps ${DIR}/*.aux
- rm -f ${DIR}/*.dvi ${DIR}/*.aux ${DIR}/*.log ${DIR}/*.idx
+ rm -f ${DIR}/*.dvi ${DIR}/*.aux ${DIR}/*.log ${DIR}/*.idx ${DIR}/.log
=============================================================================
Take care,
> 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
>
>
--
Camm Maguire address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
- Re: [Gcl-devel] Re: gcl/acl2, (continued)
- 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, 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 <=
- 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
- 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