dune build theories/Strings should do, I think.
Jason Gross has marked this topic as resolved.
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.
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?
@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