Add opt-in declaration and whole-proof profiling

[ejgallego]

This PR lets agents measure a single declaration or complete proof against an already-loaded Lean environment, without rebuilding the project. The existing runAt and runWith requests accept profile: true, and the CLI exposes --profile, returning elapsed wall time and bounded structured timing scopes.

• Profile an existing declaration by submitting its complete source at its start position in the synced document version; whole tactic sequences support nested and indented proof blocks.
• Include asynchronous proof-body work, preserve semantic diagnostics and cancellation, and keep profiling options and traces out of later handle continuations.
• Return parent/thread relationships and tactic syntax kinds without rendering trace labels. The 1ms threshold and explicit truncation limits keep responses bounded; timings overlap and profiling itself adds overhead.