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: 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




reply via email to

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