Skip to content
continuous integration

Update lean-toolchain for https://github.com/leanprover/lean4/pull/8577 #199560

Sign in to view logs

Update lean-toolchain for https://github.com/leanprover/lean4/pull/8577

Update lean-toolchain for https://github.com/leanprover/lean4/pull/8577 #199560

Triggered via push June 19, 2025 22:38
@ghostghost
pushed e535f02
lean-pr-testing-8577
Status Failure
Total duration 4m 18s
Artifacts –

build.yml

on: push
Lint style
2m 32s
Lint style
Build
4m 17s
Build
Post-Build Step
0s
Post-Build Step
Post-CI job
0s
Post-CI job
CI Success
0s
CI Success
Fit to window
Zoom out
Zoom in

Annotations

9 errors
Build
Process completed with exit code 1.
Build
unknown identifier 'toNatLit?'
Build
unknown constant 'Lean.Meta.DiscrTree.pushArgs'
Build
'Lean.Meta.DiscrTree.pushArgs' not found in the provided declarations:
Build
Process completed with exit code 1.
Build
unknown identifier 'toNatLit?'
Build
unknown constant 'Lean.Meta.DiscrTree.pushArgs'
Build
'Lean.Meta.DiscrTree.pushArgs' not found in the provided declarations:
Build
Process completed with exit code 3.