Ali Caglayan (Feb 21 2022 at 18:16): Ali Caglayan (Feb 21 2022 at 18:16):I seem to have broken the install of the dev version of CoqIDE from the opam archive with https://github.com/coq/coq/pull/15645. I'm getting:
### output ###
# (cd _build/default && /mnt/sdd1/.opam/coq.dev/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -I ide/coqide/.coqide_gui.objs/byte -I ide/coqide/.coqide_gui.objs/native -I /mnt/sdd1/.opam/coq.dev/lib/cairo2 -I /mnt/sdd1/.opam/coq.dev/lib/coq-core/boot -I /mnt/sdd1/.opam/coq.dev/lib/coq-core/clib -I /mnt/sdd1/.opam/coq.dev/lib/coq-core/config -I /mnt/sdd1/.opam/coq.dev/lib/coq-core/lib[...]
# File "ide/coqide/coqide.ml", line 1805, characters 28-38:
# 1805 | let coqide_specific_usage = Boot.Usage.{
# ^^^^^^^^^^
# Error: Unbound module Boot.Usage
But I explicitly said that the dune file for coqide relies on coq-core.boot, so why is opam struggling here?
Ali Caglayan (Feb 21 2022 at 18:18):Ah the .opam file isn't correct it looks like
Ali Caglayan (Feb 21 2022 at 18:18):Do I need to update coqide.opam in the main repo and the opam archive?
Ali Caglayan (Feb 21 2022 at 18:22):Are we going to generate these opam files using dune at some point?
Ali Caglayan (Feb 21 2022 at 18:30):Is anybody able to do opam install coqide.dev and see if it breaks for them?
Emilio Jesús Gallego Arias (Feb 21 2022 at 19:01):Can't look into this now but usually the problem is due to versions mismatch, the dev thing doesn't really track the concrete hash needed
Emilio Jesús Gallego Arias (Feb 21 2022 at 19:01):[it's a guess]
Paolo Giarrusso (Feb 21 2022 at 20:19):The opam files inside coq/ are dune-generated and use the full dune build, but those in repos still used the old build last I checked
Last updated: May 31 2023 at 16:01 UTC