commit: bdaa083aa40761325a4f114b7253900a3354ecc8

[log]
author: Sebastian Ullrich <sebasti@nullri.ch>

Thu Oct 08 16:39:38 2026 +0000
committer: Sebastian Ullrich <sebasti@nullri.ch>

Thu Oct 08 16:40:46 2026 +0000
tree: 5f2d8b150e28d6187eb6f9694220f54733c474f4
parent: 998cfe5c790e8d95a6b1dc391e2e7a388e1cd885 [diff]

perf: do not import `Lean.Elab.Idbg` in `LeanIR`

Its `@[extern]` counterpart `Idbg.idbgClientLoop` is only declared in `Lean.Setup` and never called by `leanir`, so the test exempts it. The import was however the only thing initializing `Lean.Parser`, which implements the parenthesizer and formatter hooks of the pretty printer; import that directly.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

src/LeanIR.lean[diff]

1 file changed

tree: 5f2d8b150e28d6187eb6f9694220f54733c474f4

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.