Huỳnh Trần Khanh (Apr 23 2023 at 03:51): Huỳnh Trần Khanh (Apr 23 2023 at 03:51):they now have a turnkey tool to display complex visualizations in the infoview https://github.com/EdAyers/ProofWidgets4. in your view, is this useful for coq users? my opinion is i like the idea, but I'm skeptical of its usefulness
Karl Palmskog (Apr 23 2023 at 08:26):probably useful in teaching and documentation, most obviously together with Alectryon
Paolo Giarrusso (Apr 23 2023 at 12:03):Wouldn't it be useful for a CAS-like application?
Huỳnh Trần Khanh (Apr 23 2023 at 17:53):i dont get what you mean :)
Huỳnh Trần Khanh (Apr 23 2023 at 18:07):I'm conflicted. on one hand the widgets are quite beautiful and i believe they're a nifty use of the JavaScript ecosystem. on the other hand if i need to visualize something it might be faster and more flexible to just use pen and paper. and additionally the widgets take up a decent amount of space. if they were to become pervasive I'd argue the user experience would be degraded
Paolo Giarrusso (Apr 24 2023 at 01:36):From their README
We have good support for building diagrams with Penrose, and expose some Recharts components for plotting functions and other kinds of data.
Seems useful for plotting functions like CAS (computer-algebra systems) do, Coq has libraries for doing it correctly
alternative and domain-specific goal state displays
That describes proof modes for custom embedded logics like Iris, I definitely refuse to stick to pen and paper for that
Your post seems to say that this library can be misused. I'm sure that's true, I'm less sure we'll actually write so much bad code.
Karl Palmskog (Apr 24 2023 at 06:48):for verified plotting, there are no less than two different solutions in Coq: https://coq.discourse.group/t/interval-4-2-now-with-plotting/1248
Paolo Giarrusso (Apr 24 2023 at 08:42):yes, I was thinking of that; such widgets might have UX upsides over "run gnuplot"
Last updated: Oct 13 2024 at 01:02 UTC