The Coq mailing list

["Paul A. Steckler" <steck AT stecksoft.com>]

I've created a fork of Proof General that uses the XML protocol in Coq
8.5 (and later, if you're using development versions). The main
advantage of the XML protocol is that it allows coqtop to process
proofs asynchronously, which is how CoqIDE is able to use that
feature.

We hope to release the code around the time 8.6 is released, or soon
thereafter. I'd like your help in testing out the code.

This is alpha-level code, so there will be bugs. There's been only
limited testing so far. I'm announcing the availability of this fork
here in order to get some more people trying out the code.

I mentioned this fork on the coq-dev mailing list a few weeks ago.
Since then, we've fixed a few significant bugs and also folded in the
latest fixes from the main PG repo.

Instructions on how to use the code appear below.

-- Paul

-------------------------------------------------------------------------------

How to try out Proof General with the coqtop XML protocol
-----------------------------------------------------------------------

1) Get the code from Github

The repo is at:

 https://github.com/psteckler/ProofGeneral

You should clone the repo via ssh or https.

2) Switch to the branch that supports the XML protocol

 $ git checkout server-protocol

3) In the ProofGeneral directory that was created via cloning:

 $ make

-----------------------------------------------------------------------------

You're probably already a Proof General user, so you'll want a way to
switch between the current distribution, and this experimental
version. Here's one way to do that on Linux, assuming you're running
bash as your shell.

In your .emacs file, add something like:

  (defun pg-xml ()
    (load-file "<path-to>/ProofGeneral/generic/proof-site.el")
    '(defun message (&rest s) nil))

And in your ~/.bashrc, add a line like:

  alias emacs-pg-xml="<path-to>/emacs -eval \"(pg-xml)\""

Run:

  $ source ~/.bashrc

Then, to run a Coq script foo.v:

  $ emacs-pg-xml foo.v

To run the current Proof General distribution, you can setup another
.emacs load function and bash alias:

  (defun pg ()
    (load-file "<path-to>/ProofGeneral/generic/proof-site.el"))

  alias emacs-pg="<path-to>/emacs -eval \"(pg)\""

The Proof General code is still experimental, and prints a lot of
debug messages, which may be annoying. To get rid of those, you can
remove the quote from the "defun" above (although you'll lose the
information provided by those messages).

Please note, this code is of alpha quality.

If you discover a bug, please work out the steps to reproduce
it. There's a transcript of the traffic between Emacs and coqtop in
the buffer *coq-log*, which may be helpful. Please create a new
issue in the Github repo above (not in the standard PG repo).

Thanks for trying out the code!