Sorry, this is probably a naive question: I'd like to build stdlib and run coqide using dune
What I did: make -f Makefile.dune world && dune exec dev/shim/coqide-prelude
Unfortunately, the second command triggered some recompilation and now Require Import
on an stdlib file complains about inconsistent assumptions.
We should have something to disable those checks, they're way too sensitive
also debugging when dune unexpectedly recompiles something is way too occult
I have a POC branch somewhere on my tree to do that, I hacked that a long time ago because I was fed up with recompilation.
(that was not for dune, but to override the check)
but the real problem here is not the check
why did the second command recompile vo
files?
alternatively, is there a documentation of the dune commands for typical workflows like this?
I read dev/doc/build-system.dune.md
, but couldn't find how to build stdlib
I think dune build path/to/file.vo
should rebuild the .vo.
but I precisely don't want to rebuild the vo
as it is not outdated
ah ok, I thought you had a broken vo file to repair (without recompiling everything)
no, I just want to launch CoqIDE after having built stdlib
Maxime Dénès said:
What I did:
make -f Makefile.dune world && dune exec dev/shim/coqide-prelude
Umm, the second command should not do any rebuild, did you modify any file meanwhile?
the *-prelude
shims only depend on Coq.Prelude.Init
thus they won't rebuild the rest of the stdlib
we could have a coqide-stdlib
which checks the stdlib is updated
indeed building the stdlib is just building all *.vo files
usually building the coq package will do it [or the coq-stdlib one would we split]
we can add an alias for that if it is convenient
the way I checked dune exec -- dev/shim/coqide-prelude
didn't rebuild anything is by looking at _build/log
Last updated: Dec 07 2023 at 14:02 UTC