Visualization Lean in VS Code

Stream: lean4

[Guilherme Silva]

I saw that it is possible to do a visualization of the Rubik's Cube in Lean:
https://github.com/leanprover/lean4-samples/tree/main/RubiksCube

However, I have seen that they made a good way of doing visualization in Racket:
https://youtu.be/EQCsw0HTO3A

Is it possible to do the same thing in Lean?

The idea is that each GUI visualization has a state that can be changed in the GUI. This state can also be changed in the editor.
I think that a difficult part of implementation is if, for example, I define the state as List Natural and I changed it in Gui to [1,2,3]. If Lean 4 is smart enough to transform [1,2,3] to "[1,2,3]" as a string in the code editor automated.

[Mario Carneiro]

Most of the moving parts for that already exist. The main thing that is missing is a way to write the changed state back into the lean file

[Mario Carneiro]

transforming [1,2,3] into "[1, 2, 3]" already exists, that's the ToString function

[Guilherme Silva]

Mario Carneiro said:

transforming [1,2,3] into "[1, 2, 3]" already exists, that's the ToString function

Do you know if toString work with all the types? If not, maybe it is necessary to make some restrictions to the type like (A : Type) [printable A].

[James Gallicchio]

It's managed by a ToString typeclass :)

[Johan Commelin]

@Guilherme Silva Is this roughly what you want https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/by.20interactive!

[Tomas Skrivan]

Also there is InteractiveSvg where the State can be anything having ToJson instance.

[Guilherme Silva]

Johan Commelin said:

Guilherme Silva Is this roughly what you want https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/by.20interactive!

I saw it. One thing that is missing is just changing the text editor from GUI.

[Guilherme Silva]

Mario Carneiro said:

transforming [1,2,3] into "[1, 2, 3]" already exists, that's the ToString function

I thought more about this. Maybe this toString is not necessary.
If Lean has some macro toExpr that works for all types and after, Expr -> String, it can be possible to extract the state and put it in the text editor.