Ralf Jung (Apr 27 2021 at 17:48): Ralf Jung (Apr 27 2021 at 17:48):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[1]: *** [_build/install/default/bin/coqc] Error 69
# make[1]: *** 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[1]: *** [_build/default/user-contrib/Ltac2/ltac2_plugin.cmxs] Error 69
# make[1]: 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
Ralf Jung (Apr 27 2021 at 17:55):On CI I am seeing a different error that I cannot reproduce
Ralf Jung (Apr 27 2021 at 17:56):also FWIW, the coq package does not depend on dune, so that might be why the two machines behave differently
Emilio Jesús Gallego Arias (Apr 27 2021 at 18:20):It seems the package is indeed broken due to the wrong install file.
Emilio Jesús Gallego Arias (Apr 27 2021 at 18:20):Fortunately the fix is very easy as dune will generate the install file for the coq-core one!
Emilio Jesús Gallego Arias (Apr 27 2021 at 18:20):So actually you need to introduce coq-core.dev which is a regular dune package.
Emilio Jesús Gallego Arias (Apr 27 2021 at 18:21):Except for the configure call
Ralf Jung (Apr 28 2021 at 07:21):I don't know what you mean by any of this...
Ralf Jung (Apr 28 2021 at 07:21):@Emilio Jesús Gallego Arias could you just update the package?
Théo Zimmermann (Apr 28 2021 at 12:36):I've opened https://github.com/coq/opam-coq-archive/pull/1699 with a quick fix attempt (no splitting into coq-core / coq-stdlib).
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:40):Sorry I was not clear, what we have to do is not so hard:
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:41):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.
Théo Zimmermann (Apr 28 2021 at 12:42):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: Sep 15 2024 at 13:02 UTC