Stream: Coq devs & plugin devs

Topic: coq.dev package broken?


view this post on Zulip 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

view this post on Zulip Ralf Jung (Apr 27 2021 at 17:49):

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

view this post on Zulip Ralf Jung (Apr 27 2021 at 17:54):

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

view this post on Zulip Ralf Jung (Apr 27 2021 at 17:55):

On CI I am seeing a different error that I cannot reproduce

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 18:20):

It seems the package is indeed broken due to the wrong install file.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 18:21):

Except for the configure call

view this post on Zulip Ralf Jung (Apr 28 2021 at 07:21):

I don't know what you mean by any of this...

view this post on Zulip Ralf Jung (Apr 28 2021 at 07:21):

@Emilio Jesús Gallego Arias could you just update the package?

view this post on Zulip 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).

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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: Oct 16 2021 at 03:02 UTC