Wojciech's Widget Wishlist

Stream: general

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

Hi! I am one of the developers of user widgets and ProofWidgets4. While I was working on these systems, I have accumulated a wishlist of features related to Lean's UI/UX that could improve everyone's experience. In this post I wish to share the list with the Lean commmunity. While I do not have time to implement most of the items there, I am happy to provide mentoring, review PRs, etc. So if you are interested, do pick up an item, post here or DM me if you have questions, and write some code :)

The items are listed below; feel free to react to ones you would find most useful.

Please note that for items that touch core Lean and don't already have an issue assigned, an RFC must be made first in accordance with the contribution guidelines.

[Eric Wieser]

Could I suggest splitting these into separate messages in this thread to collect reactions on each?

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

Structure-aware syntax editing

All widgets and code actions that modify code in some way currently operate on strings; e.g. when we edit apply? to apply theBestLemma via a code action, we produce the string "apply theBestLemma" together with positioning information regarding where to insert it. While we do have to produce a string eventually as that is what editors expect, it is tragic that this is also the high-level API in widget/code action implementations; instead, there should be an API that allows users to conveniently modify structured docs#Lean.Syntax objects and generate stringly-typed edits from that (e.g. by diffing two Syntax objects). A reasonable starting point might be to look at any tactic which directly produces strings representing source code - e.g. conv? - and see what it would take to operate on structured syntax there.

Repos: mathlib4/possibly upstream to lean4

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

Commutative diagrams

Mathlib contains a commutative diagram widget (docs#Mathlib.Tactic.Widget.mkCommDiag) which is not used by anyone, including the author (me). The task is to write a replacement with better UX, addressing the issues described here, and bring it to mathlib. A starting point might be this widget which I have written for myself while working on polynomial functors. I have found it more useful than the mathlib version.

Repos: mathlib4/possibly ProofWidgets4

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

Semantic highlighting in the tactic state

It's 2025, yet types in the infoview are still black-and-white. Add support for semantic highlighting of syntax there. Likely requires somewhat invasive changes to the infoview extension and the RPC method signatures. One idea would be to extend docs#Lean.Widget.CodeWithInfos to use tags in SubexprInfo | SemanticToken. The Final Pretty Printer may contain good ideas on how to structure something like this.

Repos: lean4/vscode-lean4

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

Finer-grained visual diffs

The diffing algorithm for goals is useful, but coarse. For instance, in

example (h : 10 = 11) : let a := 10; True := by
  rw [h]
  sorry

the entire goal, rather than just the subterm 10, is highlighted in red. The task is to identify where finer/more accurate diffs can be provided, and then do so. See docs#Lean.Widget.exprDiffCore.

Repos: lean4/maybe vscode-lean4

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

Visual diffs for expected/actual type

The 'has type A but is expected to have type B' error message does a lot of heavy lifting when informing users about mistakes. Although Lean does a relatively good job of filling in implicit parameters so that the difference between A and B can be found, this is still not an easy task when the two types are long. We already have an expression diffing algorithm - the red/green highlights on tactic states - and components to display diffs visually. The task is to bring this to the 'has type .. but is expected to have type ..' message, perhaps hidden behind an option for users who do not want it. This may be implementable using a widget message.

Repos: lean4/vscode-lean4

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

Widget to debug unification failures

In a similar spirit to the issue above, improve the UX for 'could not unify the type of t A with the goal B'. Straightforward diffing probably does not make sense here because A often contains metavariables, but it could be useful to gain the ability to, for example, click on a subterm of A and a subterm of B and see why they could not be unified. (Tracing trace.Meta.isDefEq can already help here to an extent, but it would be more efficient to click around. The widget might also auto-scroll to the relevant subtrace of trace.Meta.isDefEq when we click on a subterm of A or B.)

Repos: lean4/vscode-lean4

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

Allow widgets to modify the selection context

Goals in the infoview come with an associated selection context - a list of terms selected by the user with shift-click or the right-click menu (see section 3.2. of our paper). Right now, user widget JS code may not modify the selection context. This makes building visual provers such as EuclideanConstructions awkward because the user may not select a circle C by clicking on it in the plane, but rather has to click on C in the tactic state. The task is to allow widgets to modify selection contexts. This probably requires a technical understanding of the infoview code, in particular regarding how goals and the tactic state are represented.

This task is also a key enabler for fully custom tactic states, i.e., widgets that replace the tactic state entirely. Selection contexts must be widget-modifiable for that to work.

Repos: vscode-lean4

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

Finally, I wanted to highlight some tasks that already have issues assigned.

Clickable infoview links

Implement vscode-lean4#631.

Repos: vscode-lean4

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

Make 'Try this' use a widget message

Implement lean4#4551.

Repos: lean4

[Julian Berman]

(If/when anyone works on any of the UI-side parts of these I'd certainly also appreciate a ping on the PR so I can bring them to lean.nvim as well.)