Show diff highlights in the Show, Show <num> and Show <id> commands.

[jfehrle]

Kind: feature.

Currently these Show commands don't display diff highlights, which they should. Also, Proof General uses a Show when it undoes a proof step, so there are no diff highlights. That makes the same proof step look different depending on whether you got to that step by going forward or backward.

This PR adds that support.

One wart in this code is the need to create the reference variable Proof_global.get_prev_proof, which is set from Stm. The problem is that if Vernacentries calls Stm directly, it creates a circular dependency that won't compile or link. If anyone has a better idea, please let me know.

I hope we can get this into 8.10.

[vbgl]

Postponing to 8.11: the set of features for 8.10 has been frozen a few weeks ago. Thanks for your understanding.

[ejgallego]

One wart in this code is the need to create the reference variable Proof_global.get_prev_proof, which is set from Stm. The problem is that if Vernacentries calls Stm directly, it creates a circular dependency that won't compile or link. If anyone has a better idea, please let me know.

I'm afraid we won't be able to add this kind of fragile hack to the codebase; indeed, the API is purposely structured as to avoid this kind of pattern.

Already in the original PR adding diff state, I suggested to use a design where ownership of the proof was more clear; with regards Show goals usually the UI would utilize a show with diffs operation that takes the two identifiers needed and is implemented in the PG-specific layer [g_toplevel]

[jfehrle]

I'm afraid we won't be able to add this kind of fragile hack to the codebase

How is this more fragile than any other bit of code?

I suggested to use a design where ownership of the proof was more clear; with regards Show goals usually the UI would utilize a show with diffs operation that takes the two identifiers needed and is implemented in the PG-specific layer [g_toplevel]

While it's needed for PG, this is not a PG-specific change. If diffs are turned on, you should see them in the Show command output for consistency.

This is a reasonable and modest change to the user experience. There should be a reasonable way to implement it with a moderate effort rather than requiring major changes. The current structure of diffs is based on what you requested. I can't tell from your comment what you're proposing. Perhaps to pass the previous proof down through Vernacentries.interp in Stm.vernac_interp?

(What are you trying to achieve for the APIs with the various refactorings you've been doing? I don't know what you're aiming for architecturally or trying to preserve. It would helpful to understand that.)

[ejgallego]

How is this more fragile than any other bit of code?

It violates separation of components and state ownership invariants.

Perhaps to pass the previous proof down through Vernacentries.interp in Stm.vernac_interp?

Indeed that would be a reasonable choice, and we could incorporate such a change.

However IMO diffs should be always initiated by the UI; for example in SerAPI you would write (Query ((sid id1) (diff_with id2)) Goals) and the interpreter, which at that level has full access to the document manager would indeed return the right diff object.

Using "Vernaculars" for print is anachronic and indeed shouldn't be relied upon; I have brought this issue in PG a few times but so far we didn't do a lot of progress.

[jfehrle]

Postponing to 8.11: the set of features for 8.10 has been frozen a few weeks ago. Thanks for your understanding.

@vbgl IIRC @Zimmi48 told me that there was plenty of time before 8.10 would be shipped (until early June) when I asked in early April about completing some work for 8.10. Perhaps I misunderstood. I suppose https://github.com/coq/coq/projects/32 is the list of things planned for inclusion. Right? (FWIW, I notice the activity list therein doesn't show your moving this PR to 8.11)

Is the schedule posted somewhere and updated when it changes significantly? It would be helpful if the process was documented some (e.g. criteria for including PRs submitted after the release branch is first created), assuming there will be some consistency on that across releases. That might save release managers from some questions.

Regarding this PR, "new feature" overstates its novelty. The current code can display diffs as part of the proof state after each tactic. The Show commands use a different code path that displays part of the proof state, which I wasn't aware of until a couple days ago. This PR just makes their behavior consistent. "bug" is probably just as appropriate a kind for this PR. If that makes a difference, I hope we get this into 8.10. And if not, so be it. We can manage without it for a while. (No need for a lengthy reply.)

[ejgallego]

Is the schedule posted somewhere and updated when it changes significantly?

Indeed communication in the release process could be improved quite a bit.

Not so long ago I added a link to the wiki from the readme tho https://github.com/coq/coq/wiki/Release-Plan

I'm much afraid that this PR, given its current state, will miss 8.10. We can however get #10019 in if the PG developers confirm the tags are OK for them.

[jfehrle]

I'm much afraid that this PR, given its current state, will miss 8.10

The current state is not what you think :-) Check the version I just pushed.

