refactor: add MonadLift CoreM CommandElabM

[Kha]

No description provided.

[Kha]

!bench

[leanprover-radar]

Benchmark results for 897ef1b against dc7c184 are in! @Kha

[leanprover-bot]

Here are the benchmark results for commit 897ef1b.
There were significant changes against commit dc7c184:

  Benchmark                            Metric                    Change
  ===============================================================================
- Init.Data.List.Sublist async         branches                    1.8%  (97.5 σ)
- Init.Data.List.Sublist async         instructions                1.6%  (75.8 σ)
- Init.Prelude async                   branches                    3.6% (244.5 σ)
- Init.Prelude async                   instructions                3.3% (196.8 σ)
- Std.Data.Internal.List.Associative   branches                    1.6% (181.9 σ)
- Std.Data.Internal.List.Associative   instructions                1.4% (155.2 σ)
+ big_deceq_rec                        branch-misses              -1.5% (-20.6 σ)
+ libleanshared.so                     binary size                -1.9%
- stdlib                               process pre-definitions     1.4%  (22.9 σ)
- stdlib                               type checking               1.3%  (62.6 σ)
+ stdlib size                          bytes .ir                  -1.5%
+ stdlib size                          lines C                    -1.4%
+ stdlib size                          max dynamic symbols        -1.7%
+ tests/compiler                       sum binary sizes           -1.3%

[Kha]

!bench

[leanprover-radar]

Benchmark results for 671e6c1 against dc7c184 are in! @Kha

[leanprover-bot]

Here are the benchmark results for commit 671e6c1.
There were significant changes against commit dc7c184:

  Benchmark                      Metric                       Change
  ============================================================================
- Init.Data.List.Sublist async   branches                       1.1%  (45.6 σ)
- Init.Prelude async             branches                       2.5%  (85.5 σ)
- Init.Prelude async             instructions                   2.3%  (72.3 σ)
- binarytrees                    maxrss                         2.1%  (76.0 σ)
+ libleanshared.so               binary size                   -1.9%
+ stdlib                         grind mark subsingleton       -2.0% (-31.4 σ)
- stdlib                         let-to-have transformation     1.5%  (67.6 σ)
+ stdlib size                    bytes .ir                     -1.5%
+ stdlib size                    lines C                       -1.4%
+ stdlib size                    max dynamic symbols           -1.7%
+ tests/compiler                 sum binary sizes              -1.3%

[Kha]

!bench

[leanprover-radar]

Benchmark results for 94f1c74 against dc7c184 are in! @Kha

[leanprover-bot]

Here are the benchmark results for commit 94f1c74.
There were significant changes against commit dc7c184:

  Benchmark            Metric                       Change
  ===================================================================
- Init.Prelude async   branches                       1.4%   (61.1 σ)
- Init.Prelude async   instructions                   1.3%   (46.4 σ)
- channel.lean         boundedn_seq                   1.4%
+ libleanshared.so     binary size                   -1.9%
+ riscv-ast.lean       maxrss                        -1.6%  (-39.0 σ)
+ riscv-ast.lean       task-clock                    -1.7% (-341.4 σ)
+ simp_subexpr         task-clock                    -2.8%  (-35.7 σ)
+ simp_subexpr         wall-clock                    -2.9%  (-30.3 σ)
+ stdlib               compilation (IR)              -1.8%  (-25.1 σ)
- stdlib               let-to-have transformation     3.0%   (21.2 σ)
+ stdlib               tactic execution              -1.2%  (-22.9 σ)
+ stdlib size          bytes .ir                     -1.5%
+ stdlib size          lines C                       -1.3%
+ stdlib size          max dynamic symbols           -1.7%
+ tests/compiler       sum binary sizes              -1.3%
+ unionfind            task-clock                   -11.5%  (-20.1 σ)
+ unionfind            wall-clock                   -11.4%  (-20.0 σ)

[Kha]

!bench

[leanprover-radar]

Benchmark results for b5ddb00 against dc7c184 are in! @Kha

[leanprover-bot]

Here are the benchmark results for commit b5ddb00.
There were significant changes against commit dc7c184:

  Benchmark                 Metric                      Change
  =======================================================================
- Init.Prelude async        branches                      1.3%  (168.4 σ)
- Init.Prelude async        instructions                  1.2%  (130.1 σ)
- binarytrees               maxrss                        2.1%   (34.7 σ)
- channel.lean              boundedn_seq                  1.4%
+ libleanshared.so          binary size                  -1.7%
+ omega_stress.lean async   branch-misses                -2.3%  (-20.8 σ)
+ riscv-ast.lean            branch-misses                -3.1%  (-92.5 σ)
+ stdlib                    grind typeclass inference    -2.3% (-194.8 σ)
+ stdlib                    longest rebuild path         -1.9%  (-31.8 σ)
+ stdlib size               bytes .ir                    -1.3%
+ stdlib size               lines C                      -1.2%
+ stdlib size               max dynamic symbols          -1.7%
+ tests/compiler            sum binary sizes             -1.2%

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase dc7c184ee287ed4ad8fd19165349965cd85d1977 --onto 4ce7ad19cea348506876685a19a7e0cca442c6d0. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-18 15:30:31)
• 💥 Mathlib branch lean-pr-testing-10829 build failed against this PR. (2025-10-18 17:19:31) View Log

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase dc7c184ee287ed4ad8fd19165349965cd85d1977 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-18 15:30:32)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-17 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-10-18 17:15:32)