This is the topic to ask questions on the talk "The Coq Proof Script Visualiser (coq-psv)".
Tool session will start at 16:00 Paris time
à priori: project page of Coq-psv is http://cs.uni-potsdam.de/coq-psv
My, jsCoq is looking sharp these days :)
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?
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.
I like Clément's idea.
How do you handle modification of existing tactics?
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.
@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.
@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: Feb 06 2023 at 07:03 UTC