Prooftree updates

[hendriktews]

This PR contains the work in progress for updating proof tree display support in PG. It should work with the upstream head of prooftree and Coq PR 10489. I strongly suggest to not merge this until after this Coq PR has been merged.

[erikmd]

Hi @hendriktews, what the status of this PR?

• In particular, I've just seen https://github.com/coq/coq/pull/10489 had been merged.
• But that PR 10489 is only integrated in Coq 8.11+, so will this fact hinder PG+prooftree support with Coq < 8.11?

[erikmd]

• On the other hand, coq/coq#10489 mentions it addressed issue coq/coq#10399, which did not seem to impact Coq <= 8.10
• Anyway you'll need to solve the merge conflict that arose meanwhile (e.g. with a git rebase?)

[hendriktews]

Erik Martin-Dorel [email protected] writes:

Hi @hendriktews, what the status of this PR?

It is work in progress. More precisely, it works mostly fine and I have used it already heavily. However, there are a number of bugs left in some edge cases that sometimes crash the proof tree display and sometimes only cause it to show incorrect information. I am still working on this and I have already more on my hard disk than what is currently visible in this PR. Let me know, if you want to have a look, then I make something available.

• In particular, I've just seen coq/coq#10489 had been merged.

Yes, and also coq/coq#10356. Both patches are present in Coq 8.11.

• But that PR 10489 is only integrated in Coq 8.11+, so will this fact hinder PG+prooftree support with Coq < 8.11?

Yes, but the main reason is PR 10356. For Coq >= 8.7 and < 8.11 prooftree is completely broken, because the variant of Show Goal that it relies on is missing in these Coq versions. Coq 8.4 and 8.5 work nicely and 8.6 works with a limited feature set. In general only certain combinations of Coq, Proof General and prooftree work together. Because there is no hope to fix prooftree for Coq 8.7 - 8.10 and nobody was ever complaining, I suggest to only support proof tree display for Coq >= 8.11 in the future. In fact, this PR removes a lot of code that is needed to run older versions of prooftree with Coq 8.5.

• On the other hand, coq/coq#10489 mentions it addressed issue coq/coq#10399, which did not seem to impact Coq <= 8.10

Yes, but coq/coq#10315 does.

• Anyway you'll need to solve the merge conflict that arose meanwhile (e.g. with a git rebase?)

Yes I know, I have introduced some conflicts myself and I have already resolved at least those locally.

If there is interest in trying proof tree visualization with Coq 8.11 with a few known bugs, then let me know and I will make something available. Otherwise I would slowly continue with the remaining bugs and also add documentation, before proposing to merge this PR.

Hendrik

[erikmd]

Thanks a lot @hendriktews for your detailed reply.

I suggest to only support proof tree display for Coq >= 8.11 in the future.

OK for me!

If there is interest in trying proof tree visualization with Coq 8.11 with a few known bugs, then let me know and I will make something available.

Thanks @hendriktews! but at first sight there is no hurry, unless some users request it soon…

Otherwise I would slowly continue with the remaining bugs and also add documentation, before proposing to merge this PR.

LGTM. − And at that time, you may also want to further document/advertise the feature? (e.g. by mentioning the proof-tree feature and installation instructions in https://proofgeneral.github.io/ and in Coq's discourse :)

[hendriktews]

Finally I solved the crashes and the other critical problems. Some minor problems are still present, but I believe they can be postponed until after merging this PR. This PR is in sync with the current version of Prooftree (hendriktews/proof-tree@7b18f01a6a6b09547a25ed464c2deb7f8a2f5481).

[Matafou]

@hendriktews this seems to ne easy to rebase. Is there any reason not to?

[hendriktews]

Hi @erikmd and @Matafou, IMO this PR is now ready for review. What remains is maybe some polishing of the prooftree repo and then a release there. Some of the commits are quite big, so I am not sure how the review could be done. Maybe you just try it out?

[Matafou]

Hi Hendrik. Seems to work like charm here (ocaml 4.14.1, coq 8.15.1).

One remark on compiling prooftree: configure.sh displays an error:

test ocamlopt.opt -I +lablgtk2
File "_none_", line 1:
Error: Cannot find file lablgtk.cmxa
test ocamlopt.opt -I /home/courtieu/.opam/coq-8.15/lib/lablgtk2

although I had the opam package lablgtk installed and the file /home/courtieu/.opam/coq-8.15/lib/lablgtk2/lablgtk2.cmxa does exist. And indeed doing make afterward succeeded. I am not sure why this happens but this is confusing.

[hendriktews]

Thanks for testing.

One remark on compiling prooftree: configure.sh displays an error:

I agree it is confusing, but it also printed Configuration successful at the end, didn't it?

This happens because I still support compilation without findlib, as it might happen, eg. on bullseye. There one needs -I +lablgtk2, but in your case on opam one would need -I +lablgtk2/lablgtk2. My configure script does a little bit trial-and-error, therefore you might see an error of the first failing trial.

I see if I can add some more messages.

[Matafou]

One remark on compiling prooftree: configure.sh displays an error: I agree it is confusing, but it also printed Configuration successful at the end, didn't it?

Yes.

This happens because I still support compilation without findlib, as it might happen, eg. on bullseye. There one needs -I +lablgtk2, but in your case on opam one would need -I +lablgtk2/lablgtk2. My configure script does a little bit trial-and-error, therefore you might see an error of the first failing trial.

I see if I can add some more messages.

No big deal.

[Matafou]

@hendriktews do we merge this?

[hendriktews]

@hendriktews do we merge this?

I would be in favor of merging sooner than later.

[hendriktews]

I just released Prooftree 0.14. Merging this now.