Skip to content
continuous integration

Trigger CI for https://github.com/leanprover/lean4/pull/3756 #87099

Sign in to view logs

Trigger CI for https://github.com/leanprover/lean4/pull/3756

Trigger CI for https://github.com/leanprover/lean4/pull/3756 #87099

Triggered via push April 25, 2024 16:17
@leanprover-community-mathlib4-botleanprover-community-mathlib4-bot
pushed 0f7d60e
lean-pr-testing-3756
Status Failure
Total duration 15m 41s
Artifacts –

build.yml

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

Annotations

20 errors
Build: Mathlib/Data/Nat/Bits.lean#L138
'Nat.bit' has already been declared
Build: Mathlib/Data/Nat/Bits.lean#L151
'Nat.bit_val' has already been declared
Build: Mathlib/Data/Nat/Bits.lean#L164
'Nat.bitCasesOn' has already been declared
Build: Mathlib/Data/Nat/Bits.lean#L204
'Nat.binaryRec' has already been declared
Build: Mathlib/Data/Nat/Bits.lean#L244
'Nat.binaryRec_zero' has already been declared
Build: Mathlib/Data/Nat/Bits.lean#L289
unknown identifier 'and_one_is_mod'
Build: Mathlib/Data/Nat/Bits.lean#L299
type mismatch
Build: Mathlib/Data/Nat/Bits.lean#L307
type mismatch
Build: Mathlib/Data/Nat/Bits.lean#L310
'Nat.binaryRec_eq' has already been declared
Build: Mathlib/Data/Nat/Bits.lean#L417
'Nat.bitCasesOn_bit' has already been declared
Build: Mathlib/Data/Nat/Bits.lean#L138
'Nat.bit' has already been declared
Build: Mathlib/Data/Nat/Bits.lean#L151
'Nat.bit_val' has already been declared
Build: Mathlib/Data/Nat/Bits.lean#L164
'Nat.bitCasesOn' has already been declared
Build: Mathlib/Data/Nat/Bits.lean#L204
'Nat.binaryRec' has already been declared
Build: Mathlib/Data/Nat/Bits.lean#L244
'Nat.binaryRec_zero' has already been declared
Build: Mathlib/Data/Nat/Bits.lean#L289
unknown identifier 'and_one_is_mod'
Build: Mathlib/Data/Nat/Bits.lean#L299
type mismatch
Build: Mathlib/Data/Nat/Bits.lean#L307
type mismatch
Build: Mathlib/Data/Nat/Bits.lean#L310
'Nat.binaryRec_eq' has already been declared
Build: Mathlib/Data/Nat/Bits.lean#L417
'Nat.bitCasesOn_bit' has already been declared