> 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.
I don't quite understand.
> Anyway, what is your front-end technology (also the programming language
> platform for that)? Why are you using PGIP anyway?
Uh, it's a bit of an unholy soup of all the languages (right now we're doing
Haskell and Urweb, but I'm very happy to drop/add languages as necessary).
I'm using PGIP because Coq doesn't have any machine-interchangeable
formats for it's prover process, and the logical format to use
if I'm adding this format is PGIP; if people consider it the "right
thing" it's probably more likely to get accepted than some random
scheme I personally cook up.
But it seems there is some disagreement here.
> Consider this tiny library to exchange algebraic datatypes between
> different processes in a reasonably portable way:
> 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).
Yes, this is another approach that we have considered. Actually, in this case
I would have wanted to cut out the middleman, lib-ified Coq and just run 'open
Coq' and directly do this (this may be worth doing anyway, independent of this
conversation, although I don't have infinite time).
The main problem with this approach is that the internal representation
of Coq (and any compiler really) is rather specialized, and not
necessarily what anyone expects to interact with. Furthermore,
it means your code now is tightly coupled to Coq, which is annoying
if the representation ever changes. None of these are unsurmountable
difficulties, but it certainly made go for a less coupled approach first.
ProofGeneral-devel mailing list