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
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
Last updated: Feb 05 2023 at 20:03 UTC