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