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.

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.

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

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

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

Last updated: Oct 04 2023 at 21:01 UTC