Skip to content

[CI] Update Nix toolbox and add CoqEAL #1103

[CI] Update Nix toolbox and add CoqEAL

[CI] Update Nix toolbox and add CoqEAL #1103

Triggered via pull request October 10, 2023 07:47
Status Success
Total duration 7m 56s
Artifacts

main.yml

on: pull_request
Matrix: opam
release
0s
release
Fit to window
Zoom out
Zoom in

Annotations

19 warnings
opam (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/
opam (8.17): examples/demo2/stage10.v#L233
The default and global localities for this command outside sections
opam (8.17): examples/demo2/stage11.v#L364
The default and global localities for this command outside sections
opam (8.17): examples/Coq2020_material/CoqWS_expansion/withoutHB.v#L10
The format modifier has no effect for only-parsing notations.
opam (8.17): tests/infer.v#L20
Skipping test on Coq 8.17.1 as requested
opam (8.17): tests/funclass.v#L19
Notation plus_assoc is deprecated since 8.16.
opam (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/
opam (8.16): examples/Coq2020_material/CoqWS_expansion/withoutHB.v#L10
The format modifier has no effect for only-parsing notations.
opam (8.16): tests/infer.v#L20
Skipping test on Coq 8.16.1 as requested
opam (8.16): tests/funclass.v#L19
Notation plus_assoc is deprecated since 8.16.
opam (8.18)
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/
opam (8.18): examples/demo2/stage10.v#L4
Hiding binding of key Q to Q_scope
opam (8.18): examples/demo2/stage10.v#L233
The default and global localities for this command outside sections
opam (8.18): examples/demo2/stage11.v#L3
Hiding binding of key Q to Q_scope
opam (8.18): examples/demo2/stage11.v#L364
The default and global localities for this command outside sections
opam (8.18): examples/Coq2020_material/CoqWS_expansion/withoutHB.v#L10
The format modifier has no effect for only-parsing notations.
opam (8.18): tests/infer.v#L20
Skipping test on Coq 8.18.0 as requested
opam (8.18): tests/funclass.v#L19
Notation plus_assoc is deprecated since 8.16.
opam (8.18): tests/non_forgetful_inheritance.v#L35
Could not enable unknown warning HB.non-forgetful-inheritance