Skip to content
continuous integration (staging)

chore: update lean-pr-testing reporting logic, now that the linter al… #7590

Sign in to view logs

chore: update lean-pr-testing reporting logic, now that the linter al…

chore: update lean-pr-testing reporting logic, now that the linter al… #7590

Triggered via push April 18, 2024 02:17
@mathlib-borsmathlib-bors[bot]
pushed 5d6eaba
staging
Status Failure
Total duration 21m 40s
Artifacts –

bors.yml

on: push
Lint style
32s
Lint style
Check all files imported
12s
Check all files imported
Build
21m 33s
Build
Cancel Previous Runs (CI)
3s
Cancel Previous Runs (CI)
check workflows
9s
check workflows
Post-CI job
0s
Post-CI job
Fit to window
Zoom out
Zoom in

Annotations

12 errors
Build: Mathlib/NumberTheory/Harmonic/GammaDeriv.lean#L101
unknown identifier 'ofReal_nat_cast'
Build: Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean#L76
unknown identifier 'rpow_nat_cast'
Build: Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean#L95
unknown identifier 'rpow_nat_cast'
Build: Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean#L95
tactic 'rewrite' failed, equality or iff proof expected
Build: Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean#L202
unknown identifier 'tendsto_nat_cast_atTop_atTop'
Build
The process '/usr/bin/env' failed with exit code 1
Build: Mathlib/NumberTheory/Harmonic/GammaDeriv.lean#L101
unknown identifier 'ofReal_nat_cast'
Build: Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean#L76
unknown identifier 'rpow_nat_cast'
Build: Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean#L95
unknown identifier 'rpow_nat_cast'
Build: Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean#L95
tactic 'rewrite' failed, equality or iff proof expected
Build: Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean#L202
unknown identifier 'tendsto_nat_cast_atTop_atTop'
Build
The process '/usr/bin/bash' failed with exit code 1