leanprover-community
a demo for geogebra diagram
A demo renders a Geogebra applet for dynamic visualization based on the goal state in the infoview.
Hey, thanks for this PR! Using Geogebra is a cool idea, and loading it via an injected <script>, although hacky, at least avoids #19. But I think before we can merge this, the implementation should be improved. My main concern is that the goal is first turned into a string, and then the string is parsed back into a set of constraints. This appears quite counterproductive given that InteractiveGoals already gives us a structured and complete representation of the tactic state. It is also easy to break: for instance, write let abc := "between !" in the tactic script to break the between parser. It would be better if this did something along the lines of isEuclideanGoal? from Euclidean.lean instead, either in TypeScript or in Lean.
