diff options
| -rw-r--r-- | acl2/README | 4 | ||||
| -rw-r--r-- | coq/README | 28 | ||||
| -rw-r--r-- | generic/README | 5 | ||||
| -rw-r--r-- | hol98/README | 5 | ||||
| -rw-r--r-- | isa/README | 12 | ||||
| -rw-r--r-- | isar/README | 12 | ||||
| -rw-r--r-- | lego/README | 15 | ||||
| -rw-r--r-- | phox/README | 4 | ||||
| -rw-r--r-- | plastic/README | 5 | ||||
| -rw-r--r-- | twelf/README | 5 |
10 files changed, 68 insertions, 27 deletions
diff --git a/acl2/README b/acl2/README index 1160bd91..fbe93440 100644 --- a/acl2/README +++ b/acl2/README @@ -2,8 +2,6 @@ ACL2 Proof General, for ACL2. Written by David Aspinall. -$Id$ - Status: alpha; unsupported Maintainer: volunteer required ACL2 version: Tested briefly with acl2.5 @@ -20,3 +18,5 @@ instantiation of Proof General. +$Id$ + @@ -4,20 +4,36 @@ Originally written by Healfdene Goguen. Later contributions by Patrick Loiseleur, Pierre Courtieu, David Aspinall -$Id$ - Status: supported Maintainer: Pierre Courtieu -Coq version: 6.3 +Coq version: 6.3, 6.3.1, 7.0 Coq homepage: http://pauillac.inria.fr/coq/assis-eng.html ======================================== -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. +Coq Proof General has experimental multiple file handling for 6.3 +versions. It does not have support for proof by pointing. There is support for X Symbol, but not using a proper token language. There is a tags program, coqtags. +======================================== + +Installation notes: + +Check the values of coq-tags and coq-prog-name in coq.el to see that +they correspond to the paths for coqtop and the library on your system. + +Install coqtags in a standard place or add <proof-home>/coq to your PATH. +NB: You may need to change the path to perl at the top of the file. + +If you are running Coq, generate a TAGS file for the library by running + coqtags `find . -name \*.v -print` +in the root directory of the library, $COQTOP/theories. If you are +running LEGO, do the same using legotags in the appropriate directory. + + +======================================== + +$Id$ diff --git a/generic/README b/generic/README index 2fcd56a3..f3c92262 100644 --- a/generic/README +++ b/generic/README @@ -1,7 +1,5 @@ Proof General -$Id$ - The code in this directory implements the generic basis of Proof General. @@ -12,3 +10,6 @@ Several other people helped with contributions and modifications, see individual credits in the code or summary in the Proof General manual. Contributions to the generic basis are welcome! + +$Id$ + diff --git a/hol98/README b/hol98/README index 40d35fc3..e6c3b4b3 100644 --- a/hol98/README +++ b/hol98/README @@ -2,8 +2,6 @@ HOL Proof General, for HOL98. Written by David Aspinall. -$Id$ - Status: not officially supported yet Maintainer: volunteer required HOL version: HOL98, tested with Taupo 2 @@ -50,3 +48,6 @@ 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$ + @@ -3,8 +3,6 @@ Isabelle Proof General Written by David Aspinall, later with assistance from Markus Wenzel and David von Oheimb. -$Id$ - Status: supported Maintainer: David Aspinall Isabelle version: 99-1, 99-2 @@ -25,4 +23,12 @@ There is no support for proof by pointing yet, and no tags program. The script `interface' and file 'interface-setup.el' are used to start Isabelle Proof General via the 'Isabelle' shell command. These files -were provided by Markus Wenzel. +were provided by Markus Wenzel. For `interface' you may need to +adjust the path to bash on the first line. + +Check the value of isabelle-prog-name. + +======================================== + +$Id$ + diff --git a/isar/README b/isar/README index 671d0920..e86950dc 100644 --- a/isar/README +++ b/isar/README @@ -2,8 +2,6 @@ Isabelle/Isar Proof General Written by Markus Wenzel -$Id$ - Status: supported Maintainer: Markus Wenzel Isabelle version: 99-1, 99-2 @@ -25,4 +23,12 @@ There is no support for proof by pointing yet, and no tags program. The script `interface' and file 'interface-setup.el' are used internally to start Isabelle Proof General via the 'Isabelle' shell command. This is the default way to invoke Proof General from the -Isabelle perspective. +Isabelle perspective. For `interface' you may need to adjust the path +to bash on the first line. + +Check the value of isabelle-prog-name. + +======================================== + +$Id$ + diff --git a/lego/README b/lego/README index 2ddd6fd1..0ecc9910 100644 --- a/lego/README +++ b/lego/README @@ -3,8 +3,6 @@ LEGO Proof General Written by Thomas Kleymann and Dilip Sequeira. Later maintainance by David Aspinall and Paul Callaghan. -$Id$ - Status: supported Maintainer: Paul Callaghan / David Aspinall LEGO version: 1.3.1 @@ -19,3 +17,16 @@ There is support for X Symbol, but not using a proper token language. There is a tags program, legotags. +======================================== + +Installation notes: + +Install legotags in a standard place or add <proofgeneral-home>/lego +to your PATH. +NB: You may need to change the path to perl at the top of the file. + + +======================================== + +$Id$ + diff --git a/phox/README b/phox/README index 9c955b84..06f20189 100644 --- a/phox/README +++ b/phox/README @@ -2,8 +2,6 @@ PhoX Proof General, for Phox. Written by Christophe Raffalli -$Id$ - Status: supported Maintainer: Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> PhoX version: 0.7 @@ -15,5 +13,5 @@ This mode has support for script management with PhoX, and some other features ported from PhoX's own Emacs mode. - +$Id$ diff --git a/plastic/README b/plastic/README index b96cd172..729b7530 100644 --- a/plastic/README +++ b/plastic/README @@ -2,11 +2,12 @@ Plastic Proof General Written by Paul Callaghan -$Id$ - Status: under development together with Plastic Maintainer: Paul Callaghan Plastic version: ?? Plastic homepage: http://www.dur.ac.uk/CARG/plastic.html ======================================== + +$Id$ + diff --git a/twelf/README b/twelf/README index 704545c4..2d91f558 100644 --- a/twelf/README +++ b/twelf/README @@ -2,8 +2,6 @@ Twelf Proof General, for Twelf. Written by David Aspinall. -$Id$ - Status: not officially supported yet Maintainer: volunteer required Twelf version: Twelf 1.2 (and later, I hope) @@ -24,3 +22,6 @@ doesn't work properly with font lock. I have written this in the hope that somebody from the Twelf community will adopt it, maintain and improve it, and thus turn it into a proper instantiation of Proof General. + +$Id$ + |