On Fri, 6 Apr 2012, Edward Z. Yang wrote:

Excerpts from Makarius's message of Fri Apr 06 06:34:47 -0400 2012:
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.

If PGIP is obsolete I would love to know, then I will not spend any time learning it :-)

I don't think that PGIP was ever sufficiently established, so that it could be called obsolete now.

PGIP was an early attempt (around 2004) by David Aspinall and a few others to overcome raw TTY interaction with old-school proof assistants. The idea was to require provers to implement a more explicit model of interaction as explicit protocol. I have occasionally participated in PGIP design and implementation as Isabelle expert, but started to rethink the whole affair more seriously in 2007. In 2011/2012 the Isabelle/Scala infrastructure is sufficiently robust to support non-trivial applications, so I am no longer looking back towards PGIP.

David, are there still any users of PGIP/PGEclipse in Edinburgh? If not, we can really start to dismantle the PGIP implementation that is still in the Isabelle codebase.

ProofGeneral-devel mailing list

Reply via email to