feat: goal-diffs

[EdAyers]

InteractiveGoals now has information that a client infoview can use to show what parts of the goal have changed after applying a tactic.

There are lots of exciting ways to extend this, but I think this PR should be just limited to a first version and getting a sensible and extensible server/client API in place.

API changes

All API changes are conservative so old versions of vscode will still be able to render the goals.

• InteractiveGoals, InteractiveGoal, InteractiveHypothesisBundle now have a message? : Option String field that can be used to emit debugging messages.
• InteractiveGoal and InteractiveHypothesisBundle now have a isInserted? : Option Bool which is true when it is a new goal or hypothesis and should be rendered with a green highlight.
• SubexprInfo has a new tags?: Option String field. Currently the infoview is highlighting green anything that has the tag inserted on it. I would like some comments on whether this is a good way to implement the diff api. The tag approach could cause issues later because it depends on both client and server using the same magic string. Another problem is that it might be causing bloat of SubexprInfo, perhaps instead the diff info should live on its own map from position to tags.

Todos

• tidy up
• feat: preliminary definitions for goal-diffs #1607 no longer depends on this
• vscode extension PR feat: goal-diffs vscode-lean4#251
• unit tests
• explain the api here
• write a docstring explaining diffing algorithm used

Todos/ future work

• We use goalsBefore and goalsAfter on the TacticInfo object to get the diff. Currently I only show the diff on useAfter = true, perhaps I can also write a version for useAfter = false so that you see the change that is about to happen.
• If a hypothesis is deleted, render it with a red triangle at the point that the hypothesis was deleted.

Resolves #1469

[Vtec234]

• SubexprInfo has a new tags?: Option String field. Currently the infoview is highlighting green anything that has the tag inserted on it. I would like some comments on whether this is a good way to implement the diff api. The tag approach could cause issues later because it depends on both client and server using the same magic string. Another problem is that it might be causing bloat of SubexprInfo, perhaps instead the diff info should live on its own map from position to tags.

From the perspective of the size of sent packets this is not an issue because we serialize tags? := none as nothing (0 bytes) in JSON. Earlier on I was thinking we may still prefer to use an external map SubexprPos -> Tag alongside the current TaggedText<SubexprInfo> rather than including Tags in the SubexprInfo, basically because the current set of tags (used for goal diffs) is only relevant to the goal view; so when we use CodeWithInfos aka TaggedText<SubexprInfo> elswhere, such as in error messages, we get the "extra stuff" of tags which could be considered bloat.

However I am now thinking that tags could be useful more generally. For example, some error messages may want to bring the user's attention to a subexpression at which a tactic failed, or whatever, while still displaying the full top-level expression. For this though, because in different contexts (goal vs error message vs hover popup vs ..), "green background" may have different meanings, it might be better to think of the infoview as a "dumb" display which doesn't know the semantics of "inserted/deleted/relevant" subexpression but simply gives it a particular colour or style. So i'd suggest renaming the tags to something style-y rather than semantic-y. E.g. "green"/"red". What do you think?

[EdAyers]

Yes I'm always in favour of functional styling

[Vtec234]

I didn't review Diff.lean in detail but everything else looks good!

[Kha]

I didn't think about the new heuristics too hard yet. I'd say let's simply give them a try.

[Kha]

@EdAyers Feel free to PR a changelog entry for RELEASES.md once the extension change has landed!

[gebner]

Sorry for only getting to this PR now.

"green background" may have different meanings, it might be better to think of the infoview as a "dumb" display which doesn't know the semantics of "inserted/deleted/relevant" subexpression but simply gives it a particular colour or style. So i'd suggest renaming the tags to something style-y rather than semantic-y. E.g. "green"/"red". What do you think?

For the record, I would have preferred "inserted" and "removed" instead of "green" and "red," resp. There are several reasons:

1. It is consistent with the isInserted? and isRemoved? fields.
2. We could maybe show an "inserted" tooltip to explain what the color means. (I didn't think about this a lot though, the tooltip probably doesn't mix well with the popup we already have.)
3. The "blue" color clashes with the highlighting.

[digama0]

Also, it's generally a bad idea to talk about colors directly because people have themes that can make the colors different, and then it's really confusing when isGreen means it's blue and isRed means it's gray in the theme. (Also colorblind people exist, and they usually switch the themes to something appropriate.)

[Vtec234]

I agree, but it seems none of the points raised here apply to the style-predicates vs semantic-predicates choice, it's just that green/red/blue is maybe not the best choice of style-predicates. To be fair, we could think of inserted/removed as style-predicates which indicate "draw this in the same way git diff would".

[EdAyers]

I am happy to open a PR reverting to semantic tags instead of colours. In response to the theming and colour-blindness, the actual colours that are displayed at the moment are a function of whether the theme is light or dark. It should be possible to get the colours to be completely theme-dependent by using these.

In the case of using a semantic tags model, are you ok with having a tags?: string[] field or would you prefer something more type-safe like diffTag?: 'inserted' | 'removed'?

[Kha]

In the case of using a semantic tags model, are you ok with having a tags?: string[] field or would you prefer something more type-safe like diffTag?: 'inserted' | 'removed'?

Let me highlight this question since people may have missed the edit. Personally I don't have any strong opinions on it.
I'm assuming we're waiting on this change before the extension PR is merged.