Skip to content

Adapt with respect to rocq-prover/rocq#21371 #3904

Adapt with respect to rocq-prover/rocq#21371

Adapt with respect to rocq-prover/rocq#21371 #3904

Re-run triggered November 28, 2025 14:48
Status Failure
Total duration 7m 4s
Artifacts

ci.yml

on: pull_request
Matrix: build
Matrix: opam-build
Matrix: quick-build
Matrix: coqchk
Matrix: install
doc-alectryon
14s
doc-alectryon
doc-dep-graphs
18s
doc-dep-graphs
doc-coqdoc
13s
doc-coqdoc
doc-timing
13s
doc-timing
deploy-doc
0s
deploy-doc
delete-artifacts
9s
delete-artifacts
Fit to window
Zoom out
Zoom in

Annotations

8 errors and 18 warnings
install (supported)
Unable to download artifact(s): Artifact not found for name: workspace-8.19 Please ensure that your artifact is not expired and the artifact was uploaded using a compatible version of toolkit/upload-artifact. For more information, visit the GitHub Artifacts FAQ: https://github.com/actions/toolkit/blob/main/packages/artifact/docs/faq.md
doc-timing
Unable to download artifact(s): Artifact not found for name: workspace-8.19 Please ensure that your artifact is not expired and the artifact was uploaded using a compatible version of toolkit/upload-artifact. For more information, visit the GitHub Artifacts FAQ: https://github.com/actions/toolkit/blob/main/packages/artifact/docs/faq.md
doc-coqdoc
Unable to download artifact(s): Artifact not found for name: workspace-8.19 Please ensure that your artifact is not expired and the artifact was uploaded using a compatible version of toolkit/upload-artifact. For more information, visit the GitHub Artifacts FAQ: https://github.com/actions/toolkit/blob/main/packages/artifact/docs/faq.md
doc-alectryon
Unable to download artifact(s): Artifact not found for name: workspace-8.19 Please ensure that your artifact is not expired and the artifact was uploaded using a compatible version of toolkit/upload-artifact. For more information, visit the GitHub Artifacts FAQ: https://github.com/actions/toolkit/blob/main/packages/artifact/docs/faq.md
coqchk (latest)
Unable to download artifact(s): Artifact not found for name: workspace-latest Please ensure that your artifact is not expired and the artifact was uploaded using a compatible version of toolkit/upload-artifact. For more information, visit the GitHub Artifacts FAQ: https://github.com/actions/toolkit/blob/main/packages/artifact/docs/faq.md
install (latest)
Unable to download artifact(s): Artifact not found for name: workspace-latest Please ensure that your artifact is not expired and the artifact was uploaded using a compatible version of toolkit/upload-artifact. For more information, visit the GitHub Artifacts FAQ: https://github.com/actions/toolkit/blob/main/packages/artifact/docs/faq.md
coqchk (supported)
Unable to download artifact(s): Artifact not found for name: workspace-8.19 Please ensure that your artifact is not expired and the artifact was uploaded using a compatible version of toolkit/upload-artifact. For more information, visit the GitHub Artifacts FAQ: https://github.com/actions/toolkit/blob/main/packages/artifact/docs/faq.md
doc-dep-graphs
Unable to download artifact(s): Artifact not found for name: workspace-8.19 Please ensure that your artifact is not expired and the artifact was uploaded using a compatible version of toolkit/upload-artifact. For more information, visit the GitHub Artifacts FAQ: https://github.com/actions/toolkit/blob/main/packages/artifact/docs/faq.md
build (dev, --warnings)
Could not find a terminator for warning: File "./theories/Basics/Overture.v", line 73, characters 0-8: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default]
build (dev, --warnings): ./theories/Basics/Settings.v#L52
There is no flag or option with this name: "Loose Hint Behavior".
build (dev, --warnings): ./theories/Basics/Settings.v#L10
"coq-core" has been renamed to "rocq-runtime".
build (dev, --warnings)
Could not find a terminator for warning: File "./theories/Basics/Settings.v", line 10, characters 0-90: Warning: "coq-core" has been renamed to "rocq-runtime". [coq-core-plugin,deprecated-since-9.0,deprecated,default]
build (dev, --warnings)
Could not find a terminator for warning: File "./theories/Basics/Settings.v", line 10, characters 0-90: Warning: Legacy loading plugin method has been removed from Rocq, and the `:` syntax is deprecated, and its first argument ignored; please remove "number_string_notation_plugin:" from your Declare ML [legacy-loading-removed,deprecated-since-9.0,deprecated,default]
build (dev, --warnings): ./theories/Basics/Settings.v#L8
"coq-core" has been renamed to "rocq-runtime".
build (dev, --warnings)
Could not find a terminator for warning: File "./theories/Basics/Settings.v", line 8, characters 0-54: Warning: "coq-core" has been renamed to "rocq-runtime". [coq-core-plugin,deprecated-since-9.0,deprecated,default]
build (dev, --warnings)
Could not find a terminator for warning: File "./theories/Basics/Settings.v", line 8, characters 0-54: Warning: Legacy loading plugin method has been removed from Rocq, and the `:` syntax is deprecated, and its first argument ignored; please remove "ltac_plugin:" from your Declare ML [legacy-loading-removed,deprecated-since-9.0,deprecated,default]
opam-build (dev, ubuntu-latest): theories/Basics/Overture.v#L199
Use of "Notation" keyword for abbreviations is deprecated, use
opam-build (dev, ubuntu-latest): theories/Basics/Overture.v#L190
Use of "Notation" keyword for abbreviations is deprecated, use
opam-build (dev, ubuntu-latest): theories/Basics/Overture.v#L189
Use of "Notation" keyword for abbreviations is deprecated, use
opam-build (dev, ubuntu-latest): theories/Basics/Overture.v#L142
Use of "Notation" keyword for abbreviations is deprecated, use
opam-build (dev, ubuntu-latest): theories/Basics/Overture.v#L76
Implicitly declaring hint databases is deprecated. Please explicitly
opam-build (dev, ubuntu-latest): theories/Basics/Overture.v#L74
Use of "Notation" keyword for abbreviations is deprecated, use
opam-build (dev, ubuntu-latest): theories/Basics/Overture.v#L73
Use of "Notation" keyword for abbreviations is deprecated, use
opam-build (dev, ubuntu-latest): theories/Basics/Settings.v#L52
There is no flag or option with this name: "Loose Hint Behavior".
opam-build (dev, ubuntu-latest): theories/Basics/Settings.v#L10
"coq-core" has been renamed to "rocq-runtime".
opam-build (dev, ubuntu-latest): theories/Basics/Settings.v#L8
"coq-core" has been renamed to "rocq-runtime".