[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: |
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.
> 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)
> 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.
=============================================================================
--- 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
- [Gcl-devel] Re: gcl/acl2, (continued)
- [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, 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 <=
- 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
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/17
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/17