Stream: Coq devs & plugin devs

Topic: coqide dev opam package broken


view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Feb 21 2022 at 18:18):

Ah the .opam file isn't correct it looks like

view this post on Zulip Ali Caglayan (Feb 21 2022 at 18:18):

Do I need to update coqide.opam in the main repo and the opam archive?

view this post on Zulip Ali Caglayan (Feb 21 2022 at 18:22):

Are we going to generate these opam files using dune at some point?

view this post on Zulip Ali Caglayan (Feb 21 2022 at 18:30):

Is anybody able to do opam install coqide.dev and see if it breaks for them?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 21 2022 at 19:01):

[it's a guess]

view this post on Zulip 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: Feb 01 2023 at 16:03 UTC