Euclidean geometry diagram in InfoView?

Stream: general

[Weiyi Wang]

This is just a random idea I had. How feasible it is to show diagram in InfoView for Euclidean geometry, based on the definition and hypothesis in the current proof state?

[Mirek Olšák]

https://github.com/leanprover-community/ProofWidgets4/blob/main/ProofWidgets/Demos/Euclidean.lean

[Mirek Olšák]

I would prefer if the diagram data (coordinates) were also present on Lean side, and could be manipulated with. An interaction with the infoview picture (like geogebra) would be certainly possible (infoview can run arbitrary typescript, or even Lean code). A difficulty is where do we store the modified picture... Although the infoview can edit the Lean file, it is not super-reliable...