Skip to content

Cannot build Rocq with rocq.theory for Corelib and Ltac2 #12895

@rlepigre

Description

@rlepigre

Expected Behavior

When working with a composed build of Rocq and other Rocq libraries, it is generally not sufficient to just clone git@github.com:rocq-prover/rocq.git. We generally work around that with a few tweaks, the main part of which being to enable using coq.theory stanzas for Corelib and Ltac2. This still seems to work with 3.21.0_alpha2, but not if I try the same thing with the new rocq.theory.

CC @ejgallego @Lysxia who added rocq.theory in #12035.

Actual Behavior

Dune reports a dependency cycle, and also hangs (with 0 jobs running).

Reproduction

git clone --branch dune-rocq --depth 1 git@github.com:rlepigre/coq.git rocq
cd rocq
cp theories/Corelib/dune.disabled theories/Corelib/dune 
cp theories/Ltac2/dune.disabled theories/Ltac2/dune
dune build

The ast command hangs with the following output:

Error: Dependency cycle between:
   _build/default/topbin/rocq.exe
-> Computing installable artifacts for package rocqide
-> _build/default/tools/coqdep/lib/static_toplevel_libs.ml
-> _build/default/tools/coqdep/lib/.coqdeplib.objs/native/coqdeplib__Static_toplevel_libs.cmx
-> _build/default/tools/coqdep/lib/coqdeplib.a
-> _build/default/topbin/rocq.exe
-> required by Computing installable artifacts for package rocq-runtime
-> required by _build/default/rocq-runtime.install
-> required by alias default in dune:22
Done: 99% (1160/1170, 10 left, 1 failed) (jobs: 0)

Specifications

Tested with tag 3.21.0_alpha2.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions