[coq] Composition with (boot) theories hangs with a cycle in Dune > 3.7 when coq lang > 0.6 #7908
Description
I've discovered some issues when testing composition with Coq itself in Dune 3.8.
First issue is as follows, given:
- a composed Coq build (see [1] how to setup)
- a
(lang coq 0.7) or 0.8
Then Dune will fail with:
Error: Dependency cycle between:
Computing installable artifacts for package coqide-server
-> required by Computing installable artifacts for package coq-core
-> required by _build/default/coq-core.install
-> required by alias default in dune:22
This seems to be related to the Coq_config resolution in boot. Note that the issue doesn't occur for lower versions of the Coq language.
cc @Alizter
[1] To reproduce, you can use Coq's main branch:
$ git clone https://github.com/coq/coq.git
$ cd coq && cp theories/dune.disabled theories/dune
$ # edit dune-project to raise `(lang coq ...)`
$ dune build @default