Skip to content
continuous integration

update DeriveTraversable meta code #64632

Sign in to view logs

update DeriveTraversable meta code

update DeriveTraversable meta code #64632

Triggered via push January 8, 2024 00:31
@kim-emkim-em
pushed 9786389
lean-pr-testing-3124
Status Failure
Total duration 4m 19s
Artifacts –

build.yml

on: push
Lint style
18s
Lint style
Check all files imported
8s
Check all files imported
Build
4m 11s
Build
Cancel Previous Runs (CI)
3s
Cancel Previous Runs (CI)
check workflows
8s
check workflows
Post-CI job
0s
Post-CI job
Fit to window
Zoom out
Zoom in

Annotations

12 errors
Lint style: Mathlib/Tactic/SimpIntro.lean#L69
Mathlib/Tactic/SimpIntro.lean#L69: ERR_LIN: Line has more than 100 characters
Lint style
Process completed with exit code 123.
Build: Mathlib/Testing/SlimCheck/Sampleable.lean#L203
tactic 'simp' failed, nested error:
Build: Mathlib/GroupTheory/Perm/Basic.lean#L591
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
Build: Mathlib/CategoryTheory/Limits/Opposites.lean#L545
tactic 'simp' failed, nested error:
Build: Mathlib/CategoryTheory/Limits/Opposites.lean#L546
tactic 'simp' failed, nested error:
Build: Mathlib/Combinatorics/Composition.lean#L1000
(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
Build: Mathlib/Combinatorics/Composition.lean#L1018
Declaration Composition.toCompositionAsSet_blocks not found.
Build: Mathlib/Combinatorics/Composition.lean#L1055
invalid field 'toCompositionAsSet_blocks', the environment does not contain 'Composition.toCompositionAsSet_blocks'
Build: Mathlib/Computability/Primrec.lean#L817
(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
Build: Mathlib/Computability/Primrec.lean#L830
Declaration Primrec.nat_div not found.
Build: Mathlib/Computability/Primrec.lean#L833
unknown identifier 'nat_div'