Walkthrough uses Isabelle when Isabelle 2015 and newer don't work

[talwrii]

Proof general does not work with new version of Isabelle:

• https://github.com/ProofGeneral/PG/issues/186
• https://github.com/ProofGeneral/PG/issues/66
• http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2015/000352.html

And yet the documentation walkthrough is for Isabelle (also: https://proofgeneral.github.io/doc/userman/ProofGeneral_3/#Basic-Script-Management)

Is this a good idea from the point of view of encouraging adoption?

[Matafou]

Indeed PG support for isabelle has been discontinued for some years now.

We are in eht process of focusing next version of PG on Coq only. We will need to also focus the documentation.

[andreas-roehler]

Hi, I'm volunteering for this part. Please assign me if interested.

[Matafou]

Thanks, please proceed! That said the adaptability of PG to new provers is not our priority currently. We rather would like to adapt PG to modern asynchronous interaction protocols first. And then maybe provide a generic interface again. But the vanilla PG may stay around for while before we can do that. So I think this is worth updating the documentation if you have time. Which prover will us use as an example?

[andreas-roehler]

Am 06.07.20 um 16:34 schrieb Pierre Courtieu:

Thanks, please proceed! That said the adaptability of PG to new provers is not our priority currently. We rather would like to adapt PG to modern asynchronous interaction protocols first. And then maybe provide a generic interface again.

Sounds reasonable.

But the vanilla PG may stay around for while before we can do that. So I think this is worth updating the documentation if you have time. Which prover will us use as an example?

Would remove all the broken references first.

As for example-code, would take Coq, which is known to work AFAIU. As this might take time, maybe replace some broken parts with a TBD?

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/ProofGeneral/PG/issues/218#issuecomment-654276234, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAI6NEZO46VBHOX3IBRPIRDR2HOFRANCNFSM4EH6ZNZQ.

[solna86]

I note the master branch still includes a directory full of Isabelle code, and generated docs do talk about Isabelle support.

Is Isabelle support definitely discontinued? That's pretty sad as their jEdit default IDE is a bit clunky compared to Emacs.

[hendriktews]

solna86 [email protected] writes:

Is Isabelle support definitely discontinued? That's pretty sad as their jEdit default IDE is a bit clunky compared to Emacs.

For years, maybe even a decade, nobody turned up to maintain Proof General for Isabelle. To me, this seems to indicate that the majority of Isabelle users are quite happy with jedit.

Hendrik

[andreas-roehler]

Can't see why Isabelle should not work from Emacs. Should be worth looking into again.

https://isabelle.in.tum.de/Isar/ still writes:

Together with the Isabelle/Isar instantiation of Proof General, a generic (X)Emacs interface for interactive proof assistants, we arrive at a reasonable environment for live proof document editing.

[hendriktews]

I doubt it is worth, given that most Isabelle users seem to be happy with jedit.

The people currently contributing to Proof General are mostly Coq users. They don't have the knowledge or motivation to work on Isabelle. Therefore, IMO, we should remove the Isabelle code together with other unused stuff (eg, obsolete, phox, pgocaml, pghaskell). The code won't be lost - this is git, you can always resurrect it.

If you would like to get Proof General/Isabelle working again, pull requests are certainly welcome!

[erikmd]

Hello, I fully agree with @hendriktews, all the more as the current protocol supported by Isabelle >2015 and by PG.master are strongly different (PIDE vs. REPL). So a "direct" update of the current PG.isabelle codebase is not feasible actually.

Therefore, IMO, we should remove the Isabelle code together with other unused stuff (eg, obsolete, phox, pgocaml, pghaskell). The code won't be lost - this is git, you can always resurrect it.

Yes: this cleanup had already be done in the async branch (a bit too aggressively as phox and easycrypt should have been kept in particular). But IMO this makes sense to do this cleanup in the master branch as well, including documentation, removing everything that is not distributed through MELPA: https://github.com/melpa/melpa/blob/master/recipes/proof-general#L7-L9

@hendriktews do you want to open one such cleanup PR in the upcoming days? or tell me if you prefer that I have a look.

Anyway, once support for async proofs (as opposed to REPL) will be fully OK for Coq, I guess it would be easier to re-add support for Isabelle.

[solna86]

Thanks. My initial comment about Isabelle support was not intended to raise any controversy. I was just confused because PG's current master docs referred to Isabelle, yet this was supposedly discontinued a few years ago.

I totally agree with PG focusing on Coq if that's where most users come from and supporting Isabelle is a lot of effort as it is significantly different.

Perhaps for Isabelle it'd be easier to extract all jEdit-independent code to a Language Server Protocol backend.

[hendriktews]

Erik Martin-Dorel [email protected] writes:

@hendriktews do you want to open one such cleanup PR in the upcoming days? or tell me if you prefer that I have a look.

I would appreciate, if you would take a look. Thanks!

[erikmd]

Hi @hendriktews, OK thanks for your reply; so I add this in my backlog.

[andreas-roehler]

Fine for me too, let's stay tuned.