Skip to content
CI (Coq, docker)

Change default target to the one used for Coq's CI #153

Sign in to view logs

Change default target to the one used for Coq's CI

Change default target to the one used for Coq's CI #153

Triggered via push November 30, 2023 21:00
@JasonGrossJasonGross
pushed cf4acee
master
Status Failure
Total duration 6m 21s
Artifacts –

docker-coq.yml

on: push
Matrix: build
check-all-docker
0s
check-all-docker
Fit to window
Zoom out
Zoom in

Annotations

11 errors and 40 warnings
dev (fiat-core parsers parsers-examples coq-ci): src/Common/Frame.v#L1
Cannot find a physical path bound to logical path Coq.Arith.Max.
dev (fiat-core parsers parsers-examples coq-ci): src/Common/Le.v#L3
Cannot find a physical path bound to logical path Coq.Arith.Le.
dev (fiat-core parsers parsers-examples coq-ci): src/Common/Wf.v#L450
The reference EqNat.beq_nat was not found in the current environment.
dev (fiat-core parsers parsers-examples coq-ci): src/Common/NatFacts.v#L3
Cannot find a physical path bound to logical path
dev (fiat-core parsers parsers-examples coq-ci): src/Computation/Decidable.v#L153
The reference beq_nat was not found in the current environment.
dev (fiat-core parsers parsers-examples coq-ci): src/Common.v#L2
Cannot find a physical path bound to logical path
dev (fiat-core parsers parsers-examples coq-ci): src/Parsers/BaseTypesLemmas.v#L115
The reference Lt.le_lt_trans was not found in the current environment.
dev (fiat-core parsers parsers-examples coq-ci): src/Parsers/GenericCorrectnessBaseTypes.v#L66
The reference beq_nat was not found in the current environment.
dev (fiat-core parsers parsers-examples coq-ci): src/Common/Frame.v#L1
Cannot find a physical path bound to logical path Coq.Arith.Max.
dev (fiat-core parsers parsers-examples coq-ci): src/Common.v#L2
Cannot find a physical path bound to logical path
check-all-docker
Process completed with exit code 1.
dev (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L12
There is no flag or option with this name: "Template Check".
dev (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L28
There is no flag or option with this name:
dev (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L29
There is no flag or option with this name: "Apply With Renaming".
dev (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L57
Use of “Require” inside a module is fragile. It is not recommended
dev (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L58
Use of “Require” inside a module is fragile. It is not recommended
dev (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L59
Use of “Require” inside a module is fragile. It is not recommended
dev (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L60
Use of “Require” inside a module is fragile. It is not recommended
dev (fiat-core parsers parsers-examples coq-ci): src/Computation/Notations.v#L20
Declaring a scope implicitly is deprecated; use in advance an
dev (fiat-core parsers parsers-examples coq-ci): src/Common/BoolFacts.v#L11
Declaring a scope implicitly is deprecated; use in advance an
dev (fiat-core parsers parsers-examples coq-ci): src/Common/Wf.v#L279
Tactic Notation revert dependent (hyp) is deprecated since 8.18.
8.17 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L11
There is no flag or option with this name: "Template Check".
8.17 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L29
There is no flag or option with this name:
8.17 (fiat-core parsers parsers-examples coq-ci): src/Parsers/StringLike/Core.v#L21
A coercion will be introduced instead of an instance in future
8.17 (fiat-core parsers parsers-examples coq-ci): src/Parsers/StringLike/Core.v#L47
Declaring a scope implicitly is deprecated; use in advance an
8.17 (fiat-core parsers parsers-examples coq-ci): src/Parsers/StringLike/Core.v#L107
A coercion will be introduced instead of an instance in future
8.17 (fiat-core parsers parsers-examples coq-ci): src/Computation/Decidable.v#L153
Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead.
8.17 (fiat-core parsers parsers-examples coq-ci): src/Computation/Decidable.v#L155
Notation beq_nat_true_iff is deprecated since 8.16.
8.17 (fiat-core parsers parsers-examples coq-ci): src/Computation/Decidable.v#L155
Notation beq_nat_true_iff is deprecated since 8.16.
8.17 (fiat-core parsers parsers-examples coq-ci): src/Parsers/ExtrOcamlPrimitives.v#L17
Declaring a scope implicitly is deprecated; use in advance an
8.17 (fiat-core parsers parsers-examples coq-ci): src/Computation/Notations.v#L20
Declaring a scope implicitly is deprecated; use in advance an
8.18 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L11
There is no flag or option with this name: "Template Check".
8.18 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L29
There is no flag or option with this name:
8.18 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L30
There is no flag or option with this name: "Apply With Renaming".
8.18 (fiat-core parsers parsers-examples coq-ci): src/Common/Tactics/IsClosed.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet"!
8.18 (fiat-core parsers parsers-examples coq-ci): src/Common/Tactics/IsClosed.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet"!
8.18 (fiat-core parsers parsers-examples coq-ci): src/Common/Tactics/IsClosed.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet.set_diff_nodup"!
8.18 (fiat-core parsers parsers-examples coq-ci): src/Common/Tactics/PrintContext.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet"!
8.18 (fiat-core parsers parsers-examples coq-ci): src/Common/Tactics/PrintContext.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet"!
8.18 (fiat-core parsers parsers-examples coq-ci): src/Common/Tactics/PrintContext.v#L1
Trying to mask the absolute name "Coq.Lists.ListSet.set_diff_nodup"!
8.18 (fiat-core parsers parsers-examples coq-ci): src/Parsers/StringLike/Core.v#L5
Trying to mask the absolute name "Coq.Lists.ListSet"!
8.16 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L11
There is no flag or option with this name: "Template Check".
8.16 (fiat-core parsers parsers-examples coq-ci): src/Common/Coq__8_4__8_5__Compat.v#L29
There is no flag or option with this name:
8.16 (fiat-core parsers parsers-examples coq-ci): src/Parsers/StringLike/Core.v#L47
Declaring a scope implicitly is deprecated; use in advance an
8.16 (fiat-core parsers parsers-examples coq-ci): src/Computation/Decidable.v#L153
Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead.
8.16 (fiat-core parsers parsers-examples coq-ci): src/Computation/Decidable.v#L155
Notation beq_nat_true_iff is deprecated since 8.16.
8.16 (fiat-core parsers parsers-examples coq-ci): src/Computation/Decidable.v#L155
Notation beq_nat_true_iff is deprecated since 8.16.
8.16 (fiat-core parsers parsers-examples coq-ci): src/Parsers/ExtrOcamlPrimitives.v#L17
Declaring a scope implicitly is deprecated; use in advance an
8.16 (fiat-core parsers parsers-examples coq-ci): src/Computation/Notations.v#L20
Declaring a scope implicitly is deprecated; use in advance an
8.16 (fiat-core parsers parsers-examples coq-ci): src/Common/BoolFacts.v#L11
Declaring a scope implicitly is deprecated; use in advance an
8.16 (fiat-core parsers parsers-examples coq-ci): src/Common/Frame.v#L215
Notation Le.le_refl is deprecated since 8.16.