Conversation
* make the code action more informative
|
The Can we support their use case? They are doing something a bit extra, which is actually running the tactics against the goal and putting in 🎉 emojis where appropriate. They also need to cope with the case of "bad suggestions" for which they only have Strings that can't be parsed into |
|
@semorrison I think so! There are two additional pieces of functionality I see that we'd need to supply here:
If these both become fields of the Then, there are two ways I can think of for modifying the setup to handle the "bad suggestions".
I'll think about this a bit, but if you have an opinion on which of these options would be the best way to handle the invalid suggestions (or favor a different option), please let me know! :) |
|
The reason there are non-parseable suggestions in the llmstep example is that the suggestions are coming from a language model, which sometimes has no idea what it is doing! :-) Nevertheless, the thinking is that sometimes there might be the germ of a good idea, which the human could still make use of. So for their application, they do want to be able to show plain text suggestions (whether or not they are clickable is probably less important: users will use these ones less often, and perhaps can be expected to copy and paste). The wrapper for And yes, absolutely |
* replaces `info` field
* used in place of `TSyntax` * `Suggestion` loses its `kind` parameter
This reverts commit 7ccdd98.
* instead of "Tactic replacement"("s")
* reflects fact that we might not be suggesting a tactic
* `style` can be used to specify replacement text style * this handles e.g. recolors correctly on mouseover * appending `red` to the class behaved incorrectly on mouseover * `className?` simply overrides the attr instead of appending * no need to hem the user in; provides greater flexibility
* at the cost of duplicate code
|
(Apologies for the force push, accidentally pushed some clutter.) |
|
@digama0, what do you think of this PR at this point? It would be nice to get this in so that both LeanInfer and LLMStep can adopt it, rather than having a version in each repository. I'd also like it to restore the |
joehendrix
left a comment
There was a problem hiding this comment.
This looks good to me. Thanks for all the comments.
digama0
left a comment
There was a problem hiding this comment.
Apologies for not giving this a proper review for so long. I've made several changes, most notably to remove all of the getStyle logic and just let users pass in a json object with the style they want (and retaining the existing styles, as presets). Anyway it is now ready to merge IMO, but I will give @joehendrix @thorimur @semorrison time to speak up since I made some significant modifications.
|
For ease of reviewing, Mario's changes are: |
|
@digama0 I quite like the refactor you've made to the style logic! I was also wary of all that JS and reluctant to constrain the user to my choices. This is much better. (And I don't think we had the I went through the code and only found an incorrect test description from myself, which I fixed. LGTM. :) |
There's a reason it was merged just a few hours ago... |
This PR introduces
Try these:functionality to thetryThiswidget and associated definitions, such asaddSuggestions, which renders an array of replacement suggestions as a bulleted list in the infoview preceded by "Try these:".Currently, tactics in Mathlib which return many different "Try this:" suggestions, such as
apply?andrw?, work by creating a separate "Try this:" widget for each individual suggestion. This takes up a lot of space in the infoview—each suggestion includes its own "Tactic replacement" summary element and the wordsTry this:.This was discussed briefly and requested as a std4 PR on zulip.
This PR also provides both widgets with configurable headers—the text
Try these:andTry this:can now be modified at will. (This is motivated by upcoming tactics likehint, which may want different lists for different things, e.g. a list of tactics which close the goal, and a list of tactics which don't.)This PR also modifies the form of the code actions. Currently, tryThis code actions all read simply
"Apply 'Try this'". We change this to the more informative"Try this: {replacementText}". This is necessary in order to have distinguishable code actions now that we're handling a list of different possible replacements instead of just one.Finally, this PR also allows for a bare
String(instead ofTSyntax) to be used as a suggested replacement viaSuggestionText, and provides 6 basic styling options for each entry viaSuggestionStyle:.error,.warning,.success;.asHypothesis,.asInaccessible; and.value (t : Float), which draws from a red-yellow-green color gradient with red at0.0and green at1.0.I'm not 100% sure these are the "right" HTML classes to be using to style the text in a code-like fashion, even though they look alright so far.