[nongnu] elpa/proof-general 48bd86b 02/13: Remove HOL98 support

[ELPA Syncer]

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

    Remove HOL98 support
---
 Makefile              |   4 +-
 README.md             |   4 +-
 doc/ProofGeneral.texi |   6 +-
 generic/proof-site.el |   1 -
 hol98/README          |  53 ----------------
 hol98/example.sml     |  30 ---------
 hol98/hol98.el        | 170 --------------------------------------------------
 hol98/root2.sml       |  83 ------------------------
 8 files changed, 5 insertions(+), 346 deletions(-)

diff --git a/Makefile b/Makefile
index b51aaef..bda39cc 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 ccc coq easycrypt hol-light hol98 isar lego pghaskell pgocaml 
pgshell phox
+PROVERS=acl2 ccc coq easycrypt hol-light isar lego 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 hol98/*.sml isar/*.thy lclam/*.lcm lego/*.l 
pgshell/*.pgsh phox/*.phx plastic/*.lf
+DOC_EXAMPLES=acl2/*.acl2 isar/*.thy lclam/*.lcm lego/*.l 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 558a144..3ed9d29 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/) and
   [LEGO](http://www.dcs.ed.ac.uk/home/lego)
-* Experimental support of: CCC, ACL2, HOL98, Hol-Light, Lambda-Clam, Shell
+* Experimental support of: CCC, ACL2, Hol-Light, Lambda-Clam, Shell
 * Obsolete instances: Demoisa, Lambda-Clam, Plastic
-* Removed instances: Twelf
+* Removed instances: Twelf, HOL98
 
 A few example proofs are included in each prover subdirectory.
 
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 14bc95f..17dab48 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -209,7 +209,7 @@ other documentation, system downloads, etc.
 @cindex news
 
 The old code for the support of the following systems have been
-removed: Twelf.
+removed: Twelf, Hol98.
 
 @node News for Version 4.4
 @unnumberedsec News for Version 4.4
@@ -520,7 +520,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       HOL98         @tab @file{.sml}    @tab @code{hol98-mode}
 @item       HOL Light     @tab @file{.ml}     @tab @code{hol-light-mode}
 @item       ACL2          @tab @file{.acl2}   @tab @code{acl2-mode}
 @item       Plastic       @tab @file{.lf}     @tab @code{plastic-mode}
@@ -679,9 +678,6 @@ Isabelle for more details.
 @c @item
 @c @b{PhoX Proof General} for PhoX 0.8X@*
 @c @xref{PhoX Proof General}, for more details.
-@c @item
-@c @b{HOL Proof General} for HOL98 (HOL4)@*
-@c @xref{HOL Proof General}, for more details.
 @item
 @b{HOL Light Proof General} for HOL Light@*
 @xref{HOL Light Proof General}, for more details.
diff --git a/generic/proof-site.el b/generic/proof-site.el
index e6dd3e3..6e295ee 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -64,7 +64,6 @@
 
       ;; Incomplete/obsolete:
 
-      ;; (hol98        "HOL" "sml")
       ;; (acl2 "ACL2" "acl2")
       ;; (plastic "Plastic" "lf")        ; obsolete
       ;; (lclam "Lambda-CLAM" "lcm")     ; obsolete
diff --git a/hol98/README b/hol98/README
deleted file mode 100644
index 8462763..0000000
--- a/hol98/README
+++ /dev/null
@@ -1,53 +0,0 @@
-HOL Proof General, for HOL98.
-
-Written by David Aspinall.
-
-Status:              not officially supported yet
-Maintainer:   volunteer required
-HOL version:  HOL4/HOL98, tested with HOL 4 Kananaskis 2
-HOL homepage: http://hol.sourceforge.net
-
-========================================
-
-
-This is a "technology demonstration" of Proof General for HOL4.
-
-It may work with other versions of HOL, but is untested (please let me
-know if you try).  Probably just a few settings need changing to
-configure for different output formats.
-
-It has basic script management support, with a little bit of
-decoration of scripts and output.
-
-There is support for X Symbol, but not using a proper token language.
-
-I have written this in the hope that somebody from the HOL community
-will adopt it, maintain and improve it, and thus turn it into a proper
-instantiation of Proof General.
-
-
-------------
-
-Notes:
-
-There are some problems at the moment.  HOL proof scripts often use
-batch-oriented single step tactic proofs, but Proof General does not
-offer an easy way to edit these kind of proofs.  The "Boomburg-HOL"
-Emacs interface by Koichi Takahashi and Masima Hagiya addressed this,
-and to some extent so perhaps does the Emacs interface supplied with
-HOL.  Perhaps one of these could be embedded/reimplemented inside
-Proof General.  Implemented in a generic way, managing batch vs
-interactive proofs might also be useful for other provers.
-
-Another problem is that HOL scripts sometimes use SML structures,
-which can cause confusion because Proof General does not really parse
-SML, it just looks for semicolons.  This could be improved by taking a
-better parser (e.g. from sml mode).
-
-These improvements would be worthwhile contributions to Proof General
-and also provide the HOL community with a nice front end.  
-Please have a go!
-
-
-$Id$
-
diff --git a/hol98/example.sml b/hol98/example.sml
deleted file mode 100644
index 7e008eb..0000000
--- a/hol98/example.sml
+++ /dev/null
@@ -1,30 +0,0 @@
-(*
-    Example proof script for HOL Proof General.
-
-    $Id$
-*)    
-
-g `A /\ B ==> B /\ A`;
-e DISCH_TAC;
-e CONJ_TAC;
-e (IMP_RES_TAC AND_INTRO_THM);
-e (IMP_RES_TAC AND_INTRO_THM);
-val and_comms = pg_top_thm_and_drop();
-
-(* Hints about HOL Proof General:
- 
-   Proof General needs to work with top-level declarations throughout,
-   and with "interactive" rather than "batch" versions of proofs.
-
-   For best results, theorems should be saved in the way that they are
-   saved above, with pg_top_thm_and_drop.  The function isn't
-   mysterious, it is defined as:
-
-    fun pg_top_thm_and_drop () = let val t = top_thm(); in (drop(); t) end;
-*)
-
-(* this simple proof is not quite like proofs in the other systems,
-   can anyone tell me a more similar proof in HOL? I want to split 
-   the IMP_RES_TAC into two steps.  
-*)
-
diff --git a/hol98/hol98.el b/hol98/hol98.el
deleted file mode 100644
index 6f89707..0000000
--- a/hol98/hol98.el
+++ /dev/null
@@ -1,170 +0,0 @@
-;;; hol98.el --- Basic Proof General instance for HOL 98
-
-;; This file is part of Proof General.
-
-;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014  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
-
-;; 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
-
-(defvar hol98-keywords nil)
-(defvar hol98-rules nil)
-(defvar hol98-tactics nil)
-(defvar hol98-tacticals nil)
-
-(proof-easy-config  'hol98 "HOL"
- proof-prog-name                "hol.unquote"
- proof-terminal-string             ";"
- proof-script-comment-start             "(*"
- proof-script-comment-end               "*)"
- ;; These are all approximations, of course.
- proof-goal-command-regexp     "^g[ `]"
- proof-save-command-regexp     "pg_top_thm_and_drop"
- proof-goal-with-hole-regexp   "val \\(\\([^ \t=]*\\)\\)[ \t]*=[ \t]*prove"
- proof-save-with-hole-regexp   "val \\(\\([^ \t=]*\\)\\)[ \t]*=[ \t]*top_thm()"
- proof-non-undoables-regexp      "b()" ; and others..
- proof-goal-command              "g `%s`;"
- proof-save-command              "val %s = pg_top_thm_and_drop();"
- proof-kill-goal-command         "drop();"
- proof-showproof-command         "p()"
- proof-undo-n-times-cmd          "(pg_repeat backup %s; p());"
- proof-auto-multiple-files       t
- proof-shell-cd-cmd              "FileSys.chDir \"%s\""
- proof-shell-filename-escapes    '(("\\\\" . "\\\\") ("\""   . "\\\""))
- proof-shell-interrupt-regexp    "Interrupted"
- proof-shell-start-goals-regexp
- (proof-regexp-alt "Proof manager status"
-                  "OK.."
-                  "val it =\n")
- proof-shell-end-goals-regexp
- (proof-regexp-alt "^[ \t]*: GoalstackPure.goalstack"
-                  "^[ \t]*: GoalstackPure.proofs")
- proof-shell-quit-cmd            "quit();"
- proof-assistant-home-page
- "http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html";
- proof-shell-annotated-prompt-regexp
- "^- "
- ;; This one is nice but less reliable, I think.
- ;; "\\(> val it = () : unit\n\\)?- "
- proof-shell-error-regexp "^! "
- proof-shell-init-cmd
- "Help.displayLines:=3000;
-  fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));
-  fun pg_top_thm_and_drop () = let val t = top_thm(); in (drop(); t) end;"
- ;; FIXME: add optional help topic parameter to help command.
- proof-info-command                "help \"hol\""
- proof-shell-proof-completed-regexp "Initial goal proved"
- ;; FIXME: next one needs setting so that "urgent" messages are displayed
- ;; eagerly from HOL.
- ;; proof-shell-eager-annotation-start
- proof-find-theorems-command   "DB.match [] (%s);"
-
- proof-forget-id-command       ";" ;; vacuous: but empty string doesn't give
-                                   ;; new prompt
- ;; We must force this to use ptys since mosml doesn't flush its output
- ;; (on Linux, presumably on Solaris too).
- proof-shell-process-connection-type t
-
- ;;
- ;; Syntax table entries for proof scripts
- ;;
- proof-script-syntax-table-entries
- '(?\` "\""
-   ?\$ "."
-   ?\/ "."
-   ?\\ "."
-   ?+  "."
-   ?-  "."
-   ?=  "."
-   ?%  "."
-   ?<  "."
-   ?>  "."
-   ?\& "."
-   ?.  "w"
-   ?_  "w"
-   ?\' "w"
-   ?\| "."
-   ?\* ". 23"
-   ?\( "()1"
-   ?\) ")(4")
-
- ;;
- ;; A few of the vast variety of keywords, tactics, tacticals,
- ;; for decorating proof scripts.
- ;;
- ;; In the future, PG will use a mechanism for passing identifier
- ;; lists like this from the proof assistant, we don't really
- ;; want to duplicate the information here!
- ;;
- hol98-keywords  '("g" "expand" "e" "val" "store_thm" "top_thm" "by"
-                  "pg_top_thm_and_drop"
-                  "Define" "xDefine" "Hol_defn"
-                  "Induct" "Cases" "Cases_on" "Induct_on"
-                  "std_ss" "arith_ss" "list_ss"
-                  "define_type")
- hol98-rules    '("ASSUME" "REFL" "BETA_CONV" "SUBST"
-                  "ABS" "INST_TYPE" "DISCH" "MP"
-                  "T_DEF" "FORALL_DEF" "AND_DEF" "OR_DEF" "F_DEF"
-                  "NOT_DEF" "EXISTS_UNIQUE_DEF" "BOOL_CASES_AX"
-                  "IMP_ANTISYM_AX" "ETA_AX" "SELECT_AX" "ONE_ONE_DEF"
-                  "ONTO_DEF" "INFINITY_AX" "LET_DEF" "COND_DEF" "ARB_DEF")
- hol98-tactics   '("ACCEPT_TAC" "ASSUME_TAC" "GEN_TAC"
-                  "CONJ_TAC" "DISCH_TAC" "STRIP_TAC"
-                  "SUBST_TAC" "ASM_CASES_TAC" "DISJ_CASES_TAC"
-                  "REWRITE_TAC" "IMP_RES_TAC" "ALL_TAC" "NO_TAC"
-                  "EQ_TAC" "EXISTS_TAC" "INDUCT_TAC"
-                  "POP_ASM" "SUBST1_TAC" "ASSUM_LIST"
-                  "PROVE" "PROVE_TAC" "DECIDE" "DECIDE_TAC" "RW_TAC"
-                  "STP_TAC" "ZAP_TAC"
-                  "EXISTS_TAC")
- hol98-tacticals '("ORELSE" "FIRST" "CHANGED_TAC" "THEN"
-                  "THENL" "EVERY" "REPEAT"
-                  "MAP_EVERY")
- proof-script-font-lock-keywords
- (list
-  (cons (proof-ids-to-regexp hol98-keywords) 'font-lock-keyword-face)
-  (cons (proof-ids-to-regexp hol98-tactics) 'font-lock-keyword-face)
-  ; (cons (proof-ids-to-regexp hol98-rules) 'font-lock-keyword-face)
-  (cons (proof-ids-to-regexp hol98-tacticals) 'proof-tacticals-name-face))
-
- ;;
- ;; Some decoration of the goals output
- ;;
- proof-goals-font-lock-keywords
- (list
-  (cons (proof-ids-to-regexp '("Proof manager status"
-                              "proof" "Incomplete"
-                              "Initial goal proved"
-                              "Initial goal"
-                              "There are currently no proofs"
-                              "OK"))
-       'font-lock-keyword-face)
-  (cons (regexp-quote "------------------------------------")
-       'font-lock-comment-face)
-  (cons ": GoalstackPure.goalstack" 'proof-boring-face)
-  (cons ": GoalstackPure.proofs"    'proof-boring-face)
-  (cons ": Thm.thm"                'proof-boring-face)
-  (cons "val it ="                 'proof-boring-face))
-
- ;; End of easy config.
- )
-
-
-(warn "Hol Proof General is incomplete!  Please help improve it!
-Read the manual, make improvements and send them to 
da+pg-feedback@inf.ed.ac.uk")
-
-(provide 'hol98)
diff --git a/hol98/root2.sml b/hol98/root2.sml
deleted file mode 100644
index 0644fc3..0000000
--- a/hol98/root2.sml
+++ /dev/null
@@ -1,83 +0,0 @@
-(* Example proof by Konrad Slind.  See http://www.cs.kun.nl/~freek/comparison/ 
-   Taken from HOL4 distribution hol98/examples/root2.sml *)
-
-(*---------------------------------------------------------------------------*)
-(* Challenge from Freek Wiedijk: the square root of two is not rational.     *)
-(* I've adapted a proof in HOL Light by John Harrison.                       *)
-(*---------------------------------------------------------------------------*)
- 
-load "transcTheory";   open arithmeticTheory BasicProvers;
-
-(*---------------------------------------------------------------------------*)
-(* Need a predicate on reals that picks out the rational ones                *)
-(*---------------------------------------------------------------------------*)
-
-val Rational_def = Define `Rational r = ?p q. ~(q=0) /\ (abs(r) = &p / &q)`;
-
-(*---------------------------------------------------------------------------*)
-(* Trivial lemmas                                                            *)
-(*---------------------------------------------------------------------------*)
-
-val EXP_2 = Q.prove(`!n:num. n**2 = n*n`,
-  REWRITE_TAC [TWO,ONE,EXP] THEN RW_TAC arith_ss []);
-
-val EXP2_LEM = Q.prove(`!x y:num. ((2*x)**2 = 2*(y**2)) = (2*(x**2) = y**2)`,
- REWRITE_TAC [TWO,EXP_2]
- THEN PROVE_TAC [MULT_MONO_EQ,MULT_ASSOC,MULT_SYM]);
-
-(*---------------------------------------------------------------------------*)
-(* Lemma: squares are not doublings of squares, except trivially.            *)
-(*---------------------------------------------------------------------------*)
-
-val lemma = Q.prove
-(`!m n. (m**2 = 2 * n**2) ==> (m=0) /\ (n=0)`,
- completeInduct_on `m` THEN NTAC 2 STRIP_TAC THEN
-  `?k. m = 2*k`      by PROVE_TAC[EVEN_DOUBLE,EXP_2,EVEN_MULT,EVEN_EXISTS] 
-                     THEN VAR_EQ_TAC THEN
-  `?p. n = 2*p`      by PROVE_TAC[EVEN_DOUBLE,EXP_2,EVEN_MULT,
-                                  EVEN_EXISTS,EXP2_LEM] 
-                     THEN VAR_EQ_TAC THEN
-  `k**2 = 2*(p**2)`  by PROVE_TAC [EXP2_LEM] THEN
-  `(k=0) \/ k < 2*k` by numLib.ARITH_TAC
- THENL [FULL_SIMP_TAC arith_ss [EXP_2],
-        PROVE_TAC [MULT_EQ_0, DECIDE (Term `~(2 = 0n)`)]]);
-
-(*---------------------------------------------------------------------------*)
-(* The proof moves the problem from R to N, then uses lemma                  *)
-(*---------------------------------------------------------------------------*)
-
-local open realTheory transcTheory
-in
-val SQRT_2_IRRATIONAL = Q.prove
-(`~Rational (sqrt 2r)`,
- RW_TAC std_ss [Rational_def,abs,SQRT_POS_LE,REAL_POS]
-  THEN Cases_on `q = 0` THEN ASM_REWRITE_TAC []
-  THEN SPOSE_NOT_THEN (MP_TAC o Q.AP_TERM `\x. x pow 2`)
-  THEN RW_TAC arith_ss [SQRT_POW_2, REAL_POS, REAL_POW_DIV,
-                        REAL_EQ_RDIV_EQ,REAL_LT, REAL_POW_LT]
-  THEN REWRITE_TAC [REAL_OF_NUM_POW, REAL_MUL, REAL_INJ]
-  THEN PROVE_TAC [lemma])
-end;
-
-(*---------------------------------------------------------------------------*)
-(* The following is a bit more declarative                                   *)
-(*---------------------------------------------------------------------------*)
-
-infix THEN1;
-fun ie q tac = Q_TAC SUFF_TAC q THEN1 tac;
-
-local open realTheory transcTheory
-in
-val SQRT_2_IRRATIONAL = Q.prove
-(`~Rational (sqrt 2r)`,
- ie `!p q. ~(q=0) ==> ~(sqrt 2 = & p / & q)` 
-             (RW_TAC std_ss [Rational_def,abs,SQRT_POS_LE,REAL_POS] 
-               THEN PROVE_TAC[]) THEN RW_TAC std_ss [] THEN
- ie `~(sqrt 2 = & p / & q)` (PROVE_TAC []) THEN 
- ie `~(2 * q**2 = p**2)` 
-             (DISCH_TAC THEN SPOSE_NOT_THEN (MP_TAC o Q.AP_TERM `\x. x pow 2`) 
-              THEN RW_TAC arith_ss [SQRT_POW_2,REAL_POS,
-                          REAL_POW_DIV,REAL_EQ_RDIV_EQ,REAL_LT, REAL_POW_LT] 
-              THEN ASM_REWRITE_TAC [REAL_OF_NUM_POW, REAL_MUL,REAL_INJ])
-  THEN PROVE_TAC [lemma])
-end;