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.
Makarius
_______________________________________________
ProofGeneral-devel mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
