Stream: Coq workshop 2020

Topic: [S4] The Coq Proof Script Visualiser (coq-psv)


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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 05 2020 at 13:30):

Tool session will start at 16:00 Paris time

view this post on Zulip Mario Frank (Jul 05 2020 at 13:33):

à priori: project page of Coq-psv is http://cs.uni-potsdam.de/coq-psv

view this post on Zulip Mario Frank (Jul 05 2020 at 13:53):

bump

view this post on Zulip Clément Pit-Claudel (Jul 05 2020 at 14:15):

My, jsCoq is looking sharp these days :)

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

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

view this post on Zulip Yves Bertot (Jul 05 2020 at 14:21):

Never mind.

view this post on Zulip Yves Bertot (Jul 05 2020 at 14:22):

I like Clément's idea.

view this post on Zulip Yves Bertot (Jul 05 2020 at 14:22):

How do you handle modification of existing tactics?

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

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

view this post on Zulip 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: Feb 06 2023 at 07:03 UTC