Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
91bd6e19a7
This PR adds tooling for profiling Lean programs with human-readable function names in Firefox Profiler: - **`script/lean_profile.sh`** — One-command pipeline: record with samply, symbolicate, demangle, and open in Firefox Profiler - **`script/profiler/lean_demangle.py`** — Faithful port of `Name.demangleAux` from `NameMangling.lean`, with a postprocessor that folds compiler suffixes into compact annotations (`[λ, arity↓]`, `spec at context[flags]`) - **`script/profiler/symbolicate_profile.py`** — Resolves raw addresses via samply's symbolication API - **`script/profiler/serve_profile.py`** — Serves demangled profiles to Firefox Profiler without re-symbolication - **`PROFILER_README.md`** — Documentation including a guide to reading demangled names ### Example output in Firefox Profiler | Raw C symbol | Demangled | |---|---| | `l_Lean_Meta_Sym_main` | `Lean.Meta.Sym.main` | | `l_Lean_Meta_foo___redArg___lam__0` | `Lean.Meta.foo [λ, arity↓]` | | `l_Lean_MVarId_withContext___at__...___spec__2___boxed` | `Lean.MVarId.withContext [boxed] spec at Lean.Meta.bar[λ, arity↓]` | Example: <img width="1145" height="570" alt="image" src="https://github.com/user-attachments/assets/8d23cc6a-1b89-4c60-9f4a-9f9f0f6e7697" /> 🤖 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.