On Fri, 6 Apr 2012, Edward Z. Yang wrote:
I'm actually building a domain-specific frontend for Coq, and I didn't
feel like reimplementing all of ProofGeneral's parsing hacks! It's not
much: it's going to be a pedagogical theorem prover for first order
logic, but the idea is to closely support different deduction styles
(e.g. natural deduction, sequent calculus, etc.)
The "parsing hacks" are hacks as long as there is an attempt to define
that in a generic protocol. For example, Isabelle/Scala now lets the
prover do that reliably (either in ML or Scala). I have recently
discussed with some Coq insiders how to do the same specifically for Coq,
using existing Vernacular or CoqIde functionality.
Anyway, what is your front-end technology (also the programming language
platform for that)? Why are you using PGIP anyway?
Consider this tiny library to exchange algebraic datatypes between
different processes in a reasonably portable way:
https://bitbucket.org/makarius/yxml/overview
This is for OCaml and SML, in Isabelle/Scala there is a Scala version
already. The claim is that it can be ported to any reasonable programming
language in about 1 day (probably not Java).
Makarius
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
