[nongnu] elpa/proof-general da5f073 06/13: Remove ACL2 support

[ELPA Syncer]

branch: elpa/proof-general
commit da5f073fe2c496749d4cb561ffb28273215aa2ba
Author: Stefan Monnier <monnier@iro.umontreal.ca>
Commit: Stefan Monnier <monnier@iro.umontreal.ca>

    Remove ACL2 support
---
 Makefile              |   4 +-
 README.md             |   4 +-
 acl2/README           |  22 ----
 acl2/acl2.el          | 106 ---------------
 acl2/example.acl2     |   9 --
 acl2/root2.acl2       | 348 --------------------------------------------------
 doc/ProofGeneral.texi |   3 +-
 generic/proof-site.el |   1 -
 8 files changed, 5 insertions(+), 492 deletions(-)

diff --git a/Makefile b/Makefile
index f23ff28..66a77d9 100644
--- a/Makefile
+++ b/Makefile
@@ -35,7 +35,7 @@ PREFIX=$(DESTDIR)/usr
 DEST_PREFIX=$(DESTDIR)/usr
 
 # subdirectories for provers: to be compiled and installed
-PROVERS=acl2 coq easycrypt isar pghaskell pgocaml pgshell phox
+PROVERS=coq easycrypt isar pghaskell pgocaml pgshell phox
 
 # generic lisp code: to be compiled and installed
 OTHER_ELISP=generic lib
@@ -58,7 +58,7 @@ ELISP_EXTRAS=
 EXTRA_DIRS = images
 
 DOC_FILES=AUTHORS BUGS COMPATIBILITY CHANGES COPYING INSTALL README REGISTER 
doc/*.pdf
-DOC_EXAMPLES=acl2/*.acl2 isar/*.thy lclam/*.lcm pgshell/*.pgsh phox/*.phx 
plastic/*.lf
+DOC_EXAMPLES=isar/*.thy lclam/*.lcm pgshell/*.pgsh phox/*.phx plastic/*.lf
 DOC_SUBDIRS=${DOC_EXAMPLES} */README* */CHANGES */BUGS 
 
 BATCHEMACS=${EMACS} --batch --no-site-file -q 
