Added README files for each prover, summarizing status.

6 files changed, 147 insertions, 0 deletions

diff --git a/coq/README b/coq/README
new file mode 100644
index 00000000..84ead4fc
--- /dev/null
+++ b/coq/README
@@ -0,0 +1,16 @@
+Coq Proof General
+
+Originally written by Healfdene Goguen.
+Later contributions by Patrick Loiseleur and Pierre Courtieu.
+
+$Id$
+
+Presently Coq Proof General supports automatic multiple file support
+only (deduced file dependencies, not communicated ones).  It does not
+have support for proof by pointing.
+
+There is support for x-symbols, but not using a proper token
+language.  Try writing "philosophy" !
+
+There is a tags program, coqtags.
+
diff --git a/demoisa/README b/demoisa/README
new file mode 100644
index 00000000..fe2b53d4
--- /dev/null
+++ b/demoisa/README
@@ -0,0 +1,47 @@
+Example Proof General instance for Isabelle
+
+Written by David Aspinall.
+
+$Id$
+
+		"Isabelle Proof General in 30 setqs"
+
+This is a whittled down version of Isabelle Proof General, supplied
+as an (almost) minimal demonstration of how to instantiate Proof
+General to a particular proof assistant.  You can use this as a
+template to get support for a new assistant going.
+
+This mode uses the unadulterated terminal interface of Isabelle, to
+demonstrate that hacking the proof assistant is not necessary to
+get basic features working.
+
+And it really works!  You you get a toolbar, menus, short-cut keys,
+script management for multiple files, a function menu, ability to
+run proof assistant remotely, etc, etc.
+
+To try it out, set in the shell PROOFGENERAL_ASSISTANTS=demoisa
+before invoking Emacs.  (Of course, you need Isabelle installed).
+
+What's missing? 
+
+ 1. A few handy commands (e.g. proof-find-theorems-command)
+ 2. Syntax settings and highlighting for proof scripts
+ 3. Indentation for proof scripts
+ 4. Special markup characters in output for robustness 
+ 5. True script management for multiple files (automatic mode is used)
+ 6. Proof by pointing
+
+How easy is it to add all that?
+
+ 1. Trivial.  2. A table specifying syntax codes for characters
+ (strings, brackets, etc) and some regexps; depends on complexity
+ of syntax.  3. A bit of elisp to scan script; depends on
+ complexity of syntax.  4. Needs hacking in the proof assistant:
+ how hard is to hack your assistant to do this?  5. Depends on file
+ management mechanism in the prover, may need hacking there to send
+ messages. But automatic multiple files may be all you need anyway.
+ 6. Non trivial (but worth a go).
+
+
+See demoisa.el and demoisa-easy.el for more details.
+
diff --git a/generic/README b/generic/README
new file mode 100644
index 00000000..828d76e5
--- /dev/null
+++ b/generic/README
@@ -0,0 +1,12 @@
+Proof General
+
+$Id$
+
+The code in this directory implements the generic basis 
+of Proof General.
+
+It was written by Thomas Kleymann, Dilip Sequeira, Heafldene Goguen,
+and David Aspinall.
+
+Several other people helped with contributions and modifications, see
+individual credits in the code or summary in the Proof General manual.
diff --git a/hol98/README b/hol98/README
new file mode 100644
index 00000000..38cbfe26
--- /dev/null
+++ b/hol98/README
@@ -0,0 +1,43 @@
+HOL Proof General, for HOL 98.
+
+Written by David Aspinall.
+
+$Id$
+
+This is a "technology demonstration" of Proof General for HOL 98.
+
+It may well work with other versions of HOL, but is untested (please
+let me know if you try).
+
+It has basic script management support, with a little bit of
+decoration of scripts and output.
+
+There is support for x-symbols, but not using a proper token language.
+Try writing "philosophy" !
+
+I have written this in the hope that somebody from the HOL community
+will adopt it and turn it into a proper instantiation of 
+Proof General.
+
+------------------
+
+Note:
+
+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" Emacs
+interface by Koichi Takahashi and Masima Hagiya addressed this, and to
+some extent so does the Emacs interface supplied with HOL.  Perhaps
+one of these could be embedded inside Proof General.  Implemented in
+a generic way, managing batch vs interactive proofs would also be
+useful for Isabelle.
+
+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.  Again, 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!
+
diff --git a/isa/README b/isa/README
new file mode 100644
index 00000000..766cc256
--- /dev/null
+++ b/isa/README
@@ -0,0 +1,14 @@
+Isabelle Proof General 
+
+Written by David Aspinall, later with assistance from
+Markus Wenzel and David von Oheimb.
+
+$Id$
+
+Isabelle Proof General has full support for multiple file scripting,
+with dependencies between theories communicated between Isabelle and
+Proof General.  It has a mode for editing theory files taken from
+Isamode.
+
+There is no support for proof by pointing yet.
+
diff --git a/lego/README b/lego/README
new file mode 100644
index 00000000..a8fa6850
--- /dev/null
+++ b/lego/README
@@ -0,0 +1,15 @@
+LEGO Proof General
+
+Written by Thomas Kleymann and  Dilip Sequeira.
+Later maintainance by David Aspinall and Paul Callaghan.
+
+$Id$
+
+LEGO Proof General has full support for multiple file scripting, and
+experimental support for proof by pointing.
+
+There is support for x-symbols, but not using a proper token
+language.  Try writing "philosophy" !
+
+There is a tags program, legotags.
+