feat: lake: use lean --setup

[tydeu]

This PR makes use of lean --setup in Lake builds of Lean modules and adds Lake support for the new .olean artifacts produced by the module system.

Lake now computes the entire transitive import graph of a module for Lean, allowing it eagerly provide the artifacts managed by Lake to Lean via the modules field of lean --setup.

lake setup-file no longer respects the imports passed to it and instead just parses the file's header for imports. This is necessary because import statements are now more complex than a simple module name.

[tydeu]

!bench

[leanprover-bot]

Here are the benchmark results for commit ba6b4db.
There were significant changes against commit 0339cd2:

  Benchmark                            Metric            Change
  ========================================================================
+ Init.Data.BitVec.Lemmas re-elab      branch-misses      -1.3%  (-21.7 σ)
+ Init.Data.List.Sublist re-elab -j4   wall-clock         -1.3% (-322.4 σ)
- lake build clean                     instructions       40.5%  (156.2 σ)
- lake build clean                     maxrss             93.8%   (30.1 σ)
- lake build clean                     task-clock         36.5%   (34.8 σ)
- lake build clean                     wall-clock         84.3%   (36.0 σ)
- lake build no-op                     instructions     4639.7%  (101.2 σ)
- lake build no-op                     maxrss             93.7%  (203.0 σ)
- lake build no-op                     task-clock      15514.6%   (20.2 σ)
- lake build no-op                     wall-clock       2438.8%   (73.6 σ)
+ reduceMatch                          wall-clock         -2.3%  (-20.5 σ)
+ stdlib                               task-clock         -1.5%  (-29.2 σ)