Code actions wishlist

Stream: mathlib4

[Julian Berman]

I thought it might be nice to have a place to collect code action ideas. I'm not sure here is the exact right place as opposed to an issue, but maybe others have their own wishlist.
The ones I had (without doing investigating of how feasible they are) were:

• an extract_goal tactic action (mentioned here which I'd have moved here but it looks like we have a 7 day limit on moving messages, TIL!)
• a #guard_msg action -- given a line with a command which produces output, insert a guard_msg block above with the output
• a #min_imports action which changes the imports (I think this has been mentioned somewhere and the difficulty was being able to find the lines which contained imports?)
• a consecutive rewrite action -- so, given 3 consecutive lines rw [foo]; rw [bar]; rw [baz, quux] all of which rewrite the same location (here the goal), emit an action which combines the lines into rw [foo, bar, baz, quux]

[Ruben Van de Velde]

• Split simpa into simp at h; simp; exact h (inferring which hypothesis is used); I could have used this just now debugging why one broke with a newer mathlib

[Johan Commelin]

import Mathlib

#guard_msgs in
example : 0 = 1 := by
  rfl

already has a code action. Is that not doing what you want?

[Julian Berman]

The one I want is to activate on:

#check 37

or in your example just

example : 0 = 1 := by
  rfl

(because both produce output) and offer to add all of #guard_msgs in + the message

But I admit I wasn't aware of the one you mentioned either so perhaps it's enough as-is (I'll have to play with it and see how happy my fingers are).

[Yaël Dillies]

Ruben Van de Velde said:

• Split simpa into simp at h; simp; exact h (inferring which hypothesis is used); I could have used this just now debugging why one broke with a newer mathlib

I wrote a lean RFC that would make this (mostly) redundant. I will try submitting today or tomorrow