lean-pr-testing-2964 conflicts with std4#466

Stream: batteries

[Kim Morrison]

We've just got nightly-2023-12-21, which will hopefully turn into v4.5.0-rc1 tomorrow. This nightly includes lean4#2964, the recent bundle of widget improvements. (@Patrick Massot will be happy!)

I've run into a slight problem, however, which is that @Wojciech Nawrocki's Std branch containing adaptations for lean4#2964 (here's the diff) has a conflict with std4#466, @Thomas Murrills's recent PR allowing customization of the "Try this" prompt.

For now, on Std's nightly-testing branch I have simply reverted std4#466, and then successfully merged Vtec234/lean-pr-testing-2964. This all works (and Mathlib's nightly-testing branch, with the Mathlib lean-pr-testing-2964 branch merged in, does too).

Now we need to get these changes back onto the bump/v4.5.0 branches for both Std and Mathlib, in preparation for the release candidate tomorrow...

[Kim Morrison]

@Thomas Murrills, might you be able to help me "replay" std4#466 onto nightly-testing? Once we've got the changes from std4#466 incorporated there, it should be relatively easy to construct the PR to bump/v4.5.0.

[Kim Morrison]

Ah, actually I think I can do this myself.

[Thomas Murrills]

Ok! (Sorry, was a bit late.) I took a look at the diff, and the implementation would have to change a little: we’d have to push an Array (String × Option String) onto the info tree along along with an Option String.

[Thomas Murrills]

Specifically, we want TryThisInfo to instead have the fields

range : <as before>
suggestionTexts : Array (String × Option String)
codeActionPrefix? : Option String

and then, in the code action provider, have something equivalent to

let (newText, codeAction?) := suggestions[i]'h.2
…
eager.title := codeAction?.getD <| (codeActionPrefix?.getD "Try this: ") ++ newText

[Kim Morrison]

Hmm, I did something a bit different.

[Kim Morrison]

I added the fields:

  /-- The prefix to display before the code action for a "Try this" suggestion. -/
  codeActionPrefix : String := "Try this: "
  /--
  The title of the code action.
  If this is `none`, then the title will be contructed out of `codeActionPrefix` and the suggestion.
  -/
  codeActionTitle? : Option String

[Kim Morrison]

But I guess that doesn't actually make sense.

[Thomas Murrills]

Right, the code action title is individual to each suggestion if provided, and otherwise we look for a code action prefix (and if not found we use Try this:)!

[Thomas Murrills]

The remaining pieces are

• constructing the .ofCustomInfo for pushInfoLeaf
• cleaning up toJsonM and addSuggestionCore (we no longer include codeActionPrefix and codeAction in the json)

[Kim Morrison]

I

[Kim Morrison]

I think I've done it correctly now.

[Kim Morrison]

Would you be able to take a look at Std/Tactic/TryThis.lean on the nightly-testing branch?

[Kim Morrison]

(just pushed now)

[Kim Morrison]

Hmm, it's not quite right. In the test the "Also consider" case is not working.

[Thomas Murrills]

I think I can fix it. Also I’d like to avoid pretty-printing twice! (I’m going to change it to toJsonAndInfoM, if that’s alright) Shall I push?

[Thomas Murrills]

(Er, by push i mean “type it out, then push.” :P)

[Kim Morrison]

Yes please!

[Thomas Murrills]

Ok! Struggled with git a bit but it should now be on nightly-testing on thorimur/std4.

[Thomas Murrills]

(Is there a nice way to link to that or something else I should be doing? Or is that accessible?)

[Thomas Murrills]

I think zulip now subscribes people to threads they start, but here’s a ping just in case since it was 20 minutes between messages :) Scott Morrison

[Kim Morrison]

Got it. :-)

[Thomas Murrills]

(Unrelated, but that is…apparently not the same Scott Morrison when you click on the text? I don’t know what zulip is doing with tagging here :sweat_smile:)

[Thomas Murrills]

Alright, if that's all good(?), I'm going to go to sleep now—this turned out to be a fun little impromptu coding challenge! :grinning_face_with_smiling_eyes:

[Thomas Murrills]

Oof, I forgot two small things:

1. the docstring part about codeActionPrefix? for addSuggestions got lost
2. I had forgotten to pass codeActionPrefix? to all user-facing functions besides addSuggestions

[Thomas Murrills]

There are now 2 extra commits on my nightly-testing branch (described as such) which fixes that, if you want to add it in. If not I can always PR the fix later, no big deal. :)

[Thomas Murrills]

(As well as a third commit because I missed a space before : in those additions. :upside_down:)

[Kim Morrison]

Fantastic, just looking over it now.

[Kim Morrison]

I've merged it to nightly-testing, and will make a PR for bump/v4.5.0 soon.

[Kim Morrison]

Okay, looks great!

@Mario Carneiro, @Joe Hendrix, https://github.com/leanprover/std4/pull/475 should be the last PR required to the bump/v4.5.0 branch. (nightly-2023-12-21 will become v4.5.0-rc1 tomorrow).

[Thomas Murrills]

Great! :D (I'll be turning in now, but if those TryThis changes somehow made something explode (hopefully not!) I'll still be available tomorrow. :) )

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Thanks a lot for your help with this!

[Kim Morrison]

No problem! I think I've got the adaptation PR for Mathlib (i.e. turning lean-pr-testing-2964 into a PR to bump/v4.5.0) ready to go.

[Kim Morrison]

Just compiling locally.

[Kim Morrison]

Looks good to me: https://github.com/leanprover-community/mathlib4/pull/9176

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@Scott Morrison that branch has the wrong adaptations :( I'm really sorry, I made those first and then changed it to the current state here. It's only the new diff that should be used.

[Kim Morrison]

Oh no! My fault, I must have had an old copy of lean-pr-testing-2964 and forgot to pull.

[Kim Morrison]

@Wojciech Nawrocki, could you look at #9176 again? Hopefully it is right this time.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Looks good now! Thank you.