Stream: Coq users

Topic: Proof View dump


view this post on Zulip Ankit Pradhan (Jan 30 2023 at 02:48):

Is there a way to dump the entire proof view (after stepping through a tactic application) for all tactics in a file so as to analyze the diff hypotheses and proof state generated after executing each tactic.

view this post on Zulip Mycroft92 (Jan 30 2023 at 12:46):

Hey Ankit,
Try https://github.com/cpitclaudel/alectryon maybe? It has a very clean way interface that allows you to explore the proof state on hover over a specific step in the proof.

view this post on Zulip Ana de Almeida Borges (Jan 30 2023 at 12:54):

You might be interested in the built-in diff: https://coq.inria.fr/refman/proofs/writing-proofs/proof-mode.html#showing-differences-between-proof-steps

view this post on Zulip Emilio Jesús Gallego Arias (Jan 30 2023 at 18:31):

@Ankit Pradhan indeed Aletryon uses serapi, you can use coq-serapi or any of its bindings, or serapi succesor coq-lsp

view this post on Zulip Ankit Pradhan (Feb 16 2023 at 19:19):

Thanks for the suggestions! Will try out serapi and lsp.


Last updated: Jun 16 2024 at 03:41 UTC