Ankit Pradhan (Jan 30 2023 at 02:48): 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.
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.
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
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
Ankit Pradhan (Feb 16 2023 at 19:19):Thanks for the suggestions! Will try out serapi and lsp.
Last updated: Apr 19 2024 at 21:01 UTC