-Here is the latest pre-release of Proof General. For developers, -it is also available as a complete archive, including -forthcoming support for more proof assistants. -
-Pre-releases of Proof General may be buggy as we add new features and
-experiment with them. Nonetheless, we welcome bug reports. But
-please make sure you are using the current pre-release before
-reporting problems.
+Proof General follows an open development method.
+
+We welcome code contributions, suggestions, and bug reports, from all
+users and hackers!
-Check the - - file - -for a summary of changes since the last stable version, and -the planned changes to come. -
-This archive is a snapshot from our CVS repository. -
-What's the difference from the working version above? -The complete archive also includes: -
-Note: there are no pre-built documentation files in the developer's -release, because developers should have the right tools! -
--You probably don't need to download this if you're only -interested in hacking the Emacs lisp part of the program for -a prover that is currently supported. But you may -still like to check the latest - -. - -
+We have a mailing list for developers, at @@ -108,12 +43,8 @@ with the words "subscribe proofgeneral-devel"
-If you are interested in developing the core of Proof General, -we can make our CVS repository accessible to you. Please -ask. +If you are interested in becoming an official developer of Proof +General, we can make our CVS repository accessible to you. Please +ask here.
- diff --git a/html/develdownload.phtml b/html/develdownload.phtml new file mode 100644 index 00000000..b6527a50 --- /dev/null +++ b/html/develdownload.phtml @@ -0,0 +1,101 @@ + + ++Here is the latest pre-release of Proof General, made available +for those who wish to test the latest features or bug fixes. +For developers, this release is also available as a complete archive, +including forthcoming support for more proof assistants. +
++Pre-releases of Proof General may be buggy as we add new features and +experiment with them. Nonetheless, we welcome bug reports. But +please make sure you are using the current pre-release before +reporting problems. +
+ + ++Check the + + file + +for a summary of changes since the last stable version, and +the planned changes to come. +
++This archive is a snapshot from our CVS repository. +
++What's the difference from the working version above? +The complete archive also includes: +
++Note: there are no pre-built documentation files in the developer's +release, because developers should have the right tools! +
++You probably don't need to download this if you're only +interested in hacking the Emacs lisp part of the program for +a prover that is currently supported. But you may +still like to check the latest + +. + +
+ + diff --git a/html/download.phtml b/html/download.phtml index 22e3fe45..49a4c025 100644 --- a/html/download.phtml +++ b/html/download.phtml @@ -27,7 +27,7 @@ Proof GeneralDevelopers and beta-testers may like to download -a development release +a development release of Proof General.
@@ -81,6 +81,8 @@ Proof General:
For displaying logical and mathematical symbols, the excellent
X-Symbol
package.
+
It's very easy to install. See here
+for installation notes.
X-Symbol presently only works with XEmacs.
To use Proof General, simply unpack the sources with
@@ -189,3 +193,21 @@ any problems, suggestions, or patches.
+
+
+
+Contrary to what you may expect from the documentation of +X-Symbol, it's very easy to install and configures itself +automatically. +
++Simply download the binary package file, and do something +like this to install in your home directory: +
++ mkdir -p ~/.xemacsdiff --git a/html/features.phtml b/html/features.phtml index 63426bf6..c2c6dc89 100644 --- a/html/features.phtml +++ b/html/features.phtml @@ -1,5 +1,3 @@ - -
+ cd ~/.xemacs
+ tar xzf ../x-symbol-pkg.tar.gz
+
It doesn't matter if you're an Emacs militant or a pacifist!
diff --git a/html/header.phtml b/html/header.phtml index 0415a7b9..3cdc722c 100644 --- a/html/header.phtml +++ b/html/header.phtml @@ -24,6 +24,7 @@ "Features" => "features", "Download" => "download", "Documentation" => "doc", + "Development" => "devel", "About" => "about", "Links" => "links" ); diff --git a/html/links.phtml b/html/links.phtml index 5a85c3a6..08c4df2b 100644 --- a/html/links.phtml +++ b/html/links.phtml @@ -31,8 +31,45 @@ for links to include here, or find broken links, please ++There is now a new +. +I plan to apply for funding to continue managing the evolution +and development of Proof General, once my own job position +is more secure. Now is the time to flesh out ideas +for the future! Check the development page for the +latest proposals. +
+Countdown to Proof General 3.1 begins. This will be a bug fix releaase. A few bugs have been fixed in recent Proof General development releases, one important one is fixing support for non-mule versions of FSF Emacs (thanks to Pierre Courtieu for raising it to my attention). I would like to release PG 3.1 next month so that everyone can benefit. +
In the meantime, please that you would like to see fixed, and consider trying out the current development release. - -
I'm pleased to say that Proof General will be demonstrated at ETAPS 2000. @@ -29,7 +41,7 @@ the presentation A presentation of Proof General based on these slides was given at Rutherford Appleton Laboratory last week.
-Proof General 3.0 is released!
diff --git a/html/projects.phtml b/html/projects.phtml new file mode 100644 index 00000000..281c043d --- /dev/null +++ b/html/projects.phtml @@ -0,0 +1,90 @@ + + ++Here are some proposals for projects connected to Proof General. +
++The projects are designed as fairly self-contained contributions, +involving code development and possibly a small amount of supporting +research. They would be ideal projects for interested students +or researchers. +
+ ++Coq already has sophisticated notions of proof-by-pointing, +and old work on support for Proof General may be helpful. +We want to integrate with the latest version of Coq's +proof-by-pointing, possibly improving Proof General's +support along the way. +
++Skills: + Some understanding of Coq implementation, co-operation with + the Coq developers to get any Coq modifications (if any) incorporated. + Minimal Emacs Lisp knowledge. +
+Proposer: +David Aspinall. +
+ ++Isabelle has a sophisticated concrete syntax mechanism which makes it +difficult to add annotations to connect the displayed output back to +the internal abstract syntax. This issue needs to be solved to +support proof-by-pointing (and other features) in Isabelle. +A + +patch by Burkhart Wolff +providing term structure annotations for a previous release of +Isabelle may be useful here. To implement proof-by-pointing itself, +tactics using the gesture information must be written. +
++Skills: + Some understanding of Isabelle implementation, + co-operation with the Isabelle developers to get + Isabelle modifications incorporated. + Skill in writing Isabelle tactics. + Minimal Emacs Lisp knowledge. +
+Proposer: +David Aspinall. +
++If you are interested in working on any of these projects, +feel free to discuss with the project proposer or on the +. +
++Note: the proposer of the project is just that; he or she does not +guarantee to be available for formal supervision or intensive help +with the project. But it may be possible to find somebody else +to do that. Contact the project proposer first for more details. +
+ ++If you would like to submit a project proposal +for an improvement or extension of Proof General, +please send an email or write a description on the +. +Projects should be significant contributions rather than +incremental improvements (although we welcome the suggestion of those +too). +
+ + + -- cgit v1.2.3