import Lean.Util.Profiler

/-!

Usage:
```sh
lean --run ./script/collideProfiles.lean **/*.lean.json ... > merged.json
```

Merges multiple `trace.profiler.output` profiles into a single one while deduplicating samples with
the same stack. This is useful for building cumulative profiles of medium-to-large projects because
Firefox Profiler cannot handle hundreds of tracks and the deduplication will also ensure that the
profile is small enough for uploading.

As ordering of samples is not meaningful after this transformation, only "Call Tree" and "Flame
Graph" are useful for such profiles.
-/

open Lean

def main (args : List String) : IO Unit := do
  let profiles ← args.toArray.mapM fun path => do
    let json ← IO.FS.readFile ⟨path⟩
    let profile ← IO.ofExcept $ Json.parse json
    IO.ofExcept <| fromJson? profile
  -- NOTE: `collide` should not be interpreted
  let profile := Firefox.Profile.collide profiles
  IO.println <| Json.compress <| toJson profile