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)