[ejgallego]

The current state is not what you think :-) Check the version I just pushed.

You don't need to convince me but @vbgl

[ejgallego]

The fact that the previous proof needs to be added to a core function highlights the problem with overloading the base API which was already sketchy (Show I'm looking at you)

It is not clear to me if we should keep adding kludges or the moment for UI developers has arrived: they either adopt a modern protocol or they renounce to advanced functionality.

[ejgallego]

If dproof appears all the time I guess it should be placed on Vernacstate.

[ejgallego]

Looks much better, however the ownership/control of the previous proof has some small issues:

• the previous proof seems to be updated at the wrong place (should it be the state update function in vernacentries the one to update it?)
• the function that fetches the old proof seems not correctly implemented.

My general reservations about the kluges are still on; IMHO we should not overload Show in this way, but I won't oppose merging, the impact is pretty small and anyways the whole infrastructure needs cleanup.

[vbgl]

Dear Jim,

The schedule for the 8.10 release has been announced on the coqdev mailing list (see e.g., https://sympa.inria.fr/sympa/arc/coqdev/2019-01/msg00035.html). About one month ago (https://sympa.inria.fr/sympa/arc/coqdev/2019-03/msg00021.html) I wrote that “feature” PRs are no longer welcome in the 8.10 branch.

I did not look at the changes that are in this PR and expressed no opinion about them. The first line of this PR description reads: “Kind: feature”. If you believe this is inaccurate, then please choose a different wording.

Thank you for your work on improving the Coq ecosystem. Your contributions will reach the end users; probably as part of the outstanding 8.11 version.

[jfehrle]

the previous proof seems to be updated at the wrong place (should it be the state update function in vernacentries the one to update it?)

Set up the previous proof in Vernacstate.freeze_interp_state, derived from the existing proof field? That would mean passing it as an argument in 18 places in Stm.

Which one is the "state update function" in vernacentries? Lotta functions in there.

[jfehrle]

@ejgallego Please take a look at the latest version, thanks.

[Zimmi48]

IIRC @Zimmi48 told me that there was plenty of time before 8.10 would be shipped (until early June) when I asked in early April about completing some work for 8.10. Perhaps I misunderstood.

Indeed, you misunderstood. I can't find again the mail in which I told you this, otherwise I would quote it, but all I told you was the schedule of the beta and the final release, that left plenty of time for finalizing things like #10019. I never said that new features would be accepted during this period. If I were the RM, I would reject this PR from 8.10 just like @vbgl did.

[herbelin]

I think the “fix” is not critical enough to justify doing what you propose though.

How to "fairly" evaluate that?

[gares]

@gares would you approve this at least for master if it's agreeable? And what about getting it into 8.10?

I think the change wrt STM is OK for master.

I don't think this this is so urgent to justify a backport: it brings very little to CoqIDE (since Show is not something you use there) and, even if it is implemented in another way, PG users already have proof diffs if I'm not mistaken.

Don't get me wrong, It is clearly welcome to have a single proof diff feature that works for both UIs, but I believe it can be merged in master and be released in 6 month for the reason above.

I also agree that this patch is only required because PG is still interacting with Coq in a simplistic way (no protocol), so the code of this PR is going to be removed as soon as PG evolves, or we provide a valid alternative. But since we are not there today, I think we cannot reject this kind of patches on the basis of what we would like, but we did not manage yet, to do.

[maximedenes]

Don't get me wrong, It is clearly welcome to have a single proof diff feature that works for both UIs, but I believe it can be merged in master and be released in 6 month for the reason above.

+1

[jfehrle]

@ejgallego Earlier you suggested moving the commands to g_toplevel but then you seem to have changed your mind on that, too. Just to be clear, is that a reasonable solution or not?

@ejgallego: Indeed; the PG protocol already has a place where commands such as this proposed extension can be hosted, g_toplevel, so @jfehrle can implement it there if he needs it.

@jfehrle: I'm open minded, but I don't understand exactly what you're suggesting here and what changes it entails. Do you mean moving the Show commands out of Vernacentries and into here? That move wouldn't break anything?

@ejgallego: We need to think a bit what's the principled solution here; but as @gares points out (and I agree with him) this is a command that should be handled at the UI protocol layer, that's even higher in the current design than the STM. So there is no "easy" and principled solution I'm afraid.

[jfehrle]

@gares: I don't think this this is so urgent to justify a backport: it brings very little to CoqIDE (since Show is not something you use there) and, even if it is implemented in another way, PG users already have proof diffs if I'm not mistaken.

JFR, @cpitclaudel said "The [diff] feature you implemented is superior" in ProofGeneral/PG#421 (comment). He is one of the principal implementors of company-coq, the PG add-on which provides the diff feature you refer to.

[cpitclaudel]

FWIW, I don't think there's much of a hurry (I don't use diffs very often, in fact).

[ejgallego]

Indeed I had a look at this PR again and unfortunately the current approach is not going to work, specially after all the work done on the reifyication of vernacs.

IMVHO the best bet is to place the Show with Diffs command in the toplevel in a similar fashion to what's been suggested in #10356 [that is, add it to g_toplevel]; I'm convinced that will make @jfehrle 's life much easier in both cases.

[ejgallego]

This is going stale; I may close if not further updates before the end of the year [of course you are very welcome to re-open once you have time]

[erikmd]

Hi @ejgallego,

Just FYI @jfehrle's initial post mentioned that

Also, Proof General uses a Show when it undoes a proof step, so there are no diff highlights. That makes the same proof step look different depending on whether you got to that step by going forward or backward.

and that was indeed an issue! But for the record this is not the case anymore [roughly, instead of doing e.g. BackTo 18. Show., ProofGeneral triggers BackTo 10. Set Diffs "on". or so (cf. code)], so this PR is not blocking anymore for ProofGeneral's support of Diffs − albeit this PR stays a handy feature to have (and it will be necessary e.g. to ensure the Diffs are shown when doing C-c C-l C-c C-p, which is precisely a shortcut for Show :)

[jfehrle]

@erikmd is correct. This PR is less urgent but still worth doing. Just working on some higher priorities first.

[Zimmi48]

Dear PR author(s) and contributors, it seems to us this PR may need additional work beyond the 8.12 branching deadline on May 15th.

We are thus removing the 8.12+beta1 milestone; please retarget as appropriate, and also consider updating labels to reflect current status, moving the PR to draft status, etc.

We apologize in advance if we misunderstood the PR status.

[ejgallego]

As discussed with Théo there seem to be some design questions about this PR, feel free to have a discussion in a Call or in Zulip when you would like to retake this.

[jfehrle]

I'd like to clean this up but probably won't get to it for a month or 3. Still pretty focused on updating the syntax in the documentation. There's also the IMHO more urgent issue that Show Proof Diffs is only available in coqtop and PG but not in CoqIDE or, I expect, any other IDE. (Also applies to Show Goal, see #10356.) Seems like these would have a common solution.

@erikmd tells me he's finding Show Proof Diffs useful for teaching. He also tells me that we may soon see progress toward getting PG to use the XML interface (where the command isn't available), so it would be good if we can fix this for 8.13.

How can we make these commands available in all user environments?

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app]

This PR was not rebased after 30 days despite the warning, it is now closed.

[coqbot-app]

This PR was not rebased after 30 days despite the warning, it is now closed.