-
Notifications
You must be signed in to change notification settings - Fork 87
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Walkthrough uses Isabelle when Isabelle 2015 and newer don't work #218
Comments
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. |
Hi, I'm volunteering for this part. Please assign me if interested. |
Thanks, please proceed! |
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
<#218 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AAI6NEZO46VBHOX3IBRPIRDR2HOFRANCNFSM4EH6ZNZQ>.
|
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. |
solna86 <notifications@github.com> 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
|
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. |
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!
|
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.
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. |
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. |
Erik Martin-Dorel <notifications@github.com> 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!
|
Hi @hendriktews, OK thanks for your reply; so I add this in my backlog. |
Fine for me too, let's stay tuned. |
Proof general does not work with new version of Isabelle:
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?
The text was updated successfully, but these errors were encountered: