Stream: Coq devs & plugin devs

Topic: ✔ dev/shim/coqtop inconsistent assumptions

view this post on Zulip Rodolphe Lepigre (Sep 11 2023 at 16:02):

dune build theories/Strings should do, I think.

view this post on Zulip Jason Gross (Sep 11 2023 at 16:20):

Thank you!

view this post on Zulip Notification Bot (Sep 11 2023 at 16:20):

Jason Gross has marked this topic as resolved.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 11 2023 at 20:09):

Indeed @Jason Gross as of today with the shims you are required to build before calling coqtop, dune coq top tries to provide a better workflow.

view this post on Zulip Jason Gross (Sep 12 2023 at 00:43):

Hm, I did dune build -p coq-core,coq-stdlib,coqide-server,coqide, and then I did dune exec -- dev/shim/coqtop; does this leave things in an inconsistent state somehow?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 12 2023 at 18:06):

@Jason Gross yes, the first command will build _release_ versions of all the packages, usable from their specified -prefix or from _build/install if you let Dune auto-generate the prefix.

The second command will build _development_ versions of the minimal amount of binaries and files as to load the prelude, these are different so Coq will complain about wrong md5sums.

You can do dune exec --profile=release -- dev/shim/coqtop to correct this.

Last updated: Nov 29 2023 at 22:01 UTC