Prooftree updates #439
Prooftree updates #439
Conversation
|
Hi @hendriktews, what the status of this PR?
|
|
|
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
|
|
Thanks a lot @hendriktews for your detailed reply.
OK for me!
Thanks @hendriktews! but at first sight there is no hurry, unless some users request it soon…
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
force-pushed
the
prooftree-updates
branch
from
b565067 to
08e8644
Compare
|
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. |
hendriktews
force-pushed
the
prooftree-updates
branch
from
a2b0a89 to
6bbde7e
Compare
|
@hendriktews this seems to ne easy to rebase. Is there any reason not to? |
hendriktews
force-pushed
the
prooftree-updates
branch
from
6bbde7e to
d2f83e0
Compare
hendriktews
force-pushed
the
prooftree-updates
branch
2 times, most recently
from
479d319 to
c1c2711
Compare
|
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: although I had the opam package |
|
Thanks for testing.
I agree it is confusing, but it also printed This happens because I still support compilation without findlib, as it might happen, eg. on bullseye. There one needs I see if I can add some more messages. |
Yes.
No big deal. |
This is a major change, because the new Show Goal command in Coq 8.10 can print goals for previous states and therefore permits to remove all the code that was tracking goals and existential from PG and to rely on prooftree to request goals and goal updates. This change does break compatibility for the proof tree display for Coq 8.6 and before. (The old Coq versions themselves work, it's just that proof tree display won't work.) In paricular: - delete urgent proof tree actions, the hooks and all the corresponding code - delete sequent hash and existentials info and all the corresponding code - adopt prooftree regular expressions and show goal functions to Coq 8.10 (implemented in coq/coq#10489) - new hooks proof-tree-start-display-hook and proof-tree-stop-display-hook for switching Coq's dependent evar line on and off - forward the new show goal commands from prooftree to Coq - proof tree display starts with the Lemma command, because Proof does not display anything anymore - deleted superfluous proof tree code in hol-light and deconfigured prooftree for Hol-Light, IIRC, it was never working. But I am happy to provide support, if anybody wants to pick this up.
- send evar info for update sequent commands - update to protocol version 4 - fix starting prooftree inside a proof
The dependent evar line is now unconditionally switched on and off for proof tree displays. This is controlled by the new option `coq-proof-tree-manage-dependent-evar-line'.
Show goal does not increase the state number in Coq and should not be recognized as an undo command in proof-tree.el.
This commit solves the following problem: At the end of a proof with proof-tree display, a number of show goal requests from prooftree must possibly be processed, before prooftree sends the confirm-proof-complete message to signal that Proof General can continue. For Coq these show goal commands must be sent to Coq before the dependent evar line is switched off and the result must be processed by Proof General, therefore before `proof-tree-external-display' is switched off. Proof General must therefore stop processing the queue region after the command that finished the proof until all show goals are processed, the dependend evar line is off and `proof-tree-external-display' is nil again. This is achieved by only keeping the priority actions on proof-action-list and moving whatever remains to proof-tree--delayed-actions and setting proof-second-action-list-active. This way only priority actions (read show goal commands) are processed until prooftree signals completion and the stuff on proof-tree--delayed-actions is moved back. To implement this, I introduced (again) an urgent action (proof-tree-check-proof-finish), which checks for the end of the proof or the arrival of the last priority action connected with the current proof-tree display (tagged 'proof-tree-last-item and queued by the call back proof-tree-confirm-proof-complete).
Delete functions from PG-adapting that have been deleted in the sources to fix make magic. Delete also some of the outdated information of the Prooftree configuration section. Note that this section is still outdated, which is hopefully OK, given the number of attempts to add Prooftree support for more proof assistants in the last years.
This commit addresses all the points that have only been marked in the previous prooftree related commits.
Support Unshelve after all goals have been closed, which shall create a new layer with all the unshelved goals. Prooftree contains enough state to determine whether or not a new layer must be created. Therefore erase the regular expression to recognize commands that are expected to create a new layer. Also erase the new-layer flag from the current-goals display command. NOTE: This commit changes the Prooftree communication protocol. Use only with Prooftree containing a patch with the same header.
proof-second-action-list-active cannot be used by two packages (i.e., proof-tree and coq-par-compile) simultaneously. Therefore assert it is off when starting a proof-tree display. Also re-initialize proof-tree--delayed-actions, although it should always be reset at the end of a proof-tree display, if everything works as expected.
hendriktews
force-pushed
the
prooftree-updates
branch
from
b7c18a2 to
abac730
Compare
|
@hendriktews do we merge this? |
I would be in favor of merging sooner than later. |
|
I just released Prooftree 0.14. Merging this now. |
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.