On Fri, 6 Apr 2012, David Aspinall wrote:

Interesting that you're trying this! Although I should warn that we haven't been actively developing the PGIP infrastructure for a while: which interface are you hoping to use it with?

In fact, I recently considering asking if it is now time to remove the PGIP stuff from the Isabelle sources.

More than 4 years of Isabelle/Scala there is sufficient infrastructure to make it obsolete, and the "flagship application" of Isabelle/jEdit is doing reasonably well.

Even more, some concrete work with the Coq people here in the Paris area has started, to make that prover somehow participate in the game.

At some point I would like to see more forces moving in the same direction. After classic Proof General, there has mainly been some Brownian motion so far.

ProofGeneral-devel mailing list

Reply via email to