Skip to content
Docker CI

Update doc #546

Sign in to view logs

Update doc

Update doc #546

Triggered via pull request February 7, 2024 15:34
@CasteranCasteran
opened #178
updateDoc
Status Success
Total duration 8m 27s
Artifacts –

docker-action.yml

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

Annotations

55 warnings
build (mathcomp/mathcomp:1.17.0-coq-8.17)
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/ordinals/Prelude/STDPP_compat.v#L14
A coercion will be introduced instead of an instance in future
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/ordinals/Ackermann/fol.v#L836
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/ordinals/Ackermann/fol.v#L861
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/ordinals/Prelude/DecPreOrder.v#L24
A coercion will be introduced instead of an instance in future
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/ordinals/Prelude/DecPreOrder.v#L30
A coercion will be introduced instead of an instance in future
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/ordinals/Prelude/DecPreOrder.v#L50
A coercion will be introduced instead of an instance in future
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/ordinals/Prelude/Comparable.v#L7
A coercion will be introduced instead of an instance in future
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/ordinals/Ackermann/folProp.v#L6
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/ordinals/Ackermann/folProof.v#L13
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/ordinals/Ackermann/Deduction.v#L10
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.18.0-coq-8.18)
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
build (mathcomp/mathcomp:1.18.0-coq-8.18): theories/ordinals/Prelude/STDPP_compat.v#L14
A coercion will be introduced instead of an instance in future
build (mathcomp/mathcomp:1.18.0-coq-8.18): theories/ordinals/Ackermann/fol.v#L836
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.18.0-coq-8.18): theories/ordinals/Ackermann/fol.v#L861
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.18.0-coq-8.18): theories/ordinals/Prelude/DecPreOrder.v#L24
A coercion will be introduced instead of an instance in future
build (mathcomp/mathcomp:1.18.0-coq-8.18): theories/ordinals/Prelude/DecPreOrder.v#L30
A coercion will be introduced instead of an instance in future
build (mathcomp/mathcomp:1.18.0-coq-8.18): theories/ordinals/Prelude/DecPreOrder.v#L50
A coercion will be introduced instead of an instance in future
build (mathcomp/mathcomp:1.18.0-coq-8.18): theories/ordinals/Prelude/Comparable.v#L7
A coercion will be introduced instead of an instance in future
build (mathcomp/mathcomp:1.18.0-coq-8.18): theories/ordinals/Ackermann/folProp.v#L6
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.18.0-coq-8.18): theories/ordinals/Ackermann/folProof.v#L13
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.18.0-coq-8.18): theories/ordinals/Ackermann/Deduction.v#L10
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.15.0-coq-8.16)
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
build (mathcomp/mathcomp:1.15.0-coq-8.16): theories/ordinals/Ackermann/fol.v#L836
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.15.0-coq-8.16): theories/ordinals/Ackermann/fol.v#L861
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.15.0-coq-8.16): theories/ordinals/Ackermann/folProp.v#L6
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.15.0-coq-8.16): theories/ordinals/Ackermann/folProof.v#L13
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.15.0-coq-8.16): theories/ordinals/Ackermann/Deduction.v#L10
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.15.0-coq-8.16): theories/ordinals/Ackermann/model.v#L12
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.15.0-coq-8.16): theories/ordinals/Ackermann/folLogic.v#L9
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.15.0-coq-8.16): theories/ordinals/Ackermann/folLogic2.v#L11
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.15.0-coq-8.16): theories/ordinals/Ackermann/subAll.v#L12
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.15.0-coq-8.16): theories/ordinals/Ackermann/folLogic3.v#L15
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.13.0-coq-8.14)
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
build (mathcomp/mathcomp:1.13.0-coq-8.14): theories/ordinals/Ackermann/fol.v#L836
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.13.0-coq-8.14): theories/ordinals/Ackermann/fol.v#L861
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.13.0-coq-8.14): theories/ordinals/Ackermann/folProp.v#L6
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.13.0-coq-8.14): theories/ordinals/Ackermann/folProof.v#L13
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.13.0-coq-8.14): theories/ordinals/Ackermann/Deduction.v#L10
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.13.0-coq-8.14): theories/ordinals/Ackermann/model.v#L12
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.13.0-coq-8.14): theories/ordinals/Ackermann/folLogic.v#L9
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.13.0-coq-8.14): theories/ordinals/Ackermann/folLogic2.v#L11
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.13.0-coq-8.14): theories/ordinals/Ackermann/subAll.v#L12
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.13.0-coq-8.14): theories/ordinals/Ackermann/folLogic3.v#L15
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.14.0-coq-8.15)
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
build (mathcomp/mathcomp:1.14.0-coq-8.15): theories/ordinals/Ackermann/fol.v#L836
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.14.0-coq-8.15): theories/ordinals/Ackermann/fol.v#L861
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.14.0-coq-8.15): theories/ordinals/Ackermann/folProp.v#L6
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.14.0-coq-8.15): theories/ordinals/Ackermann/folProof.v#L13
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.14.0-coq-8.15): theories/ordinals/Ackermann/Deduction.v#L10
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.14.0-coq-8.15): theories/ordinals/Ackermann/model.v#L12
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.14.0-coq-8.15): theories/ordinals/Ackermann/folLogic.v#L9
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.14.0-coq-8.15): theories/ordinals/Ackermann/folLogic2.v#L11
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.14.0-coq-8.15): theories/ordinals/Ackermann/subAll.v#L12
Notation "_ = _" was already used in scope fol_scope.
build (mathcomp/mathcomp:1.14.0-coq-8.15): theories/ordinals/Ackermann/folLogic3.v#L15
Notation "_ = _" was already used in scope fol_scope.