Improve PG support of Show Proof Diffs

[CyrilAnac]

Close #487

[erikmd]

Thank you @CyrilAnac, I added several comments you could take into account till next meeting,
also it seems the current code make a CI test fail, maybe you can have a look as well (or we'll discuss this next week)

[CyrilAnac]

@erikmd The feature seems to work now, I'm waiting for an other review or merging approve.

[Matafou]

Seems good to me. github shows strang indentation, is it due to tab indent?

[Matafou]

General question: what will happen if we switch to the "always silent. Do Show when needed" described here #467 (comment)?
Same question for the "Show goal Diff" feature.

[erikmd]

Thanks @CyrilAnac ! the feature looks very nice.

However it seems the following bug is introduced:

(1) when opening a .v file

Lemma test : forall n : nat, n = n.
  reflexivity. (* (2) then doing "C-c C-RET" to here *)

(3) and finally doing "C-c C-u" to backtrack, we get:

condition-case: Wrong type argument: stringp, nil

− I'm using Coq 8.11.1 on GNU/Linux

[erikmd]

Hi @Matafou

General question: what will happen if we switch to the "always silent. Do Show when needed" described here #467 (comment)?
Same question for the "Show goal Diff" feature.

From my understanding the features are not incompatible but essentially orthogonal.

To summarize the situation:

• This PR Improve PG support of Show Proof Diffs #490 just amounts to append (if the corresponding option is enabled) a Show Proof… command at the end of the queue, typically after Show. if there is one, or just in the queue alone otherwise.
  So if the Show command must be triggered systematically to display goals (as per [coq] On goal display and silent mode. #188), we will just have the simplification that PG always append (list "Show." "Show Proof…") (assuming option coq-show-proof-stepwise is enabled)

• The PR Support Coq's proof diffs feature: highlight diffs in goals and some error messages #421 that added Coq Diffs to goals relies on the Coq option Set Diffs "on". that is not synchronized, so to avoid the fact that the option would be reset at each backtrack, the implemented solution is to re-send a Set Diffs "on". after each backtracking. It happens that if we do Show. at that point, the diff colors are not shown because the following feature has not yet been integrated in Coq: Show diff highlights in the Show, Show <num> and Show <id> commands. coq/coq#10020 (comment) − Fortunately, the Set Diffs "on". itself triggers a re-display of the goal if there is some, so actually this plays the role of the skipped Show. :)

[erikmd]

Thanks @CyrilAnac ! the feature looks very nice.

However it seems the following bug is introduced:

(1) when opening a .v file

Lemma test : forall n : nat, n = n.
  reflexivity. (* (2) then doing "C-c C-RET" to here *)

(3) and finally doing "C-c C-u" to backtrack, we get:

condition-case: Wrong type argument: stringp, nil

− I'm using Coq 8.11.1 on GNU/Linux

Apparently this can be reproduced by directly processing the first line of test_stepwise.v till the end of a comment. I added a regression test (that will fail for now)

[CyrilAnac]

Thanks @CyrilAnac ! the feature looks very nice.
However it seems the following bug is introduced:
(1) when opening a .v file

Lemma test : forall n : nat, n = n.
  reflexivity. (* (2) then doing "C-c C-RET" to here *)

(3) and finally doing "C-c C-u" to backtrack, we get:

condition-case: Wrong type argument: stringp, nil

− I'm using Coq 8.11.1 on GNU/Linux

Apparently this can be reproduced by directly processing the first line of test_stepwise.v till the end of a comment. I added a regression test (that will fail for now)

@erikmd Indeed, I introduced a bug here, the result of (car (nth 1 (car (last proof-action-list)))) is nil and the string-match-p throw a wrong type argument error.
The incoming commit should fix this issue.

[erikmd]

Thanks @CyrilAnac !

BTW if you have some time, you might want to add one or two unit tests (?)

[erikmd]

Also before merging this feature, it'd be great to have users test it a little bit further (notably to ensure there is no unforeseen regression), maybe @jfehrle or @anton-trunov would have the time to do this?

FYI to retrieve the code of this PR it should suffice to uninstall proof-general from MELPA and follow https://github.com/ProofGeneral/PG#using-git-manual-compilation-procedure then do:

cd ~/.emacs.d/lisp/PG
git config --global alias.pr '!f() { if [ $# -lt 1 ]; then echo "Usage: git pr <id> [<remote>]  # assuming <remote>[=origin] is on GitHub"; else git checkout -q "$(git rev-parse --verify HEAD)" && git fetch -fv "${2:-origin}" pull/"$1"/head:pr/"$1" && git checkout pr/"$1"; fi; }; f'
git pr 490
make clean
# make  # optional

and the two options at stake are: Coq > Diffs > on and Coq > Show Proof (Diffs), see screenshot below.

[erikmd]

Sorry, the feature is not yet ready.

BTW if you have some time, you might want to add one or two unit tests (?)

we definitely should add such tests!

I've spotted the following two bugs:

1. If we enable "Coq Diffs" and "Show Proof", with Coq 8.10, interaction is broken (because Coq Diffs are available in Coq 8.10, but not Show Proof Diffs, which have been introduced in coq/coq@5ec7eca) → Cyril could you add some appropriate conditions (if (coq--post-v811) …)? (I've updated the CI configuration to also test with Coq 8.9 and Coq 8.10, but we should also add some tests that make the ci/test.sh script fail with Coq 8.10)

2. If "Coq Diffs" and "Show Proof" are disabled and we backtrack (e.g. with Coq 8.10) then run C-c C-n, then the frontend loops…

[jfehrle]

Coq Diffs are available in Coq 8.10, but not Show Proof Diffs, which have been introduced in coq/coq@5ec7eca) → Cyril could you add some appropriate conditions (if (coq--post-v811) …)

Show Proof Diffs is in 8.11. Perhaps you meant "if (coq--post-v810)"?

maybe @jfehrle or @anton-trunov would have the time to do this?

I don't use PG or emacs on a regular basis. Looks like I don't even have emacs installed on my new laptop. Perhaps Anton would be willing to try it first.

[erikmd]

Hi @jfehrle, thanks for your comment.

Perhaps you meant "if (coq--post-v810)"?

nope: the (coq--post-v811) is actually a ≥ :)

PG/coq/coq-system.el

Lines 200 to 202 in 8273e22

	(defun coq--post-v811 ()
	"Return t if the auto-detected version of Coq is >= 8.11.
	Return nil if the version cannot be detected."

[erikmd]

Thanks @CyrilAnac, I can confirm the backtracking bug is fixed!
I just left a few minor comments.

[erikmd]

Thanks @CyrilAnac, I've re-tested with Coq 8.11.1 and the PR looks very fine now!

Cc @ProofGeneral/core I propose to merge this tonight if you don't object.

[Matafou]

LGTM