feat: snapshot trees and language processors

[Kha]

trafficstars

This is the foundation for work on making processing in the language server both more fine-grained (incremental tactics) as well as parallel.

Includes:

• #2959
• #3013

TODOs before merging:

• [x] bring back cached InteractiveDiagnostics
• [x] bring back edit delay or not?
  • replaced with reporting delay
• [x] benchmarking
• [ ] manual regression testing
• [x] investigate sanitize and wasm failures (#3106)

Cleanup TODOs for further PRs:

• [x] make LSP request handlers Language-specific (#3101)
• [ ] get rid of AsyncList remnants
• [x] allow use of other language processors, i.e. #lang (#3101)

[Kha]

!bench

[leanprover-community-mathlib4-bot]

• ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-02 15:24:38)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. (2024-01-25 17:14:01)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ea665de4536061cb8b6a1b32f5b69f09d50ac335 --onto 8b8e001794e6a8b481d37f24fa77bb07797682a1. (2024-02-21 17:03:35)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 67c9498892bfb3bd20e24ceca4c94b467e735ad4 --onto 5a330917326cfc6e8afd37c0b78a72ccb9d1f09d. (2024-02-29 17:24:41)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6af7a01af643e82e1deeb6b7523b8099d177b159 --onto 611b1746896bbadf459c00cc218fa31cf51b4e08. (2024-03-07 17:19:45)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 995726f75fd7eed223c2189a54f6df3293185327 --onto 317adf42e92a4dbe07295bc1f0429b61bb8079fe. (2024-03-14 13:42:08)

[leanprover-bot]

Here are the benchmark results for commit daf6fde5b8699898d5d95e52605bbfe415ca8ea5. There were significant changes against commit 6d23450642c637e4c2f37e9501797c42228a87a5:

  Benchmark                  Metric                  Change
  ====================================================================
- lake build clean           task-clock               26.9%   (18.5 σ)
- lake build clean           wall-clock               12.7%   (14.1 σ)
- reduceMatch                instructions              2.2%   (25.8 σ)
- stdlib                     attribute application    12.4%   (22.5 σ)
- stdlib                     instructions              1.7%  (368.0 σ)
- stdlib                     tactic execution          7.7%   (19.3 σ)
- stdlib                     task-clock               12.8%   (71.6 σ)
- stdlib                     type checking            16.6% (1442.9 σ)
- stdlib                     wall-clock               12.7%   (81.1 σ)
- tests/bench/ interpreted   instructions              2.1%  (371.3 σ)
- workspaceSymbols           instructions              1.2%   (35.7 σ)
- workspaceSymbols           maxrss                   15.9%   (21.1 σ)

[Kha]

Temporarily disabling full-ci so we get a PR release

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 6ec85ec80241ae5815afbd611b481150603f9948. There were significant changes against commit d279a4871fa641f9bc423404cf2797fd3c26426e:

  Benchmark   Metric             Change
  ==============================================
- stdlib      tactic execution     1.0% (11.7 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 959fa55645dd7b25174bba112b44c19e4faa61ba. There were no significant changes against commit 6af7a01af643e82e1deeb6b7523b8099d177b159.

[Kha]

Saving original PR description -

TODOs before merging:

• [x] bring back cached InteractiveDiagnostics
• [x] bring back edit delay or not?
  • replaced with reporting delay
• [x] benchmarking
• [x] manual regression testing
• [x] investigate sanitize and wasm failures (#3106)

Cleanup TODOs for further PRs:

• [x] make LSP request handlers Language-specific (#3101)
• [ ] get rid of AsyncList remnants
• [x] allow use of other language processors, i.e. #lang (#3101)