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)
OK I believe I found the curlprit: this commit was incomplete (6184404b), I will open a PR soonish.
Done: PR #15585
Last updated: Oct 13 2024 at 01:02 UTC