Stream: Coq devs & plugin devs

Topic: Dune beginner question

Maxime Dénès (Sep 24 2020 at 17:10):

Sorry, this is probably a naive question: I'd like to build stdlib and run coqide using dune

Maxime Dénès (Sep 24 2020 at 17:11):

What I did: make -f Makefile.dune world && dune exec dev/shim/coqide-prelude

Maxime Dénès (Sep 24 2020 at 17:12):

Unfortunately, the second command triggered some recompilation and now Require Importon an stdlib file complains about inconsistent assumptions.

Gaëtan Gilbert (Sep 24 2020 at 17:14):

We should have something to disable those checks, they're way too sensitive
also debugging when dune unexpectedly recompiles something is way too occult

Pierre-Marie Pédrot (Sep 24 2020 at 17:15):

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.

Pierre-Marie Pédrot (Sep 24 2020 at 17:15):

(that was not for dune, but to override the check)

Maxime Dénès (Sep 24 2020 at 17:16):

but the real problem here is not the check

Maxime Dénès (Sep 24 2020 at 17:16):

why did the second command recompile vo files?

Maxime Dénès (Sep 24 2020 at 17:17):

alternatively, is there a documentation of the dune commands for typical workflows like this?

Maxime Dénès (Sep 24 2020 at 17:17):

I read dev/doc/build-system.dune.md, but couldn't find how to build stdlib

Enrico Tassi (Sep 24 2020 at 17:30):

I think dune build path/to/file.vo should rebuild the .vo.

Maxime Dénès (Sep 24 2020 at 17:57):

but I precisely don't want to rebuild the vo

Maxime Dénès (Sep 24 2020 at 17:57):

as it is not outdated

Enrico Tassi (Sep 24 2020 at 18:05):

ah ok, I thought you had a broken vo file to repair (without recompiling everything)

Maxime Dénès (Sep 24 2020 at 18:24):

no, I just want to launch CoqIDE after having built stdlib

Emilio Jesús Gallego Arias (Sep 24 2020 at 18:57):

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?

Emilio Jesús Gallego Arias (Sep 24 2020 at 18:58):

the *-prelude shims only depend on Coq.Prelude.Init thus they won't rebuild the rest of the stdlib

Emilio Jesús Gallego Arias (Sep 24 2020 at 18:58):

we could have a coqide-stdlib which checks the stdlib is updated

Emilio Jesús Gallego Arias (Sep 24 2020 at 18:59):

indeed building the stdlib is just building all *.vo files

Emilio Jesús Gallego Arias (Sep 24 2020 at 18:59):

usually building the coq package will do it [or the coq-stdlib one would we split]

Emilio Jesús Gallego Arias (Sep 24 2020 at 18:59):

we can add an alias for that if it is convenient

Emilio Jesús Gallego Arias (Sep 24 2020 at 19:00):

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