company-coq
company-coq copied to clipboard
cpitclaudel
visual diff of goals before/after tactic
The visual diff of long type mismatch error messages is certainly useful, but can a similar thing be done about goals? I have a few tactics that, when I apply them, make very subtle changes to the goal context - sometimes so subtle and in such a large goal that I have to undo/redo them several times before realizing what changed. It would be nice to have a visual diff to highlight that type of change.
Reading through long goals has more issues. I do have a tactic that uses the new multiple-identically-typed-hyps-per-line feature to minimize the number of lines in a goal, but I am always wishing for more help with long complex goals. One thing I do on occasion is place the cursor in the goal and regexp search for a particular hyp to get emacs to highlight all spots in other hyps and conclusion where it is used. I think it would be helpful if there were ways to do such helpful highlighting while keeping the cursor in the proof script, for instance. Just brainstorming...
Nice suggestion! One thing I use instead of the regexp search that you mentioned is `highlight-symbol-mode'. I'll consider adding support for goal diffs, though I fear that the new compact display that Pierre hinted at in https://github.com/cpitclaudel/company-coq/issues/24 might make this harder (@Matafou, opinions?).
This is the tactic (minlines) I use to minimize the lines in a goal:
Ltac revert_all :=
repeat lazymatch goal with H:_ |- _ => revert H end.
Ltac get_value H := eval cbv delta [H] in H.
Ltac has_value H := let X:=get_value H in idtac.
Ltac minlines :=
idtac; (*prevent early eval*)
let stop:=fresh "stop" in
generalize I as stop;
revert_all;
let rec f :=
try (intro;
lazymatch goal with H:?T |- _ =>
first[constr_eq H stop; clear stop
|let v := get_value H in
try match goal with H' := v : T |- _ =>
first[constr_eq H H'; fail 1
|move H before H'] end; f
|try match goal with H':T |- _ =>
first[constr_eq H H'; fail 1
|has_value H'; fail 1
|move H before H'] end; f
|f]
end)
in f.
Of course, unlike Pierre's suggestion, it can only combine hyps of the same type (or type and value). I've thought about other kinds of goal minimization - such as merely listing all non-dependently-typed hyps that are used in other hyps by name on a single line. So, all bools, nats, Zs, etc. would just be mentioned by name on one common line, unless they were not used by any other hyps (an indication that they are perhaps not meant to be implicit). Humans can do type inference, too, if it is easy enough. And maybe hovering the mouse over such a hyp's name would show its type.
I just loaded highlight-symbol-mode - thanks for that, it saves on the regexp search. I notice that it doesn't work across panes/frames/windows - so I still have to move the cursor around in the goals window to find stuff. Maybe there is some setting in this mode to share the same symbol-to-be-highlighted across several buffers?
The current experiment I am making on a private coq branch (https://github.com/Matafou/coq/tree/v8.5-compactcontexts, use "Set Compact Context") uses the following heuristic: if a sequence of hypothesis has sort Type, then print them in an horizontal box. Of course one can put all Type-sorted hypothesis on top with trivial piece of Ltac.
In most cases (i.e. no dependent programming) I find it surprisingly efficient in shrinking the goals. We could also hide their types. Doing the same with non-dependent hypothesis is probably worth a try too. P.
To answer Clément's question, it is probably not so difficult to have a decent diff mode while in compact mode:
- difference in the compact part are probably not very pertinent anyway.
- You can switch of compact mode temporarily to get the diff, and then recompactify. Or maybe use the fact that il compact mode I use a 3 space separator...
Hi people,
I have a prototype for this; it's in experiments/company-coq-goal-diffs.el. Opening that file and running eval-buffer (after opening a Coq source file) should be enough to enable it.
I'd like feedback before merging this feature :) Here's a demo: https://asciinema.org/a/7rt8tq441yy7i7eyi5zegox4l
Great :) I'll have to look into finer grained diffs. But ideally one would walk the ASTs instead of working at the text level, and I can't do that at the moment.
The obvious case where this is a big help is when a tactic like inversion impacts hypotheses that one didn't anticipate.
But, this is also going to make it easier to popularize doing proofs without directly naming hypotheses in tactic invocations. When one does something like "match goal with H : T |- _ => apply lemma in H end" in the proof script instead of "apply lemma in Hyp", one big issue is where to look in the goal window to see the change. Especially if it is "repeat match ...." - what hyps were impacted? It is very nice to have something to immediately attract your gaze in such cases.
I just tried it out, and it is not cooperating in my proofs as nicely as in your demo. I will send along some screen shots...
I ran into this soon after posting this last night, but then I quickly pushed a fix. Could it be that you got the intermediate version? Sorry about that!
Yes, re-pulling helped. Thanks!
So, this is a "semantic" diff? I noticed that moving hyps doesn't cause any diffs to show up.
Would it have been easier just to do a diff of the whole contents of the goals window? That would also so changes in conclusions, other goals, and even the subgoal header at the top. Maybe that is too much, as some of it is always expected to change (like that meaningless subgoal ID at the top). Also, it would cause a large amount of diffing on any change in focus. I don't know. But, if you do get word-level diffs working, I would recommend it on the conclusions as well as the hyps.
It's hard to show a good diff when you only see the after-case, though...
I need to try some other examples. Many of my proofs aren't doing much, because the conclusions are changing much more than the hyps...
For some weak meaning of semantic, yes. It compares the list of names, and for matching names it checks the types. It will see renamed hypotheses as new, and it won't indicate reorderings.
Word-level diffs would be great, but there doesn't seem to exist a proper elisp library for these. I've asked around.; we'll see if I overlooked something.
Thinking more about this, I think there are really two features under discussion here: one is an always-on, subtle indication of what changed in the current goal. The current prototype is a step towards this. The other one is a more intrusive "full diff", which allows for more precise comparisons.
I've pushed a draft implementation of the second feature. Can you try company-coq-goals-diff?
You mean company-coq-diff-goals - cool! I like it! I think you are right that the type of diffing needed to show enough detail so that the user doesn't have to repeat undo/redo the proof step does need to be a separate feature from the subtle changes feature. Unless a user wants to use that diff window instead of the goals window.
Great. So I think the way to go is probably to make subtle highlighting the default, and to find a way to make the full diff discoverable. Maybe a hyperlink in the goals window.
I've bound C-c C-a C-d to company-coq-diff-dwim. which invokes either company-coq-diff-unification-error or company-coq-diff-goals based on the context. The diff replaces the goal, and pressing that same key combination closes it. Adding a numeric prefix to that command changes the number of context lines. I'll leave this open until the lightweight goal highlighting code is merged.
Is there a way to interleave the diff lines, so that each hyp is next to its diff? I tried a numeric prefix of 1, but that doesn't alter it to be interleaved 1-line diffs when there are multiple adjacent hyps that changed.
Not with the default diff. I'll give this more thought after the CAV deadline on Friday :)
Some preliminary thoughts, however:
- With just GNU diff, it seems tricky; see https://stackoverflow.com/questions/22134471/git-diff-with-interleaved-lines
- If we don't care about order of hypotheses, I think I have a relatively clean solution. Do we care about order of hypotheses? I'd guess we do, but then the problem itself is slightly ill-defined.
Notice that ediff-buffer allows for this kind of things. P.
2016-01-26 7:06 GMT+01:00 Clément Pit--Claudel [email protected]:
Some preliminary thoughts, however:
- With just GNU diff, it seems tricky; see https://stackoverflow.com/questions/22134471/git-diff-with-interleaved-lines
- If we don't care about order of hypotheses, I think I have a relatively clean solution. Do we care about order of hypotheses? I'd guess we do, but then the problem itself is slightly ill-defined.
— Reply to this email directly or view it on GitHub https://github.com/cpitclaudel/company-coq/issues/29#issuecomment-174849625 .
In some interactive diff mode in emacs we can focus one diff to see the difference at the word level.
Isn'it what you are looking for? P
Le mar. 26 janv. 2016 à 14:05, Clément Pit--Claudel < [email protected]> a écrit :
@Matafou https://github.com/Matafou can you clarify?
— Reply to this email directly or view it on GitHub https://github.com/cpitclaudel/company-coq/issues/29#issuecomment-175001939 .
I think you're thinking of diff-refine-hunk, which we're already doing in the full diff case. What we're looking for is a way to adjust the semantics of diff to do what's described in https://stackoverflow.com/questions/22134471/git-diff-with-interleaved-lines.