Merging the Abella fork of PG

[phikal]

Merging the Abella fork of PG

[phikal]

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.

[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.

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]

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]

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]

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 #636 to get a fairly recent example of proof-assistant addition in PG.

Best wishes

[phikal]

ping?

[Matafou]

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]

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]

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

[phikal]

Ping?