join construction #2926
Triggered via pull request
September 28, 2024 19:05
Alizter
Status
Failure
Total duration
4m 13s
Artifacts
–
ci.yml
on: pull_request
Matrix: coqchk
Matrix: install
doc-alectryon
0s
doc-dep-graphs
0s
doc-coqdoc
0s
doc-timing
0s
delete-artifacts
6s
Annotations
4 errors and 1 warning
|
nix
Process completed with exit code 1.
|
|
build (latest):
theories/Homotopy/JoinConstruction.v#L209
Could not find an instance for "IsColimit@{HoTT.Homotopy.JoinConstruction.1231
k k k HoTT.Homotopy.JoinConstruction.1224
HoTT.Homotopy.JoinConstruction.1225
HoTT.Homotopy.JoinConstruction.1231} s
(Colimit@{u u u u u u u} s')" in
environment:
H : Funext
s : Sequence@{k k k}
ss : forall n : Graph.graph0@{k k} sequence_graph@{k k}, IsSmall@{u k} (s n)
s' :=
Build_Sequence@{u u u} (fun n : nat => smalltype@{u k} (s n))
((fun (n : nat) (x : smalltype@{u k} (s n)) =>
(equiv_smalltype@{u k} (s n.+1%nat))^-1
(sequence_arr@{k k k} s n (equiv_smalltype@{u k} (s n) x)))
:
forall n : nat,
(fun n0 : nat => smalltype@{u k} (s n0)) n ->
(fun n0 : nat => smalltype@{u k} (s n0)) n.+1%nat) : Sequence@{u u u}
Command exited with non-zero status 1
|
|
build (dev, --warnings):
theories/Homotopy/JoinConstruction.v#L209
Could not find an instance for "IsColimit@{HoTT.Homotopy.JoinConstruction.1231
k k k HoTT.Homotopy.JoinConstruction.1224
HoTT.Homotopy.JoinConstruction.1225
HoTT.Homotopy.JoinConstruction.1231} s
(Colimit@{u u u u u u u} s')"
in
environment:
H : Funext
s : Sequence@{k k k}
ss : forall n : Graph.graph0@{k k} sequence_graph@{k k}, IsSmall@{u k} (s n)
s' :=
Build_Sequence@{u u u} (fun n : nat => smalltype@{u k} (s n))
((fun (n : nat) (x : smalltype@{u k} (s n)) =>
(equiv_smalltype@{u k} (s n.+1%nat))^-1
(sequence_arr@{k k k} s n (equiv_smalltype@{u k} (s n) x)))
:
forall n : nat,
(fun n0 : nat => smalltype@{u k} (s n0)) n ->
(fun n0 : nat => smalltype@{u k} (s n0)) n.+1%nat)
: Sequence@{u u u}
Command exited with non-zero status 1
|
|
build (supported):
theories/Homotopy/JoinConstruction.v#L209
Could not find an instance for "IsColimit@{HoTT.Homotopy.JoinConstruction.1231
k k k HoTT.Homotopy.JoinConstruction.1224
HoTT.Homotopy.JoinConstruction.1225
HoTT.Homotopy.JoinConstruction.1231} s
(Colimit@{u u u u u u u} s')" in
environment:
H : Funext
s : Sequence@{k k k}
ss : forall n : Graph.graph0@{k k} sequence_graph@{k k}, IsSmall@{u k} (s n)
s' := Build_Sequence@{u u u} (fun n : nat => smalltype@{u k} (s n))
((fun (n : nat) (x : smalltype@{u k} (s n)) =>
(equiv_smalltype@{u k} (s n.+1%nat))^-1
(sequence_arr@{k k k} s n (equiv_smalltype@{u k} (s n) x)))
:
forall n : nat,
(fun n0 : nat => smalltype@{u k} (s n0)) n ->
(fun n0 : nat => smalltype@{u k} (s n0)) n.+1%nat) : Sequence@{u u
u}
Command exited with non-zero status 1
|
|
nix
Unexpected input(s) 'name', 'authToken', 'extraPullNames', valid inputs are ['extra_nix_config', 'github_access_token', 'install_url', 'install_options', 'nix_path']
|