Interactive Svg

Stream: lean4

[Tomas Skrivan]

With a huge help from @Edward Ayers I have created IteractiveSvg structure that allows you to easily create an interactive svg widget.

The structure definition is:

structure InteractiveSvg (State : Type) where
  init : State
  frame : Svg.Frame
  update (time_ms Δt_ms : Float) (action : Action)
         (mouseStart mouseEnd : Option (Svg.Point frame))
         (selectedId : Option String) (getSelectedData : (α : Type) → [FromJson α] → Option α)
         : State → State
  render (mouseStart mouseEnd : Option (Svg.Point frame)) : State → Svg frame

Where

• State is any custom type that has to be convertible from/to Json.
• init is initial value of the state
• frame contains information how to convert position in floats to pixels
• update function that is run every time step or on mouse event. The argument getSelectedData allows you to retrieve any custom data stored on a svg element that is currently selected
• render function converting State to svg

---

Code repository is https://github.com/EdAyers/WidgetKit

The build is still a bit fragile but this works for me

cd widget; npm install; cd ..
lake build widgets
lake build

Then open WidgetKit/Demos/InteractiveSvg.lean and when you place cursor on #widget svgWidget (toJson init) you should see:

ezgif-1-bfe8cf464d.gif

[Patrick Massot]

This looks very nice, but could you elaborate on the applications you have in mind?

[Tomas Skrivan]

I have few examples of simulations/computations using SciLean underway. For example I want to make interactive applets like in this article on Bezier curves.

[Tomas Skrivan]

Also merging this with @Joachim Breitner 's by interactive tactic would be interesting. This would allow you to create a custom interactive tactic without writing javascript.

[Shreyas Srinivas]

Tomas Skrivan said:

I have few examples of simulations/computations using SciLean underway. For example I want to make interactive applets like in this article on Bezier curves.

Is there a similar way to visualise graphs (I mean graphs with vertices and edges)

[Tomas Skrivan]

For me, the motivation is that I do not know any javascript and not too interested in learning it right now. However, I still wan to create my own widgets, so I just want something allowing me to draw points, lines, circles, ... and I will do everything from Lean

[Shreyas Srinivas]

Even static visualisations would very helpful in describing graph theoretic constructions

[Tomas Skrivan]

Sure, the InteractiveSvg allows you to draw any svg, so points, circle, lines and you can build a graph from that.

[Tomas Skrivan]

But you have to specify all vertex positions yourself. Which can be difficult if you have only the combinatorial description of a graph.

[Patrick Massot]

Does the interactive svg talk to Lean or is information only going one way?

[Shreyas Srinivas]

Ah I see. So this is something like tikz in that case. If it is interactive, and the gif is something to go by, then this should not be an issue. Are you taking feature requests at this time?

[Shreyas Srinivas]

In any case, thanks a lot for this wonderful tool

[Tomas Skrivan]

Shreyas Srinivas said:

Ah I see. So this is something like tikz in that case.For my particular use case. If it is interactive, and the gif is something to go by, then this should not be an issue. Are you taking feature requests at this time?

Not really, this is a result of hackathon in Freiburg and I won't have time to touch this too much in the next 3 months. So I'm taking only pull requests :) but I'm happy to help and answer questions.

[Tomas Skrivan]

Patrick Massot said:

Does the interactive svg talk to Lean or is information only going one way?

Depends what do you mean by that. The InteractiveSvg.update is a Lean function, so you can call any Lean code when you update the svg.

Currently there is no way to modify the environment, e.g. add new declaration, or talk to language server protocol. But I would really like to merge it with Joachim's interactive! tactic that can talk to lsp.

[František Silváši 🦉]

Beautiful.

[Tomas Skrivan]

Visualization of De Casteljau's algorithm to evaluate Bezier curve
bezier.gif

Code in SciLeanExamples repository

[Tomas Skrivan]

bezier.gif
Ohh I cut the gif short when converting from mp4