search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
491 stars 89 forks source link

Support for agda, pml and similars #202

Open craff opened 7 years ago

craff commented 7 years ago

The only change in this kind of provers is that the buffer is not split in two (done / undone) parts, but many parts that are done or not done (goals). Then, commands have to mention the goal, or they should be a current goal ...

So I don't know if its is a so big change, but it has a lot of potential applications.

Blaisorblade commented 7 years ago

FWIW, Agda has its own emacs mode with lots of Agda-specific support—not clear there's anything you'd want to share there.

craff commented 7 years ago

Yes and my PML prover has its own emacs mode ... But I would be still very happy to trow away more that half of the code and use PG.

craff commented 7 years ago

Moreover, here, there is a chicken and egg issue. I am sure users of Coq (and other provers) would be happy to work on many proof in parallel (in the same file). And support for this is more or less what you need for Agda or PML. And if it existed in PG, the Coq implementors might use it ... I would certainly give it a try for PhoX if I were still developing it.

Matafou commented 7 years ago

Hi,

Are you aware of the xml/pg branch? It is aimed to become the master branch soon. It uses coq's xml potocol which is made more or less for something like you describe.

By the way once it becomes the master branch the legacy branch will be much less updated. Since nowadays it seems coq is the only prover significantly used with pg, we have currently no real plan for other provers. However once the SerAPI protocol (nextgen protocol) is implemented on the coq side and supported on pg's side it could become a generic protocol (in the line of pgip) that other provers might want to implement to be supported again by PG.

No hurry anyway since legacy branch will remain on github.

Best regards, P.