So the coqide-server.dev
package is seeing these kinds of compilation errors, which affects a bunch of Docker images:
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] The compilation of coqide-server failed at "/home/palmskog/.opam/opam-init/hooks/sandbox.sh build dune build -p coqide-server -j 7 @install".
#=== ERROR while compiling coqide-server.dev ==================================#
# context 2.0.7 | linux/x86_64 | ocaml-base-compiler.4.11.1 | https://coq.inria.fr/opam/core-dev#2022-10-03 02:50
# path ~/.opam/4.11.1.coqdev/.opam-switch/build/coqide-server.dev
# command ~/.opam/opam-init/hooks/sandbox.sh build dune build -p coqide-server -j 7 @install
# exit-code 1
# env-file ~/.opam/log/coqide-server-207257-9ace5e.env
# output-file ~/.opam/log/coqide-server-207257-9ace5e.out
### output ###
# (cd _build/default && /home/palmskog/.opam/4.11.1.coqdev/bin/ocamlc.opt -w -40 -rectypes -g -bin-annot -I ide/coqide/.idetop.eobjs/byte -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/boot -I /home/palmskog
/.opam/4.11.1.coqdev/lib/coq-core/clib -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/config -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/engine -I /home/palmskog/.opam/4.11.1.[...]
# File "ide/coqide/idetop.ml", line 205, characters 33-54:
# 205 | let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal ~short ?og_s (Proof_diffs.make_goal env nsigma ng) in
# ^^^^^^^^^^^^^^^^^^^^^
# Error: This function has type
# ?og_s:Proof_diffs.goal -> Proof_diffs.goal -> Pp.t list * Pp.t
# It is applied to too many arguments; maybe you forgot a `;'.
As far as I can see, the opam package definitions in core-dev
opam repo and in the Coq GitHub repo are the same. So did something break in Coq itself?
is it getting coq-core from cache instead of recompiling it?
ah, so it might be our new addition of coqide-server.dev
as a dependency of the coq.dev
package that triggers this. coqide-server.dev
depends on coq-core
, but coqide-server.dev
is still for some reason rebuilt before coq-core.dev
when one does something like: opam upgrade coq
in that case, this is likely to affect all Docker images with coq.dev
, so one has to rebuild them all from scratch (cc: @Erik Martin-Dorel)
the compilation problems went away for me when I did: opam upgrade coq-core
... since this rebuilds coq-core.dev
before coqide-server.dev
.
Last updated: Oct 13 2024 at 01:02 UTC