Zulip Chat Archive

Stream: lean4

Topic: Interactive Svg


Tomas Skrivan (Nov 21 2022 at 12:23):

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 (Nov 21 2022 at 12:33):

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

Tomas Skrivan (Nov 21 2022 at 12:35):

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 (Nov 21 2022 at 12:37):

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 (Nov 21 2022 at 12:40):

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 (Nov 21 2022 at 12:40):

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 (Nov 21 2022 at 12:41):

Even static visualisations would very helpful in describing graph theoretic constructions

Tomas Skrivan (Nov 21 2022 at 12:42):

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

Tomas Skrivan (Nov 21 2022 at 12:43):

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 (Nov 21 2022 at 12:49):

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

Shreyas Srinivas (Nov 21 2022 at 12:51):

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 (Nov 21 2022 at 12:53):

In any case, thanks a lot for this wonderful tool

Tomas Skrivan (Nov 21 2022 at 12:54):

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 (Nov 21 2022 at 12:56):

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 🦉 (Nov 21 2022 at 13:30):

Beautiful.

Tomas Skrivan (Nov 21 2022 at 18:17):

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

Code in SciLeanExamples repository

Tomas Skrivan (Nov 21 2022 at 18:22):

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


Last updated: Dec 20 2023 at 11:08 UTC