Skip to content

MATHLIB-RADAR.md

Latest commit

 

History

History
65 lines (49 loc) · 3.22 KB

MATHLIB-RADAR.md

File metadata and controls

65 lines (49 loc) · 3.22 KB
Raw

Mathlib Radar flame explorer

Open the explorer.

This view uses the same flame explorer as the whole LeanPool profile, with an adapter for Radar's public Mathlib benchmarks. It descends from Mathlib through its folders to individual files. Switch the width between CPU instructions and source line count.

The snapshot covers 8,556 files: every 8,555 .lean file under Mathlib/ and the root Mathlib.lean. Each has both measurements. The exporter verified the file set against the complete Git tree at the measured commit, with no missing or unknown files. Dependency files such as Aesop and Batteries are excluded, as are separate whole-build aggregate measurements.

The sum is 130,279,453,598,200 CPU instructions and 2,343,682 source lines. Line counts use Radar's definition. Each selected file links to its source at the exact measured Mathlib commit.

Measurements and limits

CPU instruction counts measure file compilation with hardware performance counters. They are distinct from Lean heartbeats and from our source-attributed wall times. The folder hierarchy groups files; it is not a compiler call stack or a build dependency timeline. Summing these file counts also differs from Radar's separate whole-build measurements, which include additional work.

Radar provides no declaration or source-line measurements in this snapshot. The viewer stops at the file and states that limit explicitly. Source line count is a size metric; it is not a timing for each line. A full source-level Mathlib explorer would require a separate capture.

Provenance

The data is a pinned snapshot, not a live mirror. Loading the viewer makes no requests to Radar. File-level values retain the exact values from the API.

Reproduce the export

Save the following inputs into a directory, preserving the names:

  • latest-commit.json: Radar's /api/commits/mathlib4/<commit>/.
  • measurements.json: Radar's /api/compare/mathlib4/<commit>/<commit>/.
  • source-tree.json: GitHub's complete recursive Git tree for that commit.
  • lean-toolchain: Mathlib's file at the same commit.

Then run:

python3 scripts/export-radar.py /path/to/inputs docs/mathlib

The exporter rejects incomplete or mismatched coverage, unsuccessful runs, missing metrics, and duplicate metrics. The viewer shares docs/pool/app.js and docs/pool/style.css with the LeanPool explorer.