Stream: Coq devs & plugin devs

Topic: failing coqide-server dev opam package


view this post on Zulip Karl Palmskog (Oct 03 2022 at 09:04):

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?

view this post on Zulip Gaƫtan Gilbert (Oct 03 2022 at 09:06):

is it getting coq-core from cache instead of recompiling it?

view this post on Zulip Karl Palmskog (Oct 03 2022 at 09:09):

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

view this post on Zulip Karl Palmskog (Oct 03 2022 at 09:10):

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)

view this post on Zulip Karl Palmskog (Oct 03 2022 at 09:11):

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