Théo Zimmermann (Jun 24 2020 at 11:19): Théo Zimmermann (Jun 24 2020 at 11:19):This is the topic to ask questions on the talk "The Coq Proof Script Visualiser (coq-psv)".
Emilio Jesús Gallego Arias (Jul 05 2020 at 13:30):Tool session will start at 16:00 Paris time
Mario Frank (Jul 05 2020 at 13:33):à priori: project page of Coq-psv is http://cs.uni-potsdam.de/coq-psv
Mario Frank (Jul 05 2020 at 13:53):bump
Clément Pit-Claudel (Jul 05 2020 at 14:15):My, jsCoq is looking sharp these days :)
Yves Bertot (Jul 05 2020 at 14:19):I would think that an intermediate data-structure that is independent of Latex would be useful to many people. To you plan to document this data format?
Clément Pit-Claudel (Jul 05 2020 at 14:21):Did you consider using source annotations for users to pick which goals to show and which goals to hide? I use something like that:
Goal True /\ True.
split.
- (* .show *)
idtac "hello". (* .no-goals *)
apply I.
- (* .show *)
auto.
Qed.
Never mind.
Yves Bertot (Jul 05 2020 at 14:22):I like Clément's idea.
Yves Bertot (Jul 05 2020 at 14:22):How do you handle modification of existing tactics?
Mario Frank (Jul 05 2020 at 14:24):The data structure is currently only an OCaml type, which I show at the end of the slides. It is rather not optimal since I try to support all branching possibilities of Coq. But exposing this data structure is definitely possible.
Mario Frank (Jul 05 2020 at 14:26):@Clément Pit-Claudel I already thought about source annotations. When I started to implement the tool, it was a plugin first and I used such annotations. But then I had some problems with getting vital information about the proof, so I switched to the command line tool concept. Source annotations are definitely a topic as soon as I integrate the functionality into CoqIDE.
Mario Frank (Jul 05 2020 at 14:28):@Yves Bertot I currently do not handle it explicitely, but what exactly do you mean? Modification by integrating trailing singleton clear, for example?
Last updated: Jun 10 2023 at 23:01 UTC