6.2. After main: LeanProfiler🔗

LeanProfiler measures boundaries chosen by the Lean application. A source indexer can use names that do not exist inside the compiler or a foreign library:

profileFromEnvironment "indexer.run" do
  for (sourcePath, fileIndex) in sourcePaths.zipIdx do
    withStep fileIndex do
      let contents ← span "source.read" (readSource sourcePath)
      let syntax ← span "source.parse" (parseSource contents)
      span "source.analyze" (analyzeSource syntax)

Its measurements come from Lean and Std runtime APIs:

• IO.monoNanosNow for monotonic span boundaries;

• IO.getTID for the current Lean thread;

• IO.Process.getPID for Trace Event process identity;

• IO.getNumHeartbeats for the current thread's work counter;

• Std.IO.Process.getResourceUsage for session-wide process counters.

Heartbeats add a Lean-specific signal alongside elapsed time. LeanProfiler does not discover operations by itself: the application decides where a span begins, what it is called, and which metadata it carries.

None of these APIs produces accelerator kernel timestamps. A completion hook can synchronize a device and attach allocator counters, but an absent field means “not observed,” not zero.