Skip to content
continuous integration

Trigger CI for https://github.com/leanprover/lean4/pull/3621 #77943

Sign in to view logs

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

Trigger CI for https://github.com/leanprover/lean4/pull/3621 #77943

Triggered via push March 13, 2024 15:05
@leanprover-community-mathlib4-botleanprover-community-mathlib4-bot
pushed b618ced
lean-pr-testing-3621
Status Failure
Total duration 3m 49s
Artifacts –

build.yml

on: push
Lint style
46s
Lint style
Check all files imported
8s
Check all files imported
Build
3m 42s
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

10 errors and 4 warnings
Build
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
Build: Mathlib/Init/Data/Int/Basic.lean#L99
Declaration Int.natAbs_mul_self not found.
Build: Mathlib/Init/Data/Int/Basic.lean#L102
Declaration Int.eq_nat_or_neg not found.
Build: Mathlib/Init/Data/Int/Basic.lean#L138
Declaration Int.sign_mul_natAbs not found.
Build: Mathlib/Init/Data/Int/DivMod.lean#L14
Declaration Int.zero_div not found.
Build: Mathlib/Init/Data/Int/DivMod.lean#L15
Declaration Int.div_zero not found.
Build: Mathlib/Init/Data/Int/DivMod.lean#L16
Declaration Int.mul_sign not found.
Build: Mathlib/Init/Data/Int/Lemmas.lean#L18
Declaration Int.sign_neg not found.
Build: Mathlib/Init/Data/Int/Lemmas.lean#L19
Declaration Int.sign_mul not found.
Build: Mathlib/Init/Data/Int/Lemmas.lean#L20
Declaration Int.add_one_le_iff not found.
Check all files imported
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
check workflows
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
Lint style
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3, actions/setup-python@v4. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
Build
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3, liskin/gh-problem-matcher-wrap@v2. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.