Is it possible that the coq.dev package is broken (e.g. due to the recent dune change)?
#=== ERROR while installing coq.dev ===========================================# Some files in /home/r/.opam/coq-test/.opam-switch/install/coq.install couldn't be installed: - /home/r/.opam/coq-test/.opam-switch/build/coq.dev/bin/coqworkmgr to /home/r/.opam/coq-test/bin - /home/r/.opam/coq-test/.opam-switch/build/coq.dev/bin/coq-tex to /home/r/.opam/coq-test/bin - /home/r/.opam/coq-test/.opam-switch/build/coq.dev/bin/coq_makefile to /home/r/.opam/coq-test/bin - /home/r/.opam/coq-test/.opam-switch/build/coq.dev/bin/coqc to /home/r/.opam/coq-test/bin - /home/r/.opam/coq-test/.opam-switch/build/coq.dev/bin/coqchk to /home/r/.opam/coq-test/bin - /home/r/.opam/coq-test/.opam-switch/build/coq.dev/bin/coqdep to /home/r/.opam/coq-test/bin - /home/r/.opam/coq-test/.opam-switch/build/coq.dev/bin/coqdoc to /home/r/.opam/coq-test/bin - /home/r/.opam/coq-test/.opam-switch/build/coq.dev/bin/coqtop.byte to /home/r/.opam/coq-test/bin - /home/r/.opam/coq-test/.opam-switch/build/coq.dev/bin/coqtop to /home/r/.opam/coq-test/bin - /home/r/.opam/coq-test/.opam-switch/build/coq.dev/bin/coqwc to /home/r/.opam/coq-test/bin
On CI I have also seen
### output ### # [...] # DUNE _build/install/default/bin/coqc # DUNE _build/default/user-contrib/Ltac2/ltac2_plugin.cmxs # flock: failed to execute dune: No such file or directory # Makefile.common:101: recipe for target '_build/install/default/bin/coqc' failed # make: *** [_build/install/default/bin/coqc] Error 69 # make: *** Waiting for unfinished jobs.... # flock: failed to execute dune: No such file or directory # Makefile.common:159: recipe for target '_build/default/user-contrib/Ltac2/ltac2_plugin.cmxs' failed # make: *** [_build/default/user-contrib/Ltac2/ltac2_plugin.cmxs] Error 69 # make: Leaving directory '/builds/iris/lambda-rust/_opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq.dev' # Makefile.make:122: recipe for target 'submake' failed # make: *** [submake] Error 2
locally the build seems to succeed, actually, but then the files listed at https://github.com/coq/opam-coq-archive/blob/master/core-dev/packages/coq/coq.dev/files/coq.install don't exist
On CI I am seeing a different error that I cannot reproduce
also FWIW, the
coq package does not depend on
dune, so that might be why the two machines behave differently
It seems the package is indeed broken due to the wrong install file.
Fortunately the fix is very easy as dune will generate the install file for the coq-core one!
So actually you need to introduce
coq-core.dev which is a regular dune package.
Except for the configure call
I don't know what you mean by any of this...
@Emilio Jesús Gallego Arias could you just update the package?
I've opened https://github.com/coq/opam-coq-archive/pull/1699 with a quick fix attempt (no splitting into
Sorry I was not clear, what we have to do is not so hard:
But actually @Théo Zimmermann about native is interesting, I will think about it, for sure we want to have native working with the split.
Ideally, we would want both the Dune build and the coq_makefile build for the stdlib to be supported in the split case.
Last updated: Feb 02 2023 at 15:04 UTC