Skip to content
CI

Adapt to coq/coq#20132 (new_evar needs a relevance) #630

Sign in to view logs

Adapt to coq/coq#20132 (new_evar needs a relevance)

Adapt to coq/coq#20132 (new_evar needs a relevance) #630

Triggered via pull request January 28, 2025 12:17
@SkySkimmerSkySkimmer
opened #633
SkySkimmer:evar-relevance
Status Failure
Total duration 4m 32s
Artifacts –

build.yml

on: pull_request
Matrix: build
Fit to window
Zoom out
Zoom in

Annotations

2 errors and 20 warnings
build (dev, 4.09-flambda, hott): theories/HoTT/Classes.v#L11
Cannot find a physical path bound to logical path HoTT.HSet.
build (dev, 4.09-flambda, dune): theories/HoTT/Classes.v#L11
Cannot find a physical path bound to logical path HoTT.HSet.
build (dev, 4.09-flambda, local)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
build (dev, 4.09-flambda, local): theories/Init.v#L11
"coq-core" has been renamed to "rocq-runtime".
build (dev, 4.09-flambda, local): theories/Type/Relation_Properties.v#L40
Notations "_ * _" defined at level 40 with arguments constr
build (dev, 4.09-flambda, local): theories/Prop/NoConfusion.v#L14
Loading Stdlib without prefix is deprecated.
build (dev, 4.09-flambda, local): theories/Prop/NoConfusion.v#L14
Loading Stdlib without prefix is deprecated.
build (dev, 4.09-flambda, local)
"From Coq" has been replaced by "From Stdlib".
build (dev, 4.09-flambda, local)
Loading Stdlib without prefix is deprecated.
build (dev, 4.09-flambda, local)
Using Vector.t is known to be technically difficult, see
build (dev, 4.09-flambda, local)
Loading Stdlib without prefix is deprecated.
build (dev, 4.09-flambda, local)
Loading Stdlib without prefix is deprecated.
build (dev, 4.09-flambda, local)
Loading Stdlib without prefix is deprecated.
build (dev, 4.09-flambda, hott)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
build (dev, 4.09-flambda, hott): theories/Init.v#L11
"coq-core" has been renamed to "rocq-runtime".
build (dev, 4.09-flambda, hott): theories/HoTT/Relation_Properties.v#L46
Notations "_ * _" defined at level 40 with arguments constr
build (dev, 4.09-flambda, dune)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
build (dev, 4.09-flambda, dune): theories/Init.v#L11
"coq-core" has been renamed to "rocq-runtime".
build (dev, 4.09-flambda, dune): theories/Type/Relation_Properties.v#L40
Notations "_ * _" defined at level 40 with arguments constr
build (dev, 4.09-flambda, dune): theories/HoTT/Relation_Properties.v#L46
Notations "_ * _" defined at level 40 with arguments constr
build (dev, 4.09-flambda, dune): theories/Prop/NoConfusion.v#L14
Loading Stdlib without prefix is deprecated.
build (dev, 4.09-flambda, dune): theories/Prop/NoConfusion.v#L14
Loading Stdlib without prefix is deprecated.