Skip to content

Temporarily remove coq-trocq-std from CI - #438

Merged
gares merged 1 commit into
LPCIC:masterfrom
VojtechStep:fix/remove-trocq-ci
Aug 4, 2026
Merged

Temporarily remove coq-trocq-std from CI#438
gares merged 1 commit into
LPCIC:masterfrom
VojtechStep:fix/remove-trocq-ci

Conversation

@VojtechStep

Copy link
Copy Markdown
Contributor

Trocq is apparently known to be currently broken [1]; among other things its opam file declares a dependency on
"coq" {>= "9.0" & < "9.2"}, while rocq-stdlib@master already dropped support for rocq < 9.2 [2].

Note also that ignoring the version range on "coq" doesn't help, since the "coq" package doesn't have a version for 9.2 in the opam repository (and doesn't exist in the rocq repository), as opposed to e.g. coq-core.

Removing Trocq makes the rest of the "test users" CI pass: https://github.com/VojtechStep/elpi/actions/runs/30910579757/job/91996039212

Trocq is apparently known to be currently broken [1]; among other
things its opam file declares a dependency on
`"coq" {>= "9.0" & < "9.2"}`, while rocq-stdlib@master already dropped
support for rocq < 9.2 [2].

Note also that ignoring the version range on "coq" doesn't help, since
the "coq" package doesn't have a version for 9.2 in the opam
repository (and doesn't exist in the rocq repository), as opposed to
e.g. coq-core.

[1]: rocq-community/trocq#86
[2]: rocq-prover/stdlib#300
@gares
gares merged commit 454a559 into LPCIC:master Aug 4, 2026
8 of 10 checks passed
@VojtechStep
VojtechStep deleted the fix/remove-trocq-ci branch August 4, 2026 13:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants