Code actions status

Stream: lean4

[Heather Macbeth]

What's the current status of the work on code actions? (cc @Edward Ayers @Wojciech Nawrocki). I am aware of the discussion on the RFC lean4#1494 from September, the merged PR lean4#1661 from October ("a low-level system for registering LSP code actions"), a discussion from November about the capabilities of that system, and a thread from December which digressed into a code actions wishlist (cc @Mario Carneiro).

There are a couple of mathlib3 features which I really miss in mathlib4, and which IIUC should be implemented as code actions:

• the clickable "Try this" for a suggestion (used in library_search, polyrith, squeeze_simp, ring, ...)
• the lightbulb which comes up on {!!} to fill in a skeleton for a structure

Do the code actions we have now permit the implementation of these features? I think that the lack of these two things is a significant enough degradation in the user experience that we should consider delaying the mathlib4 flag day until they are available.

Another important code action would be something which autogenerates the boilerplate for the Lean 4-style cases and induction. I would like to respect the wishes of the Lean 4 developers and use that style when I write Lean 4 code, but currently I find myself using the imitation-Lean-3 cases' and induction' just because they require so much less typing.

Of course, there are tons of other goodies we could get with code actions, and I'm excited about them too, but the things I mentioned above seem like priorities to me.

[Wojciech Nawrocki]

Something to note is that in LSP terminology code actions are specifically about something that appears inline in the editor (e.g. the lightbulb in VSCode), whereas "Try this" appears in the infoview and is thus not a code action (of course it is one in a broader sense of the term). I proposed one mechanism for it in lean4#2064 which faced some opposition, although after some offline discussions with @Gabriel Ebner I think we perhaps worked out a solution that would make everyone happy (?). I am happy to look into it again in about two weeks or so.

[Wojciech Nawrocki]

As for lightbulbs, as far as I remember the current infrastructure is basically already sufficient to implement something like {!!} expansion as a metaprogram that lives in mathlib4. There will certainly be rough edges to improve that can be fixed in core.

[Heather Macbeth]

Thanks for the update @Wojciech Nawrocki !

[Scott Morrison]

Something I would like to have is automatically running tactics (do I have too many CPUs...?). i.e. whenever VSCode can see that a proof is incomplete at the current cursor, it tries running something (e.g. library_search, or hint when we port it) in the background. If it succeeds, it would show a try this (or a light bulb, or greyed-out text at the cursor, tab-completion, etc).

If I'm not on battery power, and not all my CPUs are maxed out, and I have an incomplete proof, surely library_search et al. should be running!

[Jireh Loreaux]

wouldn't that disrupt the infoview?

[Johan Commelin]

If so, that's a UX problem that can be solved.

[Wojciech Nawrocki]

We can run asynchronous computations in the infoview these days, so it shouldn't disrupt the infoview UI per se. It would however drain your battery rather quickly and max out your CPU, as Scott notes. As a middle ground, one could implement a widget with a toggle such that when the toggle is 'on', tactics would run in the background; otherwise not.

[Scott Morrison]

I don't know anything about running stuff in the infoview. Can anyone point me to some existing code that is closest (even if far away) to what I want: inspect the goal, run a tactic, display something the infoview based on the result?

[Wojciech Nawrocki]

@Scott Morrison the only resource we have at the moment is the user widgets tutorial which you can also load in Lean 4 Web. It's possible to implement what you want analogously to the #check as a service example. However, the user widgets system is designed to be the bare minimum needed in Lean core to get things working, so this implementation would have to be super low-level. In particular, in order to run a tactic using a goal state you'd first need to retrieve the goal state from a command snapshot manually. Here is an example. Alternatively, you could wait on the higher-level goal display API coming to ProofWidgets4 sometime in the near future™ (I will be working on this in two weeks or so).