Stream: Coq devs & plugin devs

Topic: Why `coqorg/coq:dev` FTBFS currently?


view this post on Zulip Erik Martin-Dorel (Feb 02 2022 at 01:06):

Hi all, I've noticed coqorg/coq:dev fails to build from source in GitLab CI / docker-coq, currently:

- COQC      theories/setoid_ring/Rings_R.v
- make[1]: Leaving directory '/home/coq/.opam/4.12.0+flambda/.opam-switch/build/coq.dev'
Processing  3/6: [coq: make byte]
+ /usr/bin/make "-j2" "byte" (CWD=/home/coq/.opam/4.12.0+flambda/.opam-switch/build/coq.dev)
- /usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.build byte
- make[1]: Entering directory '/home/coq/.opam/4.12.0+flambda/.opam-switch/build/coq.dev'
- DUNE      sources
- Error: no rule to make target byte (or missing .PHONY)
- make[1]: *** [Makefile.build:384: byte] Error 1
- make[1]: Leaving directory '/home/coq/.opam/4.12.0+flambda/.opam-switch/build/coq.dev'
- make: *** [Makefile.make:122: submake] Error 2
[ERROR] The compilation of coq failed at "/usr/bin/make -j2 byte".

#=== ERROR while compiling coq.dev ============================================#
# context              2.0.9 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.4.12.0+options | pinned(git+https://github.com/coq/coq#5fcaf4850a2497b72e1d72d2acda6597ddd0f497#5fcaf485)
# path                 ~/.opam/4.12.0+flambda/.opam-switch/build/coq.dev
# command              /usr/bin/make -j2 byte
# exit-code            2
# env-file             ~/.opam/log/coq-1477-0c525f.env
# output-file          ~/.opam/log/coq-1477-0c525f.out
### output ###
# /usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.build byte
# make[1]: Entering directory '/home/coq/.opam/4.12.0+flambda/.opam-switch/build/coq.dev'
# DUNE      sources
# Error: no rule to make target byte (or missing .PHONY)
# make[1]: *** [Makefile.build:384: byte] Error 1
# make[1]: Leaving directory '/home/coq/.opam/4.12.0+flambda/.opam-switch/build/coq.dev'
# make: *** [Makefile.make:122: submake] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions were aborted
| - install coq-bignums dev
+-
+- The following actions failed
| - build coq dev
+-
+- The following changes have been performed (the rest was aborted)
| - install conf-findutils 1
+-

Do you have an idea of what changed in master to explain this?

(FYI the build script is stored in this Dockerfile, to be fixed then)

view this post on Zulip Erik Martin-Dorel (Feb 02 2022 at 01:13):

OK I believe I found the curlprit: this commit was incomplete (6184404b), I will open a PR soonish.

view this post on Zulip Erik Martin-Dorel (Feb 02 2022 at 01:20):

Done: PR #15585


Last updated: Feb 02 2023 at 13:03 UTC