Skip to content
continuous integration

Update lean-toolchain for testing https://github.com/leanprover/lean4… #199332

Sign in to view logs

Update lean-toolchain for testing https://github.com/leanprover/lean4…

Update lean-toolchain for testing https://github.com/leanprover/lean4… #199332

Triggered via push June 17, 2025 21:27
@ghostghost
pushed 7a4bf74
lean-pr-testing-8577
Status Failure
Total duration 4m 8s
Artifacts –

build.yml

on: push
Lint style
1m 38s
Lint style
Build
4m 5s
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.