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?
Ah the .opam file isn't correct it looks like
Do I need to update coqide.opam in the main repo and the opam archive?
Are we going to generate these opam files using dune at some point?
Is anybody able to do opam install coqide.dev
and see if it breaks for them?
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
[it's a guess]
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