Stream: Coq users

Topic: See all steps to Qed together in Interactive ProofView?

cexpress (Jul 13 2023 at 18:10):

This may be a naive question, but just wanted to know whether this was possible.

In the following attached screenshot, I am in Line 1125, and on the proof view panel, I see the result of stepping through Line 1125.
However, what if I also want to see what the result was in Line 1124? That is, is it possible to see every change/rewrite/result
during proof statements in the panel all at once? I think having all the simplification steps at the same time will aid my understanding.

Selection_1267.png

Thanks for any pointers/help.

James Wood (Jul 13 2023 at 19:40):

Do you mean seeing multiple goal displays at once? As far as I know, the best you can do is to copy each one into a text file as you see it. There's no support in the interface for seeing multiple goal displays.

James Wood (Jul 13 2023 at 19:41):

On the other hand, if you're not bothered with seeing intermediate goals, you can replace some .s by ;s to turn several commands into a single command.

cexpress (Jul 13 2023 at 19:49):

Yes, I meant seeing each intermediate goal displayed as part of a list or something.

Thanks for the clarification, and the tip (;) -- wasn't aware of that.

Ana de Almeida Borges (Jul 14 2023 at 10:18):

You can also enable proof diffs, see this part of the manual: https://coq.inria.fr/refman/proofs/writing-proofs/proof-mode.html#showing-differences-between-proof-steps

cexpress (Jul 14 2023 at 12:27):

@Ana de Almeida Borges That's really interesting, thanks for sharing. Will try it out.

cexpress (Jul 14 2023 at 12:31):

Tried it out - and it works really nicely in CoqIDE; although in VSCoq - the setting seems to have no effect, and the diff is not shown correctly.

cexpress (Jul 14 2023 at 12:32):

Please let me know if there's any trick to make it functional in VSCoq, because I'd rather use VSCode.

James Wood (Jul 14 2023 at 12:40):

In VSCode, it's probably somewhere in the VSCoq settings. IIRC, VSCoq largely ignores the vernacular commands for changing IDE settings.

cexpress (Jul 14 2023 at 12:50):

Have enabled the settings already. Restarted VSCode, etc.

Just opened an issue in Github - let's see whether the extension author/maintainer has any insights: https://github.com/coq-community/vscoq/issues/525

Notification Bot (Jul 14 2023 at 14:16):

This topic was moved to #VsCoq devs & users > See all steps to Qed together in Interactive ProofView? by Karl Palmskog.

Last updated: Oct 13 2024 at 01:02 UTC