diff --git a/README.md b/README.md
index d10078a..66f2d17 100644
--- a/README.md
+++ b/README.md
@@ -140,9 +140,9 @@ instances are no longer maintained nor available in the 
MELPA package:
 * Legacy support of
   [Isabelle](https://www.cl.cam.ac.uk/research/hvg/Isabelle/)
   
-* Experimental support of: ACL2, Lambda-Clam, Shell
+* Experimental support of: Lambda-Clam, Shell
 * Obsolete instances: Demoisa, Lambda-Clam, Plastic
-* Removed instances: Twelf, CCC, Hol-Light, HOL98,
+* Removed instances: Twelf, CCC, Hol-Light, ACL2, HOL98,
   [LEGO](http://www.dcs.ed.ac.uk/home/lego)
 
 A few example proofs are included in each prover subdirectory.
diff --git a/acl2/README b/acl2/README
deleted file mode 100644
index fbe9344..0000000
--- a/acl2/README
+++ /dev/null
@@ -1,22 +0,0 @@
-ACL2 Proof General, for ACL2.
-
-Written by David Aspinall.
-
-Status:               alpha; unsupported
-Maintainer:    volunteer required
-ACL2 version:  Tested briefly with acl2.5
-ACL2 homepage: http://www.cs.utexas.edu/users/moore/acl2
-
-========================================
-
-This is the absolute bare beginnings of a PG instance for ACL2.
-At the moment, only basic script management is configured.
-
-I have written this in the hope that somebody from the ACL2 community
-will adopt it, maintain and improve it, and thus turn it into a proper
-instantiation of Proof General.
-
-
-
-$Id$
-
diff --git a/acl2/acl2.el b/acl2/acl2.el
deleted file mode 100644
index db3120e..0000000
--- a/acl2/acl2.el
+++ /dev/null
@@ -1,106 +0,0 @@
-;;; acl2.el --- Basic Proof General instance for ACL2
-
-;; This file is part of Proof General.
-
-;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
-;; Portions © Copyright 2001-2017  Pierre Courtieu
-;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
-;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
-;; Portions © Copyright 2015-2017  Clément Pit-Claudel
-
-;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-
-;; Author:    David Aspinall <David.Aspinall@ed.ac.uk>
-
-;;; Commentary:
-;;
-;; Needs improvement!
-;;
-;; See the README file in this directory for information.
-
-;;; Code:
-
-(require 'proof-easy-config)            ; easy configure mechanism
-(require 'proof-syntax)                        ; functions for making regexps
-
-(add-to-list 'auto-mode-alist                ; ACL2 uses two file extensions
-                                             ; Only grab .lisp extension after
-             (cons "\\.lisp\\'" 'acl2-mode)) ; an acl2 file has been loaded
-
-(proof-easy-config  'acl2 "ACL2"
- proof-assistant-home-page       "http://www.cs.utexas.edu/users/moore/acl2";
- proof-prog-name                "acl2"
-
- proof-script-sexp-commands     t
- proof-script-comment-start    ";"
-
- proof-shell-annotated-prompt-regexp "ACL2[ !]*>+"
-
- proof-save-command-regexp      "(def\\w+\\s "
- proof-goal-command-regexp       "(def\\w+\\s "
- proof-save-with-hole-regexp     "(def\\w+[ \t\n]+\\(\\w+\\)"
- proof-save-with-hole-result    1
- proof-shell-error-regexp
- "^Error: \\|Error in TOP-LEVEL: \\|\\*\\*\\*\\* FAILED \\*\\*\\*"
- proof-shell-interrupt-regexp    "Correctable error: Console interrupt."
-
- proof-shell-quit-cmd            ":q"   ;; FIXME: followed by C-d.
- proof-shell-restart-cmd        ":q\n:q\n:q\n(lp)\n"    ;; FIXME: maybe not?
- proof-info-command             ":help"
- proof-undo-n-times-cmd                 ":ubt %s"  ;; shouldn't give errors
- proof-forget-id-command        ":ubt %s"  ;; so use ubt not ubt!
- proof-context-command          ":pbt :max"
- ;; proof-showproof-cmd                 ":pbt :here"
-
- proof-shell-truncate-before-error nil
-
- ;;
- ;; Syntax table entries for proof scripts  (FIXME: incomplete)
- ;;
- proof-script-syntax-table-entries
- '(?\[ "(]  "
-   ?\] "([  "
-   ?\( "()  "
-   ?\) ")(  "
-   ?.  "w   "
-   ?_  "w   "
-   ?-  "w   "
-   ?>  "w   " ;; things treated as names can have > in them
-   ?#  "'   "
-   ?\' "'    "
-   ?`  "'    "
-   ?,  "'    "
-   ?\| "."
-   ?\; "<    "
-   ?\n ">    "
-   )
-
- ;; A tiny bit of syntax highlighting
- ;;
- proof-script-font-lock-keywords
- (append
-  (list
-   (proof-ids-to-regexp '("defthm" "defabbrev" "defaxiom" "defchoose"
-                         "defcong" "defconst" "defdoc" "defequiv"
-                         "defevaluator" "defpackage" "deflabel" "deftheory"
-                         "implies" "equal" "and")))
-  (if (boundp 'lisp-font-lock-keywords) ;; wins if font-lock is loaded
-      lisp-font-lock-keywords))
-
-
- ;; End of easy config.
- )
-
-;; Interrupts and errors enter another loop; break out of it
-(add-hook
- 'proof-shell-handle-error-or-interrupt-hook
- (lambda () (if (eq proof-shell-error-or-interrupt-seen 'interrupt)
-               (proof-shell-insert ":q" nil))))
-
-
-
-(warn "ACL2 Proof General is incomplete!  Please help improve it!
-Please add improvements at https://github.com/ProofGeneral/PG";)
-
-(provide 'acl2)
diff --git a/acl2/example.acl2 b/acl2/example.acl2
deleted file mode 100644
index a3a0f21..0000000
--- a/acl2/example.acl2
+++ /dev/null
@@ -1,9 +0,0 @@
-;;  Example proof script for ACL2 Proof General.
-;;
-;;   $Id$
-;;    
-
-(defthm assoc->assoc-equal
-  (equal (assoc x a)
-        (assoc-equal x a)))
-
diff --git a/acl2/root2.acl2 b/acl2/root2.acl2
deleted file mode 100644
index c60d05e..0000000
--- a/acl2/root2.acl2
+++ /dev/null
@@ -1,348 +0,0 @@
-(* Example proof by Ruben Gamboa.  
-   See http://www.cs.kun.nl/~freek/comparison/ *)
-
-
-(in-package "ACL2")
-
-;; This book presents the proof that sqrt(2) is an irrational number.
-;; The proof proceeds by observing that p^2 is even precisely when p
-;; is even.  Thus, if p^2 = 2 q^2, p must be even.  But then, p^2
-;; isn't just even, it's a multiple of 4, so q^2 = p^2 / 2 must also
-;; be even.  But since q^2 is even, so is q.  Now, letting p be the
-;; numerator of 2 and q the denominator of 2, we find that both the
-;; numerator and denominator are even -- but this is an
-;; impossibility.  Hence, we can conclude that 2 is not rational.
-
-;; The proof is completed by observing that sqrt(2) is not complex.
-;; The reason is that if x is complex, x^2 is real only when x is a
-;; pure imaginary number.  But in those cases, x^2 is negative
-
-(include-book "../arithmetic/top"
-             :load-compiled-file nil)
-
-;; Step 1: We begin by proving that p^2 is even precisely when p is
-;; even.
-
-(encapsulate
- ()
-
- ;; Since ACL2 is so strong in induction, it is common to use
- ;; induction to prove simple number theoretic results.  But to induce
- ;; over the even numbers requires that each time through the
- ;; induction we "step" by 2, not the usual 1.  So we start by
- ;; introducing the induction scheme for the even numbers.
-
- (local
-  (defun even-induction (x)
-    "Induct by going two steps at a time"
-    (if (or (zp x) (equal x 1))
-       x
-      (1+ (even-induction (1- (1- x)))))))
-
- ;; Now we can prove that if p^2 is even, so is p.  Because we're
- ;; doing this inductively, we only consider the even naturals to
- ;; begin with.
-
- (local
-  (defthm lemma-1
-    (implies (and (integerp p)
-                 (<= 0 p)
-                 (evenp (* p p)))
-            (evenp p))
-    :hints (("Goal"
-            :induct (even-induction p)))
-    :rule-classes nil))
-
- ;; Technically, we do not need to worry about the negative integers
- ;; in this proof, since both the numerator and denominator of 2 (if
- ;; they existed) are positive.  But it's easy enough to prove this,
- ;; and it gets rid of the "non-negative" hypothesis.  In general, it
- ;; is good to get rid of hypothesis in ACL2 rewrite rules.
-
- (local
-  (defthm lemma-2
-    (implies (and (integerp p)
-                 (<= p 0)
-                 (evenp (* p p)))
-            (evenp p))
-    :hints (("Goal"
-            :use (:instance lemma-1 (p (- p)))))
-    :rule-classes nil))
-
- ;; Now, we can prove that if p^2 is even, so is p.  But the converse
- ;; is trivial, so we could show that p^2 is even iff p is even.
- ;; Because equalities are more powerful rewrite rules than
- ;; implications, we prefer to do so, even though we don't really need
- ;; the stronger equality for this proof.  So we prove the converse
- ;; here: if p is even, so is p^2.
-
- (local
-  (defthm lemma-3
-    (implies (and (integerp p)
-                 (evenp p))
-            (evenp (* p p)))
-    :rule-classes nil))
-    
- ;; Now, we simply collect the results above to find that p^2 is even
- ;; if and only if p is even.  This is the only theorem that is
- ;; exported from this event.
-
- (defthm even-square-implies-even
-   (implies (integerp p)
-           (equal (evenp (* p p)) (evenp p)))
-   :hints (("Goal"
-           :use ((:instance lemma-1)
-                 (:instance lemma-2)
-                 (:instance lemma-3)))))
- )
-
-;; Step 2. Suppose p^2 is even.  Then, p is even, so p^2 is more than
-;; even -- it is a multiple of 4.  We prove this here, since it is the
-;; key fact allowing us to conclude that q^2 is even when we know that
-;; p^2 = 2 * q^2.
-
-(defthm even-square-implies-even-square-multiple-of-4
-  (implies (and (integerp p)
-               (evenp (* p p)))
-          (evenp (* 1/2 p p)))
-  :hints (("Goal"
-          :use ((:instance even-square-implies-even)
-                (:instance (:theorem (implies (integerp x) (integerp (* x x))))
-                           (x (* 1/2 p))))
-          :in-theory (disable even-square-implies-even))))
-
-;; In the proofs below, we disable ACL2's definition of even, but we
-;; need to remember that 2*n is always even.  So we prove that rewrite
-;; rule here.
-
-(defthm evenp-2x
-  (implies (integerp x)
-          (evenp (* 2 x))))
-
-;; Step 3. Suppose p^2 = 2 * q^2.  Then we can conclude that p is
-;; even, since p^2 is even.
-
-(defthm numerator-sqrt-2-is-even
-   (implies (and (integerp p)
-                (integerp q)
-                (equal (* p p)
-                       (* 2 (* q q))))
-           (evenp p))
-   :hints (("Goal"
-           :use ((:instance even-square-implies-even)
-                 (:instance evenp-2x (x (* q q))))
-           :in-theory (disable even-square-implies-even
-                               evenp-2x
-                               evenp))))
-
-;; Step 4. Suppose p^2 = 2 * q^2.  Then we can conclude that q is
-;; even, since p^2 is a multiple of 4, so q^2 is even.
-
-(defthm denominator-sqrt-2-is-even
-   (implies (and (integerp p)
-                (integerp q)
-                (equal (* p p)
-                       (* 2 (* q q))))
-           (evenp q))
-   :hints (("Goal"
-           :use ((:instance even-square-implies-even-square-multiple-of-4)
-                 (:instance even-square-implies-even (p q))
-                 (:instance evenp-2x 
-                            (x (* q q)))
-                 (:instance equal-*-/-1
-                            (x 2)
-                            (y (* p p))
-                            (z (* q q))))
-           :in-theory (disable even-square-implies-even-square-multiple-of-4
-                               even-square-implies-even
-                               evenp-2x
-                               evenp
-                               equal-*-/-1))))
-
-;; Step 5.  Those are all the pieces we need to prove that sqrt(2) is
-;; not rational.  For we observe that if p=numerator(sqrt(2)) and
-;; q=denominator(sqrt(2)), the theorems above show that both p and q
-;; are even, and that's an absurdity.
-
-(encapsulate
- ()
-
- ;; ACL2's algebraic prowess is modest.  In the proof of the main
- ;; theorem below, it builds the expression p^2/q^2 where x=p/q, but
- ;; it does not reduce the expression further to x^2.  We add a
- ;; rewrite rule to take care of that.
-
- (local
-  (defthm lemma-1
-    (implies (rationalp x)
-            (equal (* (/ (denominator x))
-                      (/ (denominator x))
-                      (numerator x)
-                      (numerator x))
-                   (* x x)))
-    :hints (("Goal"
-            :use ((:instance Rational-implies2)
-                  (:instance *-r-denominator-r (r x)))
-            :in-theory (disable Rational-implies2
-                                *-r-denominator-r)))))
-
- ;; Now we can prove that the square root of 2 is not rational.  This
- ;; involves using the theorems defined above, as well as some
- ;; algebraic lemmas to help reduce the terms.  The most important
- ;; hint, however, is the inclusion of the axiom Lowest-Terms, because
- ;; it is not enabled in the ACL2 world.
-
- (defthm sqrt-2-not-rational
-   (implies (equal (* x x) 2)
-           (not (rationalp x)))
-   :hints (("Goal"
-           :use ((:instance numerator-sqrt-2-is-even
-                            (p (numerator x))
-                            (q (denominator x)))
-                 (:instance denominator-sqrt-2-is-even
-                            (p (numerator x))
-                            (q (denominator x)))       
-                 (:instance Lowest-Terms
-                            (n 2)
-                            (r (/ (numerator x) 2))
-                            (q (/ (denominator x) 2)))
-                 (:instance equal-*-/-1
-                            (x (/ (* (denominator x) (denominator x))))
-                            (y 2)
-                            (z (* (numerator x) (numerator x)))))
-           :in-theory (disable equal-*-/-1
-                               numerator-sqrt-2-is-even
-                               denominator-sqrt-2-is-even))))
- )
-
-;; Step 6. Now that the rationals are ruled out, we need to weed out
-;; the remaining sqrt(2) suspects.  One possibility is that sqrt(2) is
-;; a complex number.  We explore that here.  Because ACL2 has very
-;; little knowledge of the complex numbers, we have to start with some
-;; basic facts.  First, we show that (a+bi)^2 = (a^2-b^2)+(ab+ab)i.
-(encapsulate
- ()
-
- ;; We start out with the desired theorem when the complex number is
- ;; written as a+bi instead of (complex a b).  Here, the result
- ;; follows from simple algebra and the fact that i^2=-1.
- (local
-  (defthm lemma-1
-    (equal (* (+ x (* #c(0 1) y))
-             (+ x (* #c(0 1) y)))
-          (+ (- (* x x) (* y y))
-             (* #c(0 1) (+ (* x y) (* x y)))))
-    :rule-classes nil))
-
- ;; Now we rewrite the right-hand side of the rewrite rule into the
- ;; final form of (complex (a^2-b^2) (ab+ab))
- (local
-  (defthm lemma-2
-    (implies (and (realp x)
-                 (realp y))
-            (equal (* (+ x (* #c(0 1) y))
-                      (+ x (* #c(0 1) y)))
-                   (complex (- (* x x) (* y y))
-                            (+ (* x y) (* x y)))))
-    :hints (("Goal"
-            :use ((:instance lemma-1)
-                  (:instance complex-definition
-                             (x (- (* x x) (* y y)))
-                             (y (+ (* x y) (* x y)))))))
-    :rule-classes nil))
-
- ;; And finally we rewrite the left-hand side of the rewrite rule into
- ;; the final form of (complex a b)^2.
- (defthm complex-square-definition
-   (implies (and (realp x)
-                (realp y))
-           (equal (* (complex x y) (complex x y))
-                  (complex (- (* x x) (* y y))
-                           (+ (* x y) (* x y)))))
-   :hints (("Goal"
-           :use ((:instance complex-definition)
-                 (:instance lemma-2))))
-   :rule-classes nil)
- )
-
-;; Step 7.  Since (a+bi)^2 = (a^2-b^2)+(ab+ab)i, it follows that it is
-;; real if and only if a or b is zero, i.e., if and only if the number
-;; is real or pure imaginary.  Since we're interested only in the
-;; non-real complex numbers (the ones for which complexp is true), we
-;; can conlude that only pure imaginaries have real squares.
-(encapsulate
- ()
-
- ;; First we show that (a+bi)^2 = (a^2-b^2)+(ab+ab)i is real if and
- ;; only ab+ab is zero.
- (local
-  (defthm lemma-1
-    (implies (and (complexp x)
-                 (realp (* x x)))
-            (equal (+ (* (realpart x) (imagpart x))
-                      (* (realpart x) (imagpart x)))
-                   0))
-    :hints (("Goal"
-            :use (:instance complex-square-definition
-                            (x (realpart x))
-                            (y (imagpart x)))))
-    :rule-classes nil))
-
- ;; The following rewrite rule allows us to conclude that a real
- ;; number x is zero whenever x+x is zero.
- (local
-  (defthm lemma-2
-    (implies (and (realp x)
-                 (equal (+ x x) 0))
-            (= x 0))))
-
- ;; The two lemmas above conclude that ab is zero whenever (a+bi)^2 is
- ;; zero, and since b is assumed non-zero (because a+bi is complex),
- ;; we have that a must be zero, and a+bi=bi is a pure imaginary
- ;; number.
- (defthm complex-squares-real-iff-imaginary
-   (implies (and (complexp x)
-                (realp (* x x)))
-           (equal (realpart x) 0))
-   :hints (("Goal"
-           :use ((:instance lemma-1)
-                 (:instance lemma-2
-                            (x (* (realpart x) (imagpart x))))))))
- )
-
-;; Step 7.  Trivially, the square of a pure imaginary number bi is a
-;; negative real, since bi^2 = -b^2.
-(defthm imaginary-squares-are-negative
-  (implies (and (complexp x)
-               (equal (realpart x) 0))
-          (< (* x x) 0))
-  :hints (("Goal"
-          :use (:instance complex-square-definition
-                          (x 0)
-                          (y (imagpart x))))))
-
-;; Step 8.  From the theorems above, we can conclude that sqrt(2) is
-;; not a complex number, because the only candidates are the pure
-;; imaginary numbers, and their squares are all negative.
-(defthm sqrt-2-not-complexp
-  (implies (complexp x)
-          (not (equal (* x x) 2)))
-  :hints (("Goal"
-          :use ((:instance complex-squares-real-iff-imaginary)
-                (:instance imaginary-squares-are-negative)))))
-
-;; Step 9.  That means sqrt(2) is not rational, and neither is it a
-;; complex number.  The only remaining candidates (in ACL2's universe)
-;; are the non-rational reals, so we can prove the main result: the
-;; square root of two (if it exists) is irrational.
-(defthm irrational-sqrt-2
-  (implies (equal (* x x) 2)
-          (and (realp x)
-               (not (rationalp x))))
-  :hints (("Goal"
-          :cases ((rationalp x) (complexp x)))))
-
-;; Step 10.  Next, it would be nice to show that sqrt(2) actually
-;; exists!  See the book nonstd/nsa/sqrt.lisp for a proof of that,
-;; using non-standard analysis.
-
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 4a31443..869fa87 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -207,7 +207,7 @@ other documentation, system downloads, etc.
 @cindex news
 
 The old code for the support of the following systems have been
-removed: Twelf, CCC, Lego, Hol-Light, HOL98.
+removed: Twelf, CCC, Lego, Hol-Light, ACL2, HOL98.
 
 @node News for Version 4.4
 @unnumberedsec News for Version 4.4
@@ -516,7 +516,6 @@ script file for your proof assistant, for example:
 @item       Coq           @tab @file{.v}      @tab @code{coq-mode}
 @item       Isabelle      @tab @file{.thy}    @tab @code{isar-mode}
 @item       Phox          @tab @file{.phx}    @tab @code{phox-mode}
-@item       ACL2          @tab @file{.acl2}   @tab @code{acl2-mode}
 @item       Plastic       @tab @file{.lf}     @tab @code{plastic-mode}
 @item       Lambda-CLAM   @tab @file{.lcm}    @tab @code{lclam-mode}
 @item       PG-Shell      @tab @file{.pgsh}   @tab @code{pgshell-mode}
diff --git a/generic/proof-site.el b/generic/proof-site.el
index d2c282f..7286628 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -57,7 +57,6 @@
 
       ;; Incomplete/obsolete:
 
-      ;; (acl2 "ACL2" "acl2")
       ;; (plastic "Plastic" "lf")        ; obsolete
       ;; (lclam "Lambda-CLAM" "lcm")     ; obsolete
       ;; (demoisa "Isabelle Demo" "ML")  ; obsolete