search

ProofGeneral / PG

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

Merging the Abella fork of PG #701

Open phikal opened 1 year ago

phikal commented 1 year ago

The Abella proof assistant has been maintaining a fork of Proof General for a while now, even though looking at the diff, the two don't seem that irreconcilable. Even though the upstream development appears to acknowledge that their fork back into PG would be convenient, the main developer (Kaustuv Chaudhuri) appears to believe that the PG maintainers wouldn't be interested:

I think PG's devs don't want to maintain modes for niche systems, so they will probably not accept Abella's fork.

Could someone say if this is the case, or if given a working pull request, merging support for Abella would be something could conceivably be added to Proof General?

Btw, I have contacted Kaustuv (@chaudhuri on GH), but have yet not received any response from his end.

chaudhuri commented 1 year ago

If anything, I think the onus is on Abella to provide a suitable PR for PG if indeed Abella thinks it is reasonable to have default support for it in PG.

If possible, I would like the PG devs to recommend a way for a third party to add a PG minor mode without needing to modify PG's proof-site.el or add code to particular subdirectories in PG.

monnier commented 1 year ago

If possible, I would like the PG devs to recommend a way for a third party to add a PG minor mode without needing to modify PG's proof-site.el or add code to particular subdirectories in PG.

AFAIK, the current PG code is not sufficiently modular for that, sadly :-(

phikal commented 1 year ago

monnier @.***> writes:

If possible, I would like the PG devs to recommend a way for a third party to add a PG minor mode without needing to modify PG's proof-site.el or add code to particular subdirectories in PG.

AFAIK, the current PG code is not sufficiently modular for that, sadly :-(

I'll have some more spare time soon, do you think it would be a manageable effort to try and address this?

-- Philip Kaludercic

erikmd commented 1 year ago

Thanks @phikal for opening this issue!

@chaudhuri

If anything, I think the onus is on Abella to provide a suitable PR for PG if indeed Abella thinks it is reasonable to have default support for it in PG.

During the summer, we don't meet up with my fellow colleagues @Matafou and @hendriktews, so I cannot speak from the team.

Still, IMHO I don't believe there would be some objection for merging support for another prover such as Abella.

Anyway, I think it would be much more easy if a member of the Abella community is motivated to help maintaining the Abella flavor in PG after the merge; by this I don't mean maintaining all the layers of PG! but being available to handle Abella-related issues/PRs — given we co-maintain PG essentially as part of our spare time, and we are not necessarily savvy in Abella.

If possible, I would like the PG devs to recommend a way for a third party to add a PG minor mode without needing to modify PG's proof-site.el or add code to particular subdirectories in PG.

I don't think this is required (or urgent) to do this: even if it is a sensible idea from a software engineering POV, we don't add so often support for new provers in PG! so adding a subdirectory and an entry in proof-site.el is fine. The only "boring" step is to update the MELPA and NonGNU ELPA configuration to mention the additional subdirectory.

BTW, feel free to take a look at the PR https://github.com/ProofGeneral/PG/pull/636 to get a fairly recent example of proof-assistant addition in PG.

Best wishes

phikal commented 1 year ago

The only "boring" step is to update the MELPA and NonGNU ELPA configuration to mention the additional subdirectory.

FWIW there is no need to change anything for NonGNU ELPA, it already bundles everything with the exception of two files.

phikal commented 10 months ago

ping?

Matafou commented 10 months ago

Hi. We welcome such contributions! Of course the maintenance of this code remains yours. We generally proceed by PR. I would recommend (although this is not a prerequisite) that you write a few tests (see the ci directory) in order to be warned early if something important breaks (scripting basic proofs, goal and error display).

Matafou commented 10 months ago

But an immediate PR of your current fork would be welcome. Please be patient we will look at it when we have time (we all do this in our spare time).

chaudhuri commented 10 months ago

Thanks for the encouraging comments. I will see if a suitable PR can be created from my existing Abella-specific fork.

phikal commented 4 months ago

Ping?

erikmd commented 2 months ago

Hi @chaudhuri @phikal,

as said earlier, a new PR (that could take inspiration from https://github.com/ProofGeneral/PG/pull/636) adding Abella support in PG would be welcome. We'd give you feedback within one such PR.

AFAIAC, my spare time (and thereby PR review time) is very limited currently, but I still support your contribution proposal!