Skip to content

Adapt to Coq 8.17

Adapt to Coq 8.17 #18

Triggered via pull request April 14, 2023 19:24
Status Failure
Total duration 25m 59s
Artifacts

docker-action.yml

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

Annotations

2 errors and 53 warnings
build (mathcomp/mathcomp:1.14.0-coq-8.11): theories/acyclic.v#L8
This command does not support this attribute: export.
build (mathcomp/mathcomp:1.12.0-coq-8.10): theories/acyclic.v#L8
This command does not support this attribute: export.
build (mathcomp/mathcomp-dev:coq-8.17)
Node.js 12 actions are deprecated. Please update the following actions to use Node.js 16: actions/checkout@v2. For more information see: https://github.blog/changelog/2022-09-22-github-actions-all-actions-will-begin-running-on-node16-instead-of-node12/.
build (mathcomp/mathcomp-dev:coq-8.16)
Node.js 12 actions are deprecated. Please update the following actions to use Node.js 16: actions/checkout@v2. For more information see: https://github.blog/changelog/2022-09-22-github-actions-all-actions-will-begin-running-on-node16-instead-of-node12/.
build (mathcomp/mathcomp:1.16.0-coq-8.17)
Node.js 12 actions are deprecated. Please update the following actions to use Node.js 16: actions/checkout@v2. For more information see: https://github.blog/changelog/2022-09-22-github-actions-all-actions-will-begin-running-on-node16-instead-of-node12/.
build (mathcomp/mathcomp:1.15.0-coq-8.16)
Node.js 12 actions are deprecated. Please update the following actions to use Node.js 16: actions/checkout@v2. For more information see: https://github.blog/changelog/2022-09-22-github-actions-all-actions-will-begin-running-on-node16-instead-of-node12/.
build (mathcomp/mathcomp:1.14.0-coq-8.11)
Node.js 12 actions are deprecated. Please update the following actions to use Node.js 16: actions/checkout@v2. For more information see: https://github.blog/changelog/2022-09-22-github-actions-all-actions-will-begin-running-on-node16-instead-of-node12/.
build (mathcomp/mathcomp:1.13.0-coq-8.13)
Node.js 12 actions are deprecated. Please update the following actions to use Node.js 16: actions/checkout@v2. For more information see: https://github.blog/changelog/2022-09-22-github-actions-all-actions-will-begin-running-on-node16-instead-of-node12/.
build (mathcomp/mathcomp:1.13.0-coq-8.13): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:1.12.0-coq-8.12)
Node.js 12 actions are deprecated. Please update the following actions to use Node.js 16: actions/checkout@v2. For more information see: https://github.blog/changelog/2022-09-22-github-actions-all-actions-will-begin-running-on-node16-instead-of-node12/.
build (mathcomp/mathcomp:1.12.0-coq-8.12): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:1.13.0-coq-8.12)
Node.js 12 actions are deprecated. Please update the following actions to use Node.js 16: actions/checkout@v2. For more information see: https://github.blog/changelog/2022-09-22-github-actions-all-actions-will-begin-running-on-node16-instead-of-node12/.
build (mathcomp/mathcomp:1.13.0-coq-8.12): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:1.12.0-coq-8.10)
Node.js 12 actions are deprecated. Please update the following actions to use Node.js 16: actions/checkout@v2. For more information see: https://github.blog/changelog/2022-09-22-github-actions-all-actions-will-begin-running-on-node16-instead-of-node12/.
build (mathcomp/mathcomp-dev:coq-dev)
Node.js 12 actions are deprecated. Please update the following actions to use Node.js 16: actions/checkout@v2. For more information see: https://github.blog/changelog/2022-09-22-github-actions-all-actions-will-begin-running-on-node16-instead-of-node12/.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra.v#L264
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra.v#L272
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra.v#L274
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-dev): theories/kosaraju.v#L23
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-dev): theories/kosaraju.v#L31
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-dev): theories/kosaraju.v#L33
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-dev): theories/kosaraju.v#L178
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-dev): theories/kosaraju.v#L187
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-dev): theories/kosaraju.v#L484
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-dev): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:1.12.0-coq-8.14)
Node.js 12 actions are deprecated. Please update the following actions to use Node.js 16: actions/checkout@v2. For more information see: https://github.blog/changelog/2022-09-22-github-actions-all-actions-will-begin-running-on-node16-instead-of-node12/.
build (mathcomp/mathcomp:1.12.0-coq-8.14): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp-dev:coq-8.15)
Node.js 12 actions are deprecated. Please update the following actions to use Node.js 16: actions/checkout@v2. For more information see: https://github.blog/changelog/2022-09-22-github-actions-all-actions-will-begin-running-on-node16-instead-of-node12/.
build (mathcomp/mathcomp-dev:coq-8.15): theories/extra.v#L264
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-8.15): theories/extra.v#L272
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-8.15): theories/extra.v#L274
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-8.15): theories/kosaraju.v#L23
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-8.15): theories/kosaraju.v#L31
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-8.15): theories/kosaraju.v#L33
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-8.15): theories/kosaraju.v#L178
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-8.15): theories/kosaraju.v#L187
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-8.15): theories/kosaraju.v#L484
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-8.15): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp-dev:coq-8.14)
Node.js 12 actions are deprecated. Please update the following actions to use Node.js 16: actions/checkout@v2. For more information see: https://github.blog/changelog/2022-09-22-github-actions-all-actions-will-begin-running-on-node16-instead-of-node12/.
build (mathcomp/mathcomp-dev:coq-8.14): theories/extra.v#L264
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-8.14): theories/extra.v#L272
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-8.14): theories/extra.v#L274
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-8.14): theories/kosaraju.v#L23
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-8.14): theories/kosaraju.v#L31
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-8.14): theories/kosaraju.v#L33
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-8.14): theories/kosaraju.v#L178
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-8.14): theories/kosaraju.v#L187
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-8.14): theories/kosaraju.v#L484
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp-dev:coq-8.14): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:1.13.0-coq-8.15)
Node.js 12 actions are deprecated. Please update the following actions to use Node.js 16: actions/checkout@v2. For more information see: https://github.blog/changelog/2022-09-22-github-actions-all-actions-will-begin-running-on-node16-instead-of-node12/.
build (mathcomp/mathcomp:1.13.0-coq-8.15): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:1.14.0-coq-8.14)
Node.js 12 actions are deprecated. Please update the following actions to use Node.js 16: actions/checkout@v2. For more information see: https://github.blog/changelog/2022-09-22-github-actions-all-actions-will-begin-running-on-node16-instead-of-node12/.
build (mathcomp/mathcomp:1.14.0-coq-8.14): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:1.14.0-coq-8.15)
Node.js 12 actions are deprecated. Please update the following actions to use Node.js 16: actions/checkout@v2. For more information see: https://github.blog/changelog/2022-09-22-github-actions-all-actions-will-begin-running-on-node16-instead-of-node12/.
build (mathcomp/mathcomp:1.14.0-coq-8.15): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is