Stream: Miscellaneous

Topic: lean infoview widgets


view this post on Zulip 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

view this post on Zulip Karl Palmskog (Apr 23 2023 at 08:26):

probably useful in teaching and documentation, most obviously together with Alectryon

view this post on Zulip Paolo Giarrusso (Apr 23 2023 at 12:03):

Wouldn't it be useful for a CAS-like application?

view this post on Zulip Huỳnh Trần Khanh (Apr 23 2023 at 17:53):

i dont get what you mean :)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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: Jun 13 2024 at 04:03 UTC