Widgets

[leodemoura]

Lean 3 supports tactic state widgets on VS Code, with context information (hypotheses, goals) at each point in a proof / definition,
"expected type" widgets display the context for subterms, the types of subterms in the context can be inspected interactively.
the "All Messages" widget, which shows all info, warning, and error messages from the Lean server, and other custom widgets can be rendered in the info view.

We can do much better in Lean 4 because messages, traces, and all server information are Lean objects that can be traversed and inspected.

[enjoysmath]

I am interested in helping this, on anything that helps achieve the possibility of comutative diagrams with feedback into Lean (but not necessary to start with). So for instance clicking to add in an arrow will declare an arrow in your source code for you! So you can draw diagrams with non-keyboard peripherals, or like in Blade Runner ("Arrow A_1 to D_3; Enhance.") i.e. with voice commands. That would be awesome. So I'm all about widgets. I have 8 years of PyQt5 experience (so I can code on large projects confidently iow) and about < 3 years with Django / Javascript. The Javascript / HTML / CSS experience I have will most likely be what you're looking for. I'm in the process of learning how to code in Lean4 as a new person to Lean. I'll probably be ready to take on Widget library knowledge in about 5 months or less. I'll subscribe to this thread in case you ping me regarding this.

[leodemoura]

@Vtec234 Do you see any reason for keeping this issue open? You have ideas to make the current implementation better, but we have merged your PR a long time ago.

[Vtec234]

@leodemoura I think it's okay to close this. We are currently working on dynamic loading of JavaScript code in the infoview and will later come up with a more concrete RFC for user-programmability, at which point we can make a new issue/PR.