Skip to content
Docker CI

Port to MathComp 2 #144

Sign in to view logs

Port to MathComp 2

Port to MathComp 2 #144

Triggered via pull request September 27, 2023 12:25
@pi8027pi8027
opened #16
hierarchy-builder
Status Failure
Total duration 33m 44s
Artifacts –

docker-action.yml

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

Annotations

20 errors and 50 warnings
build (mathcomp/mathcomp:1.12.0-coq-8.13): theories/tactics.v#L86
The reference subringClosed was not found in the current environment.
build (mathcomp/mathcomp:1.13.0-coq-8.15): theories/tactics.v#L86
The reference subringClosed was not found in the current environment.
build (mathcomp/mathcomp:1.14.0-coq-8.14): theories/tactics.v#L86
The reference subringClosed was not found in the current environment.
build (mathcomp/mathcomp:1.12.0-coq-8.14): theories/tactics.v#L86
The reference subringClosed was not found in the current environment.
build (mathcomp/mathcomp:1.13.0-coq-8.14): theories/tactics.v#L86
The reference subringClosed was not found in the current environment.
build (mathcomp/mathcomp:1.13.0-coq-8.13): theories/tactics.v#L86
The reference subringClosed was not found in the current environment.
build (mathcomp/mathcomp:1.14.0-coq-8.15): theories/tactics.v#L86
The reference subringClosed was not found in the current environment.
build (mathcomp/mathcomp:1.15.0-coq-8.14): theories/tactics.v#L86
The reference subringClosed was not found in the current environment.
build (mathcomp/mathcomp:1.15.0-coq-8.15): theories/tactics.v#L86
The reference subringClosed was not found in the current environment.
build (mathcomp/mathcomp:1.14.0-coq-8.13): theories/tactics.v#L86
The reference subringClosed was not found in the current environment.
build (mathcomp/mathcomp:1.15.0-coq-8.13): theories/tactics.v#L86
The reference subringClosed was not found in the current environment.
build (mathcomp/mathcomp:1.15.0-coq-8.16): theories/tactics.v#L86
The reference subringClosed was not found in the current environment.
build (mathcomp/mathcomp:1.16.0-coq-8.15): theories/tactics.v#L86
The reference subringClosed was not found in the current environment.
build (mathcomp/mathcomp:1.16.0-coq-8.14): theories/tactics.v#L86
The reference subringClosed was not found in the current environment.
build (mathcomp/mathcomp:1.16.0-coq-8.16): theories/tactics.v#L86
The reference subringClosed was not found in the current environment.
build (mathcomp/mathcomp:1.16.0-coq-8.13): theories/tactics.v#L86
The reference subringClosed was not found in the current environment.
build (mathcomp/mathcomp:1.16.0-coq-8.17): theories/tactics.v#L86
The reference subringClosed was not found in the current environment.
build (mathcomp/mathcomp-dev:coq-8.17): theories/binomialz.v#L157
The RHS of PoszM
build (mathcomp/mathcomp-dev:coq-8.16): theories/binomialz.v#L157
The RHS of PoszM
build (mathcomp/mathcomp-dev:coq-dev): theories/binomialz.v#L157
The RHS of PoszM
build (mathcomp/mathcomp:1.12.0-coq-8.13)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp:1.13.0-coq-8.15)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp:1.14.0-coq-8.14)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp:1.12.0-coq-8.14)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp:1.13.0-coq-8.14)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp:1.13.0-coq-8.13)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp:1.14.0-coq-8.15)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp:1.15.0-coq-8.14)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp:1.15.0-coq-8.15)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp:1.14.0-coq-8.13)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp:1.15.0-coq-8.13)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp:1.15.0-coq-8.16)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp:1.16.0-coq-8.15)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp:1.16.0-coq-8.14)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp:1.16.0-coq-8.16)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp:1.16.0-coq-8.13)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp:1.16.0-coq-8.17)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp-dev:coq-8.17)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L93
Notation ler_pexpn2r is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L93
Notation ler_pexpn2r is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L93
Notation ler_pexpn2r is deprecated since mathcomp 1.17.0.