Tactic code actions

Stream: mathlib4

[Mario Carneiro]

std4#132 continues the series of code action related PRs, adding a framework for running code actions on tactics and tactic sequences. There aren't any flashy code actions implemented yet, but one simple one is the Remove tactics after 'no goals' code action:

example : True := by
  trivial
  trivial -- <- remove this, proof is already done
  rfl

is transformed to

example : True := by
  trivial

Note that this is elaborator-aware, and the code action will not show up unless the tactic is applied to no goals. Hopefully this will be useful when cleaning up broken proofs after a tactic gets smarter and closes more goals.

[Mario Carneiro]

The fun part of this implementation is the indentation sensitivity:

example : true := by
  skip
  · skip
    rfl
    |

after a hypothetical "insert library_search" code action:

example : true := by
  skip
  · skip
    rfl
    library_search

as compared to:

example : true := by
  skip
  · skip
    rfl
  |

which goes to

example : true := by
  skip
  · skip
    rfl
  library_search

where the | represents the cursor position.

[Mario Carneiro]

Added another code action. Invoking tactic code action "Generate an explicit pattern match for 'induction'" in the following:

example (e : Nat) : Nat := by
  induction e

produces:

example (e : Nat) : Nat := by
  induction e with
  | zero => done
  | succ n n_ih => done

It also works with cases.

[Johan Commelin]

I guess we should bump the std dependency of mathlib to get access to all these goodies? Or do you have even more lined up?

[Mario Carneiro]

/poll How should the branches of the induction tactic be terminated?
done
sorry
_
?_
newline + 'done'

[Mario Carneiro]

@Johan Commelin They aren't merged yet, I would like to get some review on them and most of the people who could do so are indisposed

[Mario Carneiro]

Note that _/?_ at the end of induction arms means something special: it postpones the proof of that branch until after the tactic, equivalently to using induction e on its own. In practice that means that you will not get an error on the _ but rather on the by because the proof is not finished, with two subgoals remaining

[Mario Carneiro]

Since it's just for editing it doesn't matter too much one way or another but perhaps we want to encourage some style

[Damiano Testa]

The zero branch is often solved by simp: maybe the action could be optimistic and try that...

[Johan Commelin]

But the code action isn't just for induction on Nat, or is it?

[Damiano Testa]

It seems not, but it could be even more optimistic! For lists also simp could solve the empty case...

[Damiano Testa]

Anyway, it is just a suggestion: since there is the need for human input always otherwise, this takes care of some completely trivial situation where you may not need to do anything else.

[Thomas Murrills]

Re: how to terminate the branches, it would be neat if we chose something that would be standard for other code actions to chain on! E.g. if we choose sorry, maybe sorry could be a generic starting point for other code actions, and options to replace the sorry with simp, a result from library_search, propose, etc. would pop up. (Possibly in a “smart” way, informed by the position of sorry in the tactic and even the outcomes of the potential suggestions.)

[Scott Morrison]

Can we get a hook that checks for spare CPU capacity? :-)

[Mario Carneiro]

Hole and tactic code actions are now live on Std, although the API might not be quite stable yet and it might evolve as more code actions are added. I pushed two new simple code actions:

example : True := _ -- <- "start a tactic proof"

example : True := by
  done

and

example : True ∧ True := by
  constructor
  -- <- "add subgoals"

example : True ∧ True := by
  constructor
  · done
  · done

[Scott Morrison]

and bors is working on !4#4012 which brings these all to mathlib4!

[Mario Carneiro]

Thomas Murrills said:

Re: how to terminate the branches, it would be neat if we chose something that would be standard for other code actions to chain on! E.g. if we choose sorry, maybe sorry could be a generic starting point for other code actions, and options to replace the sorry with simp, a result from library_search, propose, etc. would pop up. (Possibly in a “smart” way, informed by the position of sorry in the tactic and even the outcomes of the potential suggestions.)

Code actions are currently doing a bit of both here. They are somewhat loose regarding what constitutes a tactic sequence terminator (the one I just pushed supports done, sorry, admit and nothing at the end of a tactic sequence), and will also preserve the user's preference where possible (an example of this is in the induction auto-fill code action which uses _ if you used _, ?_ if you used ?_ and sorry if you used sorry). So while yes, we certainly want code actions to be chainable, they should also be somewhat non-prescriptive regarding different lean styles

[Mario Carneiro]

@Scott Morrison Actually you might want to bump !4#4012 again if you want the other code actions, currently it only has "try this" I think

[Scott Morrison]

I bumped (again, twice).

[Scott Morrison]

Code actions have landed in mathlib4!

[Scott Morrison]

import Std

example : True := _

[Scott Morrison]

Library search code action

[Scott Morrison]

I mean, can we actually deploy this as is? I'm guessing we are going to conclude that it is unkind to people's CPUs and battery life if every time you put you cursor on a _ or sorry, library_search runs in the background...

I would sure like to, however. :-)

[Scott Morrison]

(it is worth noting that library_search is vastly more performant than you are used to, if you haven't been using it in the last few weeks)

[Adam Topaz]

I need a new computer anyway ;)

[Adam Topaz]

More seriously, can we put the automatic library search behind some optional configuration?

[Scott Morrison]

Yes, we could certainly put this behind a set_option.

[Scott Morrison]

There's not really a convenient mechanism for individuals to run mathlib with different options than the default, however.

[Scott Morrison]

You could test for an environment variable??? Try to ask the OS if there are spare CPUs? :-)

[Adam Topaz]

Can it be done with an option in the vscode extensions perhaps?

[Adam Topaz]

Scott Morrison said:

You could test for an environment variable??? Try to ask the OS if there are spare CPUs? :-)

Checking for spare CPUs still doesn't help with battery life, unfortunately.

[Heather Macbeth]

Scott Morrison said:

There's not really a convenient mechanism for individuals to run mathlib with different options than the default, however.

I'd prefer to have this fixed by addressing this issue...

[Scott Morrison]

Different options interacts somewhat scarily with caching. Do you refuse to use the olean cache? Or just hope for the best?

[Heather Macbeth]

Ah, I see.

[Heather Macbeth]

Well, where I have really wanted this is in my own tiny mathlib-dependent projects, where caching isn't an issue. But maybe indeed it wouldn't be useful for the problem at hand here

[Mario Carneiro]

Scott Morrison said:

I mean, can we actually deploy this as is? I'm guessing we are going to conclude that it is unkind to people's CPUs and battery life if every time you put you cursor on a _ or sorry, library_search runs in the background...

I would sure like to, however. :-)

For the version shown here, I see no reason why it would need to run in the background

[Floris van Doorn]

I agree with Mario. Shouldn't the computation happen after you click the "use library_search" button?

[Scott Morrison]

But I'd prefer not to even see a pop-up if library_search isn't going to solve it. I want the information of "there is an easy proof from here", not "save 14 keystrokes".

[Mario Carneiro]

I think that should be an option, set_option keep_me_warm_in_the_winter true

[Mario Carneiro]

you may as well run tidy or aesop or other general purpose automation for that

[Floris van Doorn]

But if any other code action applies (like your example already shows!), you only see whether library_search works after you click the lightbulb. So for your wish we would need additional tooling.
Your behavior sounds useful, but should probably not be the default.

[Thomas Murrills]

Does it make sense to have vscode extension preferences for things like “run library search before clicking the lightbulb”? (Is there a way to make such preferences extensible, so you don’t need to PR the extension each time you want to add a preference?) This seems like an extension behavior/UI configuration, after all, not a mathlib configuration per se.

[Mario Carneiro]

I think it would make sense to be able to set lean options in the VSCode extension settings, yes

[Mario Carneiro]

Of course you have to be careful not to set any options that change the behavior of lean code, but I think the caching concerns aren't a major issue provided that all the built oleans use the official option set and the server only uses your custom options when processing files in the editor

[Thomas Murrills]

Perhaps options could be registered (when declared) as being exclusively “UI” options (i.e. not changing the behavior of Lean code), and only these would be customizable via the extension

[Mario Carneiro]

Right now I think the bigger issue is that you can't set custom options at all via -D

[Mario Carneiro]

I think this will be a rather advanced technique and so I'm not too fussed about putting guard rails on it. Theoretically any option could affect lean code (you could just have a tactic which emits a declaration if pp.all is on), but in practice most don't, or at least not in any interesting or easily observable way even if it changes the hash in some way

[Mario Carneiro]

This is really a design criterion for options. Looking at the list, I see only two kinds of options:

1. Options that change what lean prints but not what it does
2. Options that make lean succeed or fail where it would not otherwise
3. Mostly unrepresented: Options that cause lean to change from one valid behavior to a different one

I don't see any in the third group, except possibly etaExperiment, and genInjectivity, genSizeOf which are for internal (bootstrap) use only

[Heather Macbeth]

An option which I'd like to set in a mathlib-dependent project is push_neg.use_distrib. This changes the behaviour of a tactic, so it would definitely break some proofs. Does this fall outside your classification?

[Mario Carneiro]

It would fall in the third group. You would definitely not want to set those kind of options in the extension

[Mario Carneiro]

Even changes to options in group 2 can be problematic, since it is confusing if you visit a file which apparently compiled successfully and it doesn't compile in the editor

[Mario Carneiro]

something like push_neg.use_distrib would mostly manifest as causing failures like group 2; it would be pretty rare for it to work anyway but produce a relevant difference (group 3)

[Moritz R]

@Mario Carneiro
would such a code action also be possible for match?
e.g. it would be very nice to be able to autogenerate a match for the constructors, like here for Lean.Expr:

def constInExpr (name : Name) (e : Expr) : Bool :=
match e with
| Lean.Expr.bvar _ => sorry
| Lean.Expr.fvar _ =>  sorry
| Lean.Expr.mvar _ =>  sorry
| Lean.Expr.sort _ =>  sorry
| Lean.Expr.const _ _ =>  sorry
| Lean.Expr.app _ _ =>  sorry
| Lean.Expr.lam _ _ _ _ =>  sorry
| Lean.Expr.forallE _ _ _ _ =>  sorry
| Lean.Expr.letE _ _ _ _ _ =>  sorry
| Lean.Expr.lit _ =>  sorry
| Lean.Expr.mdata _ _ => sorry
| Lean.Expr.proj _ _ _ =>  sorry

I think deleting the not-needed cases into a catch all is a much safer workflow, than adding them ontop of a catch-all, and autogenerating all constructors enables this.
Even better would be, if it wouldn't use _, but rather the original names (if there are any) used in the definition (if thats even possible)

[Mario Carneiro]

there is a code action for function types, so you can use : Expr -> Bool := _ and then apply the code action and edit it to what you want

[Moritz R]

oh thanks! Thats already pretty cool. I just wish we also had that for match - then i can keep my variables in the order i want (e.g. if expr wasn't the last one)

[Mario Carneiro]

the problem is that we don't have a way to say what the expression is, like the {! e !} holes in agda

[Mario Carneiro]

so it's unclear how to indicate what type we want to match on

[Moritz R]

i dont think i understand:
If i write
match e (with) isn't it clear from the type of e what the constructors of that type are?

[Mario Carneiro]

you're right, that's implemented for induction e already, I'll see what it takes to make that work

[Moritz R]

Also, what do you think about making the code action for function types also availible without writing the
:= _
and then deleting the unnessecarily generated := fun.

E.g. for writing

def pred : ℕ → ℕ
  | 0 => 0
  | n+1 => n

i would expect to be able to already autocomplete when only having written

def pred : ℕ → ℕ

not only after

def pred : ℕ → ℕ := _

(which generates )

def pred : ℕ → ℕ := fun
  | .zero => _
  | .succ n => _

but i want

def pred : ℕ → ℕ
  | .zero => _
  | .succ n => _

[Mario Carneiro]

the latter would be easier than the former

[Moritz R]

I think both would be optimal, though the version for match I think is much more important, since the workaround for it, is much more annoying

[Moritz R]

I would also be interested to take a shot at this myself, but i would need some pointers, for where to look for the exisiting implementation of the action for "induction n" and where the one for "match" would go

[Moritz R]

(im quite new to metaprogramming)

[Robin Arnez]

The induction and cases code actions are in https://github.com/leanprover-community/batteries/blob/main/Batteries/CodeAction/Misc.lean (at casesExpand)

[Alok Singh]

Mario Carneiro said:

the problem is that we don't have a way to say what the expression is, like the {! e !} holes in agda

reminds me of https://github.com/brendanzab/lean-holes

[Moritz R]

How do people get textual representations of anything?
f.e.

@[command_code_action]
def blabla : CommandCodeAction := fun CodeActionParams Snapshot ctx node => do
  let .node (.ofTacticInfo info) _ := node | return #[]
  logInfo m!"{info.goalsBefore}"

  let eagerAction : Lsp.CodeAction := {
    title := "My Always Visible Action"
    kind? := "quickfix"
  }

  return #[{ lazy? := none, eager := eagerAction }]

logInfo and dbg_trace fail - Is there any other options how i can see values of things?

[Aaron Liu]

Once upon a time I had to do this so I just put it in the title of the action

[Eric Wieser]

Does IO.eprintln work?

[Moritz R]

Eric Wieser schrieb:

Does IO.eprintln work?

This one gives

failed to synthesize
  ToString MessageData

[Moritz R]

Aaron Liu schrieb:

Once upon a time I had to do this so I just put it in the title of the action

I also get a clash from

type mismatch
  toMessageData "My Always Visible Action" ++ toMessageData info.goalsBefore ++ toMessageData ""
has type
  MessageData : outParam Type
but is expected to have type
  String : Type

[Aaron Liu]

Yeah I had a string representation, it wasn't a MessageData

[Aaron Liu]

(this was #lean4 > Macro vs. code action @ 💬 )

[Eric Wieser]

Right, my question was whether IO.eprintln "This is visible" is visible

[Eric Wieser]

You can deal with stringification once you've found a channel that you can send anything through

[Moritz R]

These both work:

  dbg_trace "blabla"
  IO.eprintln "This is visible"

But i cant get anything i actually want to know into it

[Aaron Liu]

What do you want to know? Maybe you can convert it into a string

[Moritz R]

e.g. what node : InfoTree contains

[Aaron Liu]

I had to hand-roll a toString function lol

[Aaron Liu]

I guess since you have access to the infotree could you just insert a node

[Moritz R]

Aaron Liu schrieb:

I guess since you have access to the infotree could you just insert a node

how would that help?

[Moritz R]

Aaron Liu schrieb:

I had to hand-roll a toString function lol

can you share it? ;)

[Eric Wieser]

Can you use docs#InfoTree.format ?

[Moritz R]

Eric Wieser schrieb:

Can you use docs#InfoTree.format ?

Yess!

[Moritz R]

more precisely in my context, this works:

let m ← InfoTree.format node ctx
dbg_trace m

[Moritz R]

For the pattern-completion of

def myfun : Nat → Nat → Nat

do we want an action to match against the second argument as well? i.e. generate smth. like

def myfun : Nat → Nat → Nat
  | _, .zero => _
  | _ , .succ n => _

If so, until which argument-number should we generate the action?

[Moritz R]

2025-06-16 12-24-24.gif
(sighs in relief)

[Jovan Gerbscheid]

That's really cool! But I would suggest using two spaces less indentation, so that the match and the | start at the same column.

[Moritz R]

good catch! - now fixed

[Moritz R]

Im not 100% happy with my implementation code, but i don't see a better way to do it -

[Moritz R]

Very open to feedback

[Moritz R]

Can somebody have a look at the code?
It's now public under https://github.com/MoritzBeroRoos/batteries

[Moritz R]

I think @Mario Carneiro is the expert for this

[Moritz R]

It seems Mario is busy, can maybe someone else have a look?

[Robin Arnez]

Could you open a PR? Then we can use the github review feature

[Mario Carneiro]

Note, this ended up in a slightly awkward position because I have already written half of the implementation and it handles a more general situation than your version, so I might replace this later. On the other hand, I didn't finish it and I don't want to block people for that reason, so I'd be okay merging your version in the meantime

[Moritz R]

I have opened a pull request at https://github.com/leanprover-community/batteries/pull/1307.
If this code is deemed ok, im fine with it only being merged and later replaced when mario finishes a more general version.

[Moritz R]

@Mario Carneiro does your generalized version already handle the implicit match as in

def myfun2 (n:Nat) : Nat <--(cursor here)

or should try to solve this?

[Moritz R]

Does anybody have any ideas for how to go from generating

def myfun : (n:Nat) : Bool :=
  match n with
  | .zero => _
  | .succ n => _

to generating

def myfun : (n:Nat) : Bool :=
  match n with
  | 0 => _
  | n + 1 => _

?

At the moment we just have annotations of definitions with [match_pattern]
which will then be unfolded in the matching, but i don't see any way to do anything nice backwards here.

Is there anything to say against hardcoding a few of the most common patterns?

[Jovan Gerbscheid]

I think it is reasonable to hard-code this special case.

[Moritz R]

Anyone have a clue why @[command_code_action Parser.Term.match] doesn't fire on anything i try?

[Mario Carneiro]

because that's not a command

[Mario Carneiro]

most of my half-implementation involved implementing term_code_action first

[Moritz R]

i see

[François G. Dorais]

FYI: @Moritz R 's batteries#1307 is ready for a final review.