coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Proof General and the XML protocol save you time and money!

From: "Paul A. Steckler" <steck AT stecksoft.com>
To: Coqdev <coqdev AT inria.fr>, coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Proof General and the XML protocol save you time and money!
Date: Thu, 15 Sep 2016 15:01:42 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=stecksoft AT gmail.com; spf=Pass smtp.mailfrom=stecksoft AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f169.google.com
Ironport-phdr: 9a23:WbSFehRKbfw2a5dBd+T+SnyeZ9psv+yvbD5Q0YIujvd0So/mwa64ZRCN2/xhgRfzUJnB7Loc0qyN4vmmBjFLuM/a+DBaKdoXCE9D0Z1X1yUbQ+e7SmTDZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5yO/inUtWK15f/hKiO/Mj4ZBxEiST1Nbh1NRm7sy3QsNMXiM1sMPB1ghDOuz5Df/lcjTdjIkvWlBLh7O+x+oRi+mJeoaRy2dRHVPCwR60lSfRxSnwdL20+58nmr1OLGRCT63Afen4KnxFLGA/L8FfxWZKn4XiyjfZ0xCTPZZ6+drszQzn3t6o=

Recently, I sent a message about my fork of Proof General that uses
coqtop's XML protocol.

I did not stress enough, perhaps, that the raison d'être for the fork
is to support the asynchronous processing of proofs introduced in Coq
8.5. With such processing, individual proofs within a script can be
run in parallel, which can considerably reduce the time needed to run
a script. And time is money, of course. :-)

This fork is likely the future of Proof General, so it would be good
to get as much feedback as possible. Github tells me that only a few
have cloned the repo; it would be great to see some more users.

Again, the repo is at:

https://github.com/psteckler/ProofGeneral

and the XML support is in the branch `server-protocol'. Instructions
are given in the file HOWTO-USE.

-- Paul

[Coq-Club] Proof General and the XML protocol save you time and money!, Paul A. Steckler, 09/15/2016