Stream: Coq users

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


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

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

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

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

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

view this post on Zulip cexpress (Jul 14 2023 at 12:27):

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

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

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

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

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

view this post on Zulip 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: Jun 23 2024 at 05:02 UTC