6.1. Import the core API🔗

If the application already owns its model loop, import only LeanProfiler:

import LeanProfiler

open LeanProfiler

def runModel (config : ProfilerConfig) : IO Unit :=
  profile config "training" do
    span "model.forward" forward
    span "loss.backward" backward
    span "optimizer.step" optimizerStep

Use the integration package to reuse its runner, MLP workload, or CUDA hooks:

[[require]]
name = "LeanProfilerTorchLean"
git = "https://github.com/lean-dojo/LeanProfiler"
rev = "main"
subDir = "integrations/TorchLean"

Then import LeanProfilerTorchLean or one of its focused modules.