5.6. Use both around a foreign boundary🔗

A Lean program calling PyTorch or LibTorch can place a LeanProfiler span around the foreign call and start the framework profiler inside that runtime. The outer span answers how long the Lean caller waited and how the call fits among surrounding application phases. The inner trace explains the operators and supported device activity responsible for that interval.

Correlating the files requires a shared identifier or timestamp convention supplied by the adapter. Two unrelated timelines should not be aligned by eye and presented as one clock.