Announcing ProofWidgets4

Stream: lean4

[Wojciech Nawrocki]

Hi everyone! @Edward Ayers, @Gabriel Ebner and I are happy to announce the initial release of ProofWidgets4, a library adding support for custom interactive extensions to the infoview using the user widgets mechanism built into Lean. Our paper covering some of the ideas behind the Lean 4 infoview and ProofWidgets4 will be presented at ITP 2023, and a draft can be found here.

ProofWidgets4 is better shown than explained, so here are some things you can visualize and do with it:

• Display data structures symbolically
  
• Work with commutative diagrams
  
• Inspect set relations
  
• Generate conv mode invocations
  
• Equip interactive tactics such as Sagredo with user interfaces

And here are some new features we added:

• Depending on ProofWidgets4 does not pull in JS build tools as a dependency by default thanks to support for cloud build caching in Lake
• Builtin support for JS libraries including Penrose and Recharts
• Component Props API for giving widget components Lean types
• JSX-like syntax so you can write what looks like HTML in Lean
• Dynamic loading of JS modules with importWidgetModule and DynamicComponent (which was requested here)
• .. many technical improvements

Do give it a try! We especially welcome bug reports, contributions (there are a few issues marked with 'good first issue' in the repository), and well-motivated feature requests.

[Siddhartha Gadgil]

Does this support using the widget to make changes to the text in the editor?

[Evgeniy Kuznetsov]

@Wojciech Nawrocki, you may want to add tags lean and lean4 to your repository

[Eric Rodriguez]

I see that the lakefile does not require Mathlib - is it possible that we could make Mathlib depend on ProofWidgets in future?

[Wojciech Nawrocki]

Siddhartha Gadgil said:

Does this support using the widget to make changes to the text in the editor?

Yeah, this part is essentially the same as with user widgets. For example the conv demo does it.

[Wojciech Nawrocki]

Eric Rodriguez said:

I see that the lakefile does not require Mathlib - is it possible that we could make Mathlib depend on ProofWidgets in future?

That would be possible, yes :)

[Scott Morrison]

I think a PR to mathlib4 that implemented the "Try this" code actions via ProofWidgets would receive an enthusiastic welcome. :-)

(I'm biased here, as I want ProofWidgets imported into mathlib4 so sagredo can use it.)

[Yaël Dillies]

From the side of the people who didn't write sagredo, I too want those fancy widgets in mathlib!

[Andrés Goens]

is there any hope whatsoever for this to work in emacs?

[Henrik Böving]

I guess if we embed a web browser in emacs^^

[Wojciech Nawrocki]

Andrés Goens said:

is there any hope whatsoever for this to work in emacs?

A while ago I conjectured a concrete plan for how that could work, but so far no one has attempted an implementation, as far as I know. One disadvantage of the plan is that it's quite specific to the emacs GUI, requires native, platform-specific code for emacs-webkit, and emacs-webkit itself has not received maintenance since 2021. A potential alternative, which would even work with terminal-based emacs when the terminal emulator is running in an otherwise graphical environment, would be to spawn a separate browser window (probably electron or something like it) and orchestrate its behavior from within emacs.

[Siddharth Bhat]

Heya, this is super cool! I've been playing around with this, and as a consumer of the library, I have one question:

How do I reuse the lakefile scripts that builds the .tsx from ProofWidgets4? I currently have copy-pasted the code for the widgetJsAllTarget, since I did not spend the cycles figuring out how to invoke a target (widgetsJsAll) from a library dependency (ProofWidgets4). @Mac , is there a simple API to do this?

I think the target widgetsJsAll might also benefit from being slightly more general, as IIUC, it currently hardcodes the paths for the widgets as widgets/.

[Wojciech Nawrocki]

@Siddharth Bhat providing nice Lake integration for building widgets is a future work item. Copy-pasting the build script is the only workable solution at the moment, unfortunately. I think a solution may require some minor additions to Lake around module facets. Contributions are always appreciated!

[Tomas Skrivan]

Having an interface to something like polyscope would be super cool!

Today I have done a nice visualization of basic geometric shapes used to build finite elements. I have bunch of functions allowing to iterate over faces, the animation shows iteration over all two dimensional faces for all the basic shapes up to dimension 4.
Peek-2023-04-25-14-55.gif

[Siddharth Bhat]

@Tomas Skrivan where's the code? :D

[Tomas Skrivan]

Siddharth Bhat said:

Tomas Skrivan where's the code? :D

here :)

[Kevin Buzzard]

I'm trying to debug a simp failure in the port and I have a conjecture that

F.map (𝟙 j, 𝟙 k'') (F.map (𝟙 j, i (𝟙 j)) (F.map (𝟙 j, gf (𝟙 j)) (F.map (𝟙 j, g j) (y j)))) =
F.map (𝟙 j, 𝟙 k'') (F.map (𝟙 j,           g ≫        gf (𝟙 j) ≫ i     (𝟙 j))     (y j))

Is there any way that I can get widgets to draw me a picture? here is my exact problem. If we had an extract_goal tactic, this would be much easier to minimise. Right now I'm working on it on paper. NB CI is only failing on the build because the file has a sorry in it, so the import in Mathlib.lean fails with an error. (I couldn't figure out how to install widgets on my machine, I opened an issue).

[Wojciech Nawrocki]

Is there any way that I can get widgets to draw me a picture?

Yes, but someone would have to write a metaprogram which "knows" about functoriality in order to draw diagrams where the top-level terms are not directly compositions but rather compositions taken through a functor. At a very high level I think it could be an @[expr_presenter] that looks at the term, and if the term has F.map applications on both sides, strips them and draws the diagram without the Fs, then readds the Fs.

[Scott Morrison]

What even is the appropriate graphical calculus here for functors to/from cartesian products?

[Adam Topaz]

I think in this case the morphisms are in Type _ (i.e. functions) and are being applied to some element ((y j)). So one would also have to extract the relevant categorical compositions

[Mac Malone]

Siddharth Bhat said:

I did not spend the cycles figuring out how to invoke a target (widgetsJsAll) from a library dependency (ProofWidgets4). Mac , is there a simple API to do this?

Unfortunately, the answer is currently a bit clunky:

let some pkg <- findPackage? `ProofWidgets4 | error "no such package"
let targetName := `widgetsJsAll
let some config := pkg.findTargetConfig? targetName | error "no such target"
let job := config.getJob (← fetch <| pkg.target targetName)

I will wrap the target job stuff into a nice single convenience function on the package (probably pkg.fetchTarget?) and release it when I jump back into Lean soon (hopefully next week).

[Mac Malone]

@Wojciech Nawrocki I noticed the ProofWidgets4 tactic keywords do not follow the snake case convention. Is that deliberate?

[Wojciech Nawrocki]

Mac said:

Wojciech Nawrocki I noticed the ProofWidgets4 tactic keywords do not follow the snake case convention. Is that deliberate?

No, that's a bug. Thanks :)

[Siddharth Bhat]

One may be pleased to know that the stanford bunny loads now :)

image.png

@Wojciech Nawrocki , couple of questions about how to use ProofWidgets4 to render complex objects like meshes:

1. Can we save the state of the widget, such that when the user returns to the widget, the camera angle remains saved in the widget state? Right now, it seems like intra-widget state is wiped away. Similarly, the state of the slider in the Rubik's cube example is reset when one moves the cursor away from the widget and comes back.

2. I currently load meshes from disk and masquerade the IO Mesh as a Mesh via a terrible hack:

https://github.com/bollu/polyscope.lean/blob/master/Main.lean#L160-L167
-- | Actually do the IO. This incurs an `unsafe`.
unsafe def unsafePerformIO [Inhabited α] (io: IO α): α :=
  match unsafeIO io with
  | Except.ok a    =>  a
  | Except.error _ => panic! "expected io computation to never fail"

-- | Circumvent the `unsafe` by citing an `implementedBy` instance.
@[implemented_by unsafePerformIO]
def performIO [Inhabited α] (io: IO α): α := Inhabited.default

def bunny : MeshProps := performIO <| loadMeshFromOffFile "./data/bunny.off"
#html <Mesh vertices={bunny.vertices} faces={bunny.faces} />

Is there a cleaner way to build top-level definitions that can be #htmld? It would really great from an API perspective if I could say #htmlIO, which would run the IO Mesh and render the Mesh if the mesh loaded successfully, and catch the IOError and display the error if the computation failed.

[Wojciech Nawrocki]

Can we save the state of the widget, such that when the user returns to the widget, the camera angle remains saved in the widget state?

Yeah, the entire React component including its state is destroyed when it is no longer in view. Note that state is preserved when moving the cursor between different positions that contain the same widget (e.g. moving around in a proof where the whole proof displays a single custom goal state widget).

I haven't thought about how to persist widget state beyond this; there is in general a tension between which parts of the UI are authoritative and which are "pure functions" of the authoritative parts. I fear that putting too much state in the UI will make it too easy to lose that state, so it is preferrable for the proof script to determine many parameters of the display. On the other hand some more transient parameters such as the collapse-state of collapsible panels, and camera angles like here, may well be worth preserving.

There is no API to do that currently; we could think about adding one. As a hack you could rely on the fact that widget JS modules are loaded once and store whatever you need in a global let in your JS script (I haven't tested this though, so there may be some obstacle preventing it from working). Beware that if you do this, the global let is shared between all instances of your component if you display more than one.

[Wojciech Nawrocki]

Is there a cleaner way to build top-level definitions that can be #htmld?

For loading data off disk and storing it in a Lean definition, you can copy the definition of the include_str elaborator and make it store whichever type you care about.

It would really great from an API perspective if I could say #htmlIO

I think this would become possible with a combination of lean4#1967 and lean4#2064.

[Siddharth Bhat]

Thanks for the help!

---

.As a hack ...

I think I shall avoid hacks for as long as possible :D

---

you can copy the definition of the include_str elaborator and make it store whichever type you care about.

Thanks, I'll try this!

---

I think this would become possible with a combination of lean4#1967 and lean4#2064.

Let me try to understand. Is it that lean4#2064 allows the widget to throw the error when the IO action fails, and lean4#1967 will give us MetaEval (IO a) instances, so I ought to be able to say #html bunnyIO, which can be evaluated via MetaEval and then rendered?

[Wojciech Nawrocki]

Is it that lean4#2064 allows the widget to throw the error when the IO action fails, and lean4#1967 will give us MetaEval (IO a) instances, so I ought to be able to say #html bunnyIO, which can be evaluated via MetaEval and then rendered?

The idea would be that lean4#1967 allows MetaEval (MetaM a) in such a way that messages produced using logInfo by the MetaM computation are shown as messages in the infoview, and lean4#2064 proposes being able to put widgets in MessageData. But barring all that it shouldn't be too hard, I think, to just write a #htmlIo elaborator without making any changes to core.

[Wojciech Nawrocki]

Here is an unchecked implementation.