Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
a79c6c44ff
This PR adds human-friendly demangling of Lean symbol names in runtime backtraces. When a Lean program panics, stack traces now show readable names instead of mangled C identifiers. **Before:** ``` 3 libleanshared.dylib 0x1119afab4 l_Lean_Meta_Grind_main___redArg___lam__0___boxed + 52 5 libleanshared.dylib 0x10db232fc l_Lean_profileitIOUnsafe___redArg___lam__0 + 20 14 libleanshared.dylib 0x11204ec80 l___private_Lean_Meta_Tactic_Grind_Main_0__Lean_Meta_Grind_withProtectedMCtx_main___at___00Lean_Meta_Grind_withProtectedMCtx___at___00Lean_Elab_Tactic_grind_spec__1_spec__1___redArg___lam__0 + 516 17 libleanshared.dylib 0x10de2aa24 l___private_Lean_Meta_Basic_0__Lean_Meta_withNewMCtxDepthImp___redArg + 648 ``` **After:** ``` 3 libleanshared.dylib 0x1119afab4 Lean.Meta.Grind.main [boxed, λ, arity↓] + 52 5 libleanshared.dylib 0x10db232fc Lean.profileitIOUnsafe [λ, arity↓] + 20 14 libleanshared.dylib 0x11204ec80 Lean.Meta.Grind.withProtectedMCtx.main [private] spec at Lean.Meta.Grind.withProtectedMCtx spec at Lean.Elab.Tactic.grind[arity↓, λ] + 516 17 libleanshared.dylib 0x10de2aa24 Lean.Meta.withNewMCtxDepthImp [arity↓, private] + 648 ``` The demangler is a C++ port of `Name.demangleAux` from `NameMangling.lean` with human-friendly postprocessing: - Suffix folding: `_redArg` → `[arity↓]`, `_boxed` → `[boxed]`, `_lam_N` → `[λ]`, `_closed_N` → `[closed]`, `_jp_N` → `[jp]` - Private name cleanup: `_private.Module.0.Name.foo` → `Name.foo [private]` - Specialization context: `_at_`/`_spec` → `spec at ...` - Hygienic suffix stripping: `_@` onward removed - Runtime helpers: `lean_apply_N` → `<apply/N>` - LLVM artifacts: `.cold.N` suffix preserved Supports both macOS and Linux `backtrace_symbols` formats. Set `LEAN_BACKTRACE_RAW=1` to disable demangling and get raw symbol names. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> |
||
|---|---|---|
| .claude | ||
| .github | ||
| doc | ||
| images | ||
| releases_drafts | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .gitpod.Dockerfile | ||
| .gitpod.yml | ||
| .ignore | ||
| CMakeLists.txt | ||
| CMakePresets.json | ||
| CODEOWNERS | ||
| CONTRIBUTING.md | ||
| flake.lock | ||
| flake.nix | ||
| lean-toolchain | ||
| lean.code-workspace | ||
| LICENSE | ||
| LICENSES | ||
| README.md | ||
| RELEASES.md | ||
This is the repository for Lean 4.
About
- Quickstart
- Homepage
- Theorem Proving Tutorial
- Functional Programming in Lean
- Documentation Overview
- Language Reference
- Release notes starting at v4.0.0-m3
- Examples
- External Contribution Guidelines
Installation
See Install Lean.
Contributing
Please read our Contribution Guidelines first.
Building from Source
See Building Lean.