feat: enable the new compiler #8577

zwarich · 2025-06-01T19:50:54Z

This PR enables the new compiler by default, adjusts test results, and updates stage0.

zwarich · 2025-06-01T19:52:55Z

!bench

leanprover-community-bot · 2025-06-01T20:16:00Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 193f59aefeb1fd233656c811444bb014f94e8129 --onto 72141b05fd9a3328c1e5d99211dc4da4495cbd42. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-01 20:16:00)
❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-06-14 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-14 15:33:52)
❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-06-15 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-15 22:03:57)
💥 Mathlib branch lean-pr-testing-8577 build failed against this PR. (2025-06-17 21:31:20) View Log
💥 Mathlib branch lean-pr-testing-8577 build failed against this PR. (2025-06-19 22:43:11) View Log
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 50cfe354bee117c3471abe1bbf54780696674566 --onto db499e96aac8ad654c8ed5ab40c4e6885d38c9a1. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-20 13:44:59)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a8d5982fce107e702ba92042ff51a7545c7f3a0d --onto db499e96aac8ad654c8ed5ab40c4e6885d38c9a1. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-20 15:34:26)
❌ Mathlib branch lean-pr-testing-8577 built against this PR, but testing failed. (2025-06-22 04:34:50) View Log

leanprover-bot · 2025-06-01T20:52:42Z

Here are the benchmark results for commit 52cfb7c.
There were significant changes against commit 193f59a:

  Benchmark                              Metric                   Change
  ===================================================================================
- Init size                              bytes .olean               7.1%
- Init.Data.BitVec.Lemmas                branch-misses              9.6%     (21.2 σ)
- Init.Data.BitVec.Lemmas                branches                   8.3%    (435.0 σ)
- Init.Data.BitVec.Lemmas                instructions               7.7%    (379.0 σ)
- Init.Data.BitVec.Lemmas                wall-clock                 9.3%     (42.3 σ)
- Init.Data.BitVec.Lemmas re-elab        branch-misses              9.3%     (66.0 σ)
- Init.Data.BitVec.Lemmas re-elab        branches                   8.0%    (281.3 σ)
- Init.Data.BitVec.Lemmas re-elab        instructions               7.4%    (247.0 σ)
- Init.Data.List.Sublist async           branches                   8.1%    (342.2 σ)
- Init.Data.List.Sublist async           instructions               8.0%    (290.9 σ)
- Init.Data.List.Sublist re-elab -j4     branches                   7.9%     (53.6 σ)
- Init.Data.List.Sublist re-elab -j4     instructions               7.7%     (53.0 σ)
- Init.Data.List.Sublist re-elab -j4     task-clock                 5.4%     (26.2 σ)
- Init.Data.List.Sublist re-elab -j4     wall-clock                 5.8%     (29.0 σ)
- Init.Prelude async                     branches                  20.9%   (1000.4 σ)
- Init.Prelude async                     instructions              18.7%    (773.0 σ)
- Std.Data.DHashMap.Internal.RawLemmas   branch-misses             11.9%     (39.7 σ)
- Std.Data.DHashMap.Internal.RawLemmas   branches                   8.1%   (1706.1 σ)
- Std.Data.DHashMap.Internal.RawLemmas   instructions               8.0%   (1408.9 σ)
- Std.Data.Internal.List.Associative     branch-misses             10.6%     (25.5 σ)
- Std.Data.Internal.List.Associative     branches                   7.5%    (668.6 σ)
- Std.Data.Internal.List.Associative     instructions               7.6%    (605.3 σ)
- big_do                                 branches                9408.3%     (43.8 σ)
- big_do                                 instructions            8224.9%     (35.5 σ)
- big_do                                 maxrss                   898.1%     (78.7 σ)
- big_omega.lean                         branches                   5.4%    (353.3 σ)
- big_omega.lean                         instructions               3.8%    (244.9 σ)
- big_omega.lean MT                      branches                   5.4%    (359.5 σ)
- big_omega.lean MT                      instructions               3.9%    (343.6 σ)
- bv_decide_inequality.lean              branches                   6.6%    (120.6 σ)
- bv_decide_inequality.lean              instructions               5.2%     (97.0 σ)
+ bv_decide_large_aig.lean               branches                  -5.5%   (-345.4 σ)
+ bv_decide_large_aig.lean               instructions              -4.7%   (-361.2 σ)
- bv_decide_mod                          branches                   6.0%     (85.1 σ)
- bv_decide_mod                          instructions               4.9%     (72.9 σ)
- bv_decide_mul                          branches                   8.8%    (440.0 σ)
- bv_decide_mul                          instructions               7.7%    (397.3 σ)
- bv_decide_mul                          wall-clock                 3.9%     (20.6 σ)
- bv_decide_realworld                    branches                  10.0%     (84.9 σ)
- bv_decide_realworld                    instructions               8.2%     (68.1 σ)
- bv_decide_realworld                    wall-clock                 8.6%     (34.2 σ)
- deriv                                  instructions               5.8%   (2287.9 σ)
- identifier auto-completion             branches                   3.4%     (43.9 σ)
- identifier auto-completion             instructions               3.0%     (32.4 σ)
+ identifier auto-completion             maxrss                    -3.7%    (-20.4 σ)
- ilean roundtrip                        branches                   5.7%    (436.8 σ)
- ilean roundtrip                        instructions               5.3%    (444.8 σ)
+ import Lean                            branches                 -15.0%  (-1127.8 σ)
+ import Lean                            instructions             -15.5%   (-914.4 σ)
+ import Lean                            maxrss                   -14.9%  (-1723.8 σ)
+ lake build clean                       instructions              -2.0%    (-34.6 σ)
+ lake build clean                       maxrss                    -8.5%    (-42.4 σ)
+ lake build clean                       task-clock                -6.9%    (-23.4 σ)
- lake build no-op                       instructions               2.3%     (20.1 σ)
- lake config elab                       instructions               9.6%    (567.0 σ)
+ lake config elab                       maxrss                   -12.0%   (-309.3 σ)
+ lake config import                     instructions             -13.7%   (-289.4 σ)
+ lake config import                     maxrss                   -13.2%   (-266.8 σ)
+ lake config tree                       instructions             -15.3%   (-761.9 σ)
+ lake config tree                       maxrss                   -13.1%   (-231.6 σ)
+ lake config tree                       task-clock               -22.5%    (-21.4 σ)
+ lake config tree                       wall-clock               -22.3%    (-21.3 σ)
+ lake env                               instructions             -13.3%   (-670.1 σ)
+ lake env                               maxrss                   -13.1%   (-313.7 σ)
- lake startup                           instructions               1.7%     (55.0 σ)
+ language server startup                instructions              -1.1%    (-20.7 σ)
- liasolver                              instructions               1.0%    (224.2 σ)
+ libleanshared.so                       binary size              -12.1%
- omega_stress.lean async                branch-misses              9.6%     (25.5 σ)
- omega_stress.lean async                branches                   6.2%    (322.2 σ)
- omega_stress.lean async                instructions               5.5%    (246.7 σ)
+ parser                                 instructions              -2.0%   (-460.8 σ)
- rbmap                                  instructions             210.9%  (28329.7 σ)
+ rbmap_1                                instructions             -13.8% (-11726.1 σ)
- rbmap_10                               instructions             144.7%   (9203.8 σ)
- rbmap_library                          instructions             199.4%  (25514.2 σ)
+ reduceMatch                            wall-clock                -4.8%    (-24.8 σ)
- riscv-ast.lean                         branches                   3.2%     (55.8 σ)
- riscv-ast.lean                         instructions               2.6%     (44.2 σ)
- simp_arith1                            branches                   3.3%     (67.2 σ)
+ simp_arith1                            maxrss                   -13.3%   (-115.1 σ)
- stdlib                                 blocked                    8.9%     (64.4 σ)
- stdlib                                 blocked (unaccounted)     25.3%     (68.3 σ)
- stdlib                                 instructions              23.4%  (11237.8 σ)
+ stdlib                                 maxrss                   -14.8%  (-2287.5 σ)
- stdlib                                 tactic execution           9.4%     (33.2 σ)
- stdlib                                 task-clock                12.6%    (132.6 σ)
- stdlib                                 wall-clock                34.8%     (36.9 σ)
- stdlib size                            bytes .olean               6.7%
+ stdlib size                            lines C                  -18.3%
+ stdlib size                            max dynamic symbols      -12.0%
- tests/bench/ interpreted               instructions               6.2%    (534.1 σ)
+ tests/bench/ interpreted               maxrss                   -12.9%   (-276.3 σ)
+ tests/compiler                         sum binary sizes          -8.9%
+ unionfind                              instructions              -1.7%   (-502.3 σ)
+ workspaceSymbols                       instructions             -80.2% (-63155.5 σ)
+ workspaceSymbols                       maxrss                   -15.2%  (-1735.1 σ)
+ workspaceSymbols                       task-clock               -77.1%    (-82.7 σ)
+ workspaceSymbols                       wall-clock               -77.2%    (-82.0 σ)

zwarich · 2025-06-01T23:18:35Z

The big_do slowdown is due to bad asymptotic behavior in LCNF simp, not the compiled code. The rbmap slowdowns appear to be due to the new compiler being better about using join points, but this appears to cause the reference counting optimizations to make suboptimal decisions (optimizing the first join point it sees, and then doing nothing for the other code paths).

zwarich · 2025-06-14T15:00:37Z

!bench

zwarich · 2025-06-14T15:16:12Z

Sadly this won't build Mathlib, even if I push the required changes, because lean4 nightly and mathlib4 nightly-testing are already broken with each other.

leanprover-bot · 2025-06-14T15:32:54Z

Here are the benchmark results for commit 5ec19d8.
There were significant changes against commit 4445958:

  Benchmark                              Metric                        Change
  =========================================================================================
- Init size                              bytes .olean                    6.7%
- Init.Data.BitVec.Lemmas                branches                        4.9%     (497.0 σ)
- Init.Data.BitVec.Lemmas                instructions                    4.5%     (412.9 σ)
- Init.Data.BitVec.Lemmas re-elab        branches                        4.7%      (43.4 σ)
- Init.Data.BitVec.Lemmas re-elab        instructions                    4.3%      (42.3 σ)
- Init.Data.List.Sublist async           branches                        4.8%     (354.6 σ)
- Init.Data.List.Sublist async           instructions                    4.7%     (362.4 σ)
- Init.Data.List.Sublist re-elab -j4     branches                        4.6%     (101.5 σ)
- Init.Data.List.Sublist re-elab -j4     instructions                    4.5%     (106.3 σ)
- Init.Prelude async                     branches                        8.3%     (261.9 σ)
- Init.Prelude async                     instructions                    6.4%     (176.9 σ)
- Std.Data.DHashMap.Internal.RawLemmas   branches                        4.9%     (414.7 σ)
- Std.Data.DHashMap.Internal.RawLemmas   instructions                    4.7%     (344.9 σ)
- Std.Data.Internal.List.Associative     branches                        5.2%     (584.2 σ)
- Std.Data.Internal.List.Associative     instructions                    5.1%     (498.9 σ)
- big_do                                 branches                      137.9%    (3496.5 σ)
- big_do                                 instructions                  127.6%    (2744.3 σ)
- big_do                                 task-clock                     90.3%     (134.0 σ)
- big_do                                 wall-clock                     92.8%     (134.6 σ)
- big_omega.lean                         branches                        2.6%     (223.4 σ)
- big_omega.lean                         instructions                    1.5%     (173.0 σ)
- big_omega.lean MT                      branches                        2.7%     (597.7 σ)
- big_omega.lean MT                      instructions                    1.6%     (396.4 σ)
- bv_decide_inequality.lean              branches                      117.1%   (11111.5 σ)
- bv_decide_inequality.lean              instructions                   76.8%    (7219.5 σ)
+ bv_decide_inequality.lean              maxrss                         -4.6%    (-608.6 σ)
+ bv_decide_large_aig.lean               branches                       -5.5%    (-220.7 σ)
+ bv_decide_large_aig.lean               instructions                   -4.9%    (-199.9 σ)
- bv_decide_mod                          branches                     1117.6%   (51305.2 σ)
- bv_decide_mod                          instructions                  749.6%   (38282.1 σ)
- bv_decide_mul                          branches                     1554.7%   (29797.6 σ)
- bv_decide_mul                          instructions                 1112.9%   (20634.8 σ)
- bv_decide_mul                          task-clock                    414.9%     (406.2 σ)
- bv_decide_mul                          wall-clock                    412.6%     (380.7 σ)
- bv_decide_realworld                    branches                      200.6%    (1776.1 σ)
- bv_decide_realworld                    instructions                  144.6%    (1183.8 σ)
- bv_decide_realworld                    task-clock                     61.8%      (74.0 σ)
- bv_decide_realworld                    wall-clock                     34.5%      (30.7 σ)
+ channel.lean                           boundedn_seq                  -10.4%
- deriv                                  instructions                    5.8%    (2555.3 σ)
- identifier auto-completion             branches                        2.5%      (49.7 σ)
- identifier auto-completion             instructions                    2.2%      (37.3 σ)
+ identifier auto-completion             maxrss                         -3.9%     (-29.2 σ)
- ilean roundtrip                        branches                        5.6%    (3182.3 σ)
- ilean roundtrip                        instructions                    5.3%     (703.4 σ)
+ import Lean                            branches                      -17.7%   (-1489.9 σ)
+ import Lean                            instructions                  -18.0%   (-1383.6 σ)
+ import Lean                            maxrss                        -15.3%    (-150.8 σ)
+ lake build clean                       instructions                   -5.9%    (-251.5 σ)
+ lake build clean                       maxrss                         -9.0%     (-86.3 σ)
+ lake build clean                       wall-clock                     -6.6%     (-31.4 σ)
+ lake config elab                       instructions                   -3.7%    (-962.3 σ)
+ lake config elab                       maxrss                        -12.7%    (-247.5 σ)
+ lake config import                     instructions                  -15.3%    (-985.5 σ)
+ lake config import                     maxrss                        -13.4%    (-169.0 σ)
+ lake config tree                       instructions                  -16.9%   (-1116.9 σ)
+ lake config tree                       maxrss                        -13.4%    (-536.2 σ)
+ lake env                               instructions                  -15.1%    (-775.1 σ)
+ lake env                               maxrss                        -13.4%    (-178.9 σ)
- lake startup                           instructions                    1.4%      (27.5 σ)
+ language server startup                branches                       -7.3%   (-1030.1 σ)
+ language server startup                instructions                   -8.7%   (-1509.4 σ)
+ language server startup                maxrss                         -6.3%     (-24.2 σ)
+ liasolver                              instructions                   -2.8%    (-393.6 σ)
+ libleanshared.so                       binary size                   -14.2%
- omega_stress.lean async                branches                        1.9%      (99.6 σ)
- omega_stress.lean async                instructions                    1.6%      (73.1 σ)
- parser                                 instructions                    1.8%    (1858.9 σ)
+ qsort                                  task-clock                     -8.8%     (-24.2 σ)
+ qsort                                  wall-clock                     -8.8%     (-24.2 σ)
- rbmap                                  instructions                  210.9%   (26898.4 σ)
+ rbmap_1                                instructions                  -13.8%  (-10142.3 σ)
- rbmap_10                               instructions                  144.7%   (51644.3 σ)
- rbmap_10                               task-clock                     94.3%      (70.6 σ)
- rbmap_10                               wall-clock                     94.2%      (70.0 σ)
- rbmap_library                          instructions                  199.1%   (25320.7 σ)
- rbmap_library                          task-clock                    169.6%      (81.2 σ)
- rbmap_library                          wall-clock                    169.3%      (81.4 σ)
+ reduceMatch                            instructions                   -3.1%    (-182.4 σ)
+ simp_arith1                            branches                       -5.8%    (-106.5 σ)
+ simp_arith1                            instructions                   -7.0%    (-107.2 σ)
+ simp_arith1                            maxrss                        -13.8%    (-134.2 σ)
+ stdlib                                 blocked (unaccounted)         -18.6%    (-663.3 σ)
+ stdlib                                 grind                         -13.9%     (-69.4 σ)
+ stdlib                                 instructions                   -5.4%   (-3489.6 σ)
+ stdlib                                 maxrss                        -14.9%    (-229.7 σ)
- stdlib                                 number of imported bytes        2.1%
+ stdlib                                 number of imported consts     -54.9%
- stdlib                                 number of imported entries     21.6%
+ stdlib                                 task-clock                     -5.9%     (-53.5 σ)
+ stdlib                                 wall-clock                     -5.6%     (-57.0 σ)
- stdlib size                            bytes .olean                    4.9%
+ stdlib size                            lines C                       -20.3%
+ stdlib size                            max dynamic symbols           -13.2%
- tests/bench/ interpreted               instructions                    2.2%     (432.3 σ)
+ tests/bench/ interpreted               maxrss                        -13.3%   (-3577.1 σ)
+ tests/compiler                         sum binary sizes              -10.4%
+ unionfind                              instructions                   -1.7%   (-3482.5 σ)
+ unionfind                              task-clock                    -13.7%     (-33.4 σ)
+ unionfind                              wall-clock                    -13.7%     (-33.7 σ)
+ workspaceSymbols                       instructions                  -81.2% (-446754.1 σ)
+ workspaceSymbols                       maxrss                        -15.9%   (-1270.3 σ)
+ workspaceSymbols                       task-clock                    -79.0%   (-3585.1 σ)
+ workspaceSymbols                       wall-clock                    -79.0%   (-3654.8 σ)

zwarich · 2025-06-14T16:48:13Z

The benchmark numbers generally look improved.

Elaboration times are actually improved when testing files other than Prelude, for reasons I have not yet discovered.

The remaining big_do regression is mostly due to the old compiler inlining all local fun decls, and forcing the new compiler to do the same makes this way closer. There are a few different things we could do to improve this, but I don’t really feel like tweaking inlining heuristics (especially for an individual test) until we add recursive join points.

The rbmap regression is due to reuse optimizations being pessimistic in the face of increased usage of join points. It is possible to fix this (and in fact is probably required for correctness with recursion JPs), but it my attempt fails for other reasons (e.g. similar bugs in later passes) I will defer it until after we enable the new compiler.

The only new thing here is a large number of bv_decide regressions, which seem so bad that they must be due to a shared linearity regression. Hopefully it won’t be too difficult to debug the underlying cause.

zwarich · 2025-06-15T21:32:16Z

!bench

zwarich · 2025-06-15T21:32:31Z

(this is testing a fix for the bv_decide linearity issue)

leanprover-bot · 2025-06-15T22:01:08Z

Here are the benchmark results for commit 820593b.
There were significant changes against commit 957b904:

  Benchmark                              Metric                       Change
  =========================================================================================
- Init size                              bytes .olean                   6.8%
- Init.Data.BitVec.Lemmas                branches                       4.6%      (259.8 σ)
- Init.Data.BitVec.Lemmas                instructions                   4.3%      (220.6 σ)
- Init.Data.BitVec.Lemmas re-elab        branches                       4.6%       (52.3 σ)
- Init.Data.BitVec.Lemmas re-elab        instructions                   4.3%       (51.4 σ)
- Init.Data.List.Sublist async           branches                       4.7%       (79.3 σ)
- Init.Data.List.Sublist async           instructions                   4.7%       (70.0 σ)
- Init.Data.List.Sublist re-elab -j4     branches                       4.6%      (421.6 σ)
- Init.Data.List.Sublist re-elab -j4     instructions                   4.6%      (337.1 σ)
+ Init.Data.List.Sublist re-elab -j4     maxrss                        -8.8%      (-22.7 σ)
- Init.Prelude async                     branches                       8.3%      (357.1 σ)
- Init.Prelude async                     instructions                   6.5%      (266.3 σ)
- Std.Data.DHashMap.Internal.RawLemmas   branches                       4.9%     (1611.9 σ)
- Std.Data.DHashMap.Internal.RawLemmas   instructions                   4.7%     (1296.9 σ)
- Std.Data.DHashMap.Internal.RawLemmas   task-clock                     5.0%       (34.1 σ)
- Std.Data.Internal.List.Associative     branches                       5.1%      (598.3 σ)
- Std.Data.Internal.List.Associative     instructions                   5.1%      (503.7 σ)
- big_do                                 branches                     175.8%    (10083.7 σ)
- big_do                                 instructions                 160.5%     (8193.4 σ)
- big_omega.lean                         branches                       2.6%     (1398.5 σ)
- big_omega.lean                         instructions                   1.6%      (574.0 σ)
- big_omega.lean MT                      branches                       2.6%      (240.1 σ)
- big_omega.lean MT                      instructions                   1.7%      (216.4 σ)
- bv_decide_inequality.lean              branches                       5.3%      (421.0 σ)
- bv_decide_inequality.lean              instructions                   4.0%      (284.5 σ)
+ bv_decide_large_aig.lean               branches                      -5.4%     (-102.7 σ)
+ bv_decide_large_aig.lean               instructions                  -4.8%      (-86.6 σ)
+ bv_decide_mod                          maxrss                        -1.1%      (-21.0 σ)
- bv_decide_mul                          branches                       8.1%      (613.9 σ)
- bv_decide_mul                          instructions                   6.8%      (780.7 σ)
+ bv_decide_mul                          maxrss                        -2.5%      (-23.7 σ)
- bv_decide_realworld                    branches                       6.2%       (86.1 σ)
- bv_decide_realworld                    instructions                   4.9%       (67.0 σ)
- deriv                                  instructions                   5.8%     (4666.5 σ)
- identifier auto-completion             branches                       2.6%       (84.8 σ)
- identifier auto-completion             instructions                   2.3%       (62.9 σ)
+ identifier auto-completion             maxrss                        -3.9%      (-22.7 σ)
- ilean roundtrip                        branches                       5.7%      (438.9 σ)
- ilean roundtrip                        instructions                   5.3%      (497.5 σ)
+ import Lean                            branches                     -17.9%    (-1724.8 σ)
+ import Lean                            instructions                 -18.1%    (-1586.6 σ)
+ import Lean                            maxrss                       -15.4%     (-561.0 σ)
+ import Lean                            task-clock                   -19.1%      (-91.7 σ)
+ import Lean                            wall-clock                   -19.0%      (-84.5 σ)
+ lake build clean                       instructions                  -5.9%      (-96.4 σ)
+ lake build clean                       task-clock                    -8.1%     (-150.9 σ)
+ lake build no-op                       wall-clock                    -6.6%      (-22.5 σ)
+ lake config elab                       instructions                  -3.4%     (-205.4 σ)
+ lake config elab                       maxrss                       -12.3%     (-260.0 σ)
+ lake config import                     instructions                 -15.5%    (-1117.6 σ)
+ lake config import                     maxrss                       -13.5%     (-387.4 σ)
+ lake config tree                       instructions                 -17.1%    (-1734.3 σ)
+ lake config tree                       maxrss                       -13.5%     (-365.0 σ)
+ lake env                               instructions                 -15.2%     (-516.2 σ)
+ lake env                               maxrss                       -13.5%     (-383.3 σ)
- lake startup                           instructions                   1.2%       (21.9 σ)
+ language server startup                branches                      -7.4%     (-177.8 σ)
+ language server startup                instructions                  -8.8%     (-179.8 σ)
+ language server startup                maxrss                        -6.3%     (-214.1 σ)
+ liasolver                              instructions                  -2.9%    (-2038.4 σ)
+ libleanshared.so                       binary size                  -14.1%
- omega_stress.lean async                branches                       1.8%      (134.7 σ)
- omega_stress.lean async                instructions                   1.5%       (94.6 σ)
- parser                                 instructions                   3.8%      (950.5 σ)
- rbmap                                  instructions                 210.9%    (23125.6 σ)
+ rbmap_1                                instructions                 -13.8%   (-14868.5 σ)
- rbmap_10                               instructions                 144.7%    (29030.0 σ)
- rbmap_library                          instructions                 199.2%    (27553.8 σ)
- rbmap_library                          task-clock                   202.8%       (21.0 σ)
- rbmap_library                          wall-clock                   202.2%       (21.0 σ)
+ reduceMatch                            instructions                  -3.1%      (-39.2 σ)
+ simp_arith1                            branches                      -5.7%     (-169.0 σ)
+ simp_arith1                            instructions                  -6.9%     (-181.5 σ)
+ simp_arith1                            maxrss                       -13.4%     (-101.8 σ)
+ stdlib                                 blocked (unaccounted)        -12.2%     (-112.8 σ)
+ stdlib                                 grind dsimp                  -28.3%      (-47.7 σ)
+ stdlib                                 instructions                  -3.6%    (-1404.6 σ)
+ stdlib                                 maxrss                       -15.0%     (-260.4 σ)
- stdlib                                 number of imported bytes       2.1%
+ stdlib                                 number of imported consts    -54.9%
- stdlib                                 number of imported entries    21.6%
- stdlib size                            bytes .olean                   4.9%
+ stdlib size                            lines C                      -20.1%
+ stdlib size                            max dynamic symbols          -13.1%
- tests/bench/ interpreted               instructions                   2.2%     (1017.7 σ)
+ tests/bench/ interpreted               maxrss                       -13.4%     (-115.3 σ)
+ tests/compiler                         sum binary sizes             -10.3%
+ unionfind                              instructions                  -1.7%     (-364.5 σ)
+ workspaceSymbols                       instructions                 -81.2% (-4395347.8 σ)
+ workspaceSymbols                       maxrss                       -15.7%      (-97.8 σ)
+ workspaceSymbols                       task-clock                   -78.8%    (-2071.8 σ)
+ workspaceSymbols                       wall-clock                   -78.8%    (-1879.7 σ)

tobiasgrosser · 2025-06-17T20:13:07Z

It seems the last PR rebase has broken the release CI for this PR. Not sure what the issue is, but merging master has fixed it for me. Not sure this warrants a deep investigation, but I would appreciate a rebase to see if this unbreaks our experimental uses of the new codegen.

zwarich · 2025-06-17T20:16:51Z

It seems the last PR rebase has broken the release CI for this PR. Not sure what the issue is, but merging master has fixed it for me. Not sure this warrants a deep investigation, but I would appreciate a rebase to see if this unbreaks our experimental uses of the new codegen.

I was going to rebase again to see what effect some perf fixes I made have on the bench results, so I'll do that now. There's one more blocking issue for Mathlib (introduced by a new use of Batteries' open private in Mathlib), which I'll hopefully fix soon. After that, there are no true blockers, but I am going to see whether I can easily fix the pessimism in the RC reuse optimizations caused by the new compiler's increased use of join points.

zwarich · 2025-06-17T21:22:19Z

!bench

zwarich · 2025-06-17T22:05:11Z

!bench

zwarich · 2025-06-17T22:05:46Z

(testing some minor inlining changes)

leanprover-bot · 2025-06-17T22:32:05Z

Here are the benchmark results for commit d733277.
There were significant changes against commit 3b2990b:

  Benchmark                              Metric                       Change
  ========================================================================================
- Init size                              bytes .olean                   6.6%
- Init.Data.BitVec.Lemmas                branches                       4.6%     (455.1 σ)
- Init.Data.BitVec.Lemmas                instructions                   4.2%     (362.5 σ)
- Init.Data.BitVec.Lemmas re-elab        branch-misses                  1.3%      (41.6 σ)
- Init.Data.BitVec.Lemmas re-elab        branches                       4.3%      (63.5 σ)
- Init.Data.BitVec.Lemmas re-elab        instructions                   4.1%      (60.9 σ)
- Init.Data.List.Sublist async           branches                       4.7%     (127.0 σ)
- Init.Data.List.Sublist async           instructions                   4.7%     (118.9 σ)
- Init.Data.List.Sublist re-elab -j4     branches                       4.5%      (65.9 σ)
- Init.Data.List.Sublist re-elab -j4     instructions                   4.5%      (69.0 σ)
- Init.Data.List.Sublist re-elab -j4     task-clock                     1.8%      (34.7 σ)
- Init.Prelude async                     branches                       7.9%     (398.6 σ)
- Init.Prelude async                     instructions                   6.0%     (315.6 σ)
- Std.Data.DHashMap.Internal.RawLemmas   branches                       4.8%     (552.3 σ)
- Std.Data.DHashMap.Internal.RawLemmas   instructions                   4.6%     (470.6 σ)
- Std.Data.Internal.List.Associative     branches                       5.0%     (894.9 σ)
- Std.Data.Internal.List.Associative     instructions                   5.0%     (770.5 σ)
- big_do                                 branches                     175.5%    (6456.2 σ)
- big_do                                 instructions                 160.1%    (5143.9 σ)
- big_omega.lean                         branches                       2.6%     (166.6 σ)
- big_omega.lean                         instructions                   1.6%     (181.9 σ)
- big_omega.lean MT                      branches                       2.6%     (224.0 σ)
- big_omega.lean MT                      instructions                   1.7%     (200.3 σ)
- bv_decide_inequality.lean              branches                       5.2%      (51.9 σ)
- bv_decide_inequality.lean              instructions                   4.3%      (51.0 σ)
+ bv_decide_large_aig.lean               branches                      -5.4%    (-187.1 σ)
+ bv_decide_large_aig.lean               instructions                  -4.6%    (-165.7 σ)
- bv_decide_mod                          branches                       5.4%     (336.0 σ)
- bv_decide_mod                          instructions                   4.7%     (236.6 σ)
- bv_decide_mul                          branches                       7.9%     (580.5 σ)
- bv_decide_mul                          instructions                   7.2%     (749.6 σ)
- bv_decide_realworld                    branches                       5.8%     (238.1 σ)
- bv_decide_realworld                    instructions                   4.9%     (220.4 σ)
- deriv                                  instructions                   5.9%    (9233.2 σ)
- identifier auto-completion             branches                       1.8%      (67.3 σ)
- identifier auto-completion             instructions                   2.0%      (59.3 σ)
+ identifier auto-completion             maxrss                        -3.7%     (-33.4 σ)
- ilean roundtrip                        branches                       4.1%     (261.4 σ)
- ilean roundtrip                        instructions                   4.8%     (348.3 σ)
+ import Lean                            branches                     -17.4%    (-883.4 σ)
+ import Lean                            instructions                 -17.4%    (-761.6 σ)
+ import Lean                            maxrss                       -15.4%   (-1218.9 σ)
+ lake build clean                       instructions                  -5.1%    (-133.4 σ)
+ lake build clean                       maxrss                       -10.1%     (-32.8 σ)
+ lake build clean                       task-clock                    -7.3%     (-95.4 σ)
+ lake build clean                       wall-clock                    -6.3%     (-99.0 σ)
+ lake config elab                       instructions                  -3.5%    (-351.8 σ)
+ lake config elab                       maxrss                       -12.2%    (-295.3 σ)
+ lake config import                     instructions                 -15.3%    (-625.4 σ)
+ lake config import                     maxrss                       -13.3%    (-206.0 σ)
+ lake config tree                       instructions                 -16.9%    (-614.7 σ)
+ lake config tree                       maxrss                       -13.3%    (-266.0 σ)
+ lake env                               instructions                 -15.1%    (-923.1 σ)
+ lake env                               maxrss                       -13.3%    (-295.3 σ)
- lake startup                           instructions                   1.5%      (85.4 σ)
+ language server startup                branches                      -7.2%    (-248.6 σ)
+ language server startup                instructions                  -8.4%    (-256.8 σ)
+ language server startup                maxrss                        -6.3%     (-22.0 σ)
+ liasolver                              instructions                  -3.0%    (-419.0 σ)
+ libleanshared.so                       binary size                  -13.3%
- omega_stress.lean async                branches                       1.8%      (46.9 σ)
- omega_stress.lean async                instructions                   1.6%      (40.2 σ)
- parser                                 instructions                   3.3%    (1539.5 σ)
+ qsort                                  instructions                  -1.0%    (-331.4 σ)
- rbmap                                  instructions                 210.9%   (29016.0 σ)
+ rbmap_1                                instructions                 -13.8%    (-171.3 σ)
- rbmap_10                               instructions                 144.7%   (76220.4 σ)
- rbmap_library                          instructions                 199.6%   (33843.1 σ)
+ reduceMatch                            instructions                  -3.0%     (-94.3 σ)
+ simp_arith1                            branches                      -5.6%     (-55.9 σ)
+ simp_arith1                            instructions                  -6.8%     (-55.5 σ)
+ simp_arith1                            maxrss                       -13.7%     (-63.3 σ)
+ stdlib                                 grind canon                  -11.1%     (-91.2 σ)
- stdlib                                 grind simp                     5.4%      (57.4 σ)
+ stdlib                                 instructions                  -3.7%   (-5923.2 σ)
+ stdlib                                 maxrss                       -11.1%     (-33.1 σ)
- stdlib                                 number of imported bytes       2.2%
+ stdlib                                 number of imported consts    -55.3%
- stdlib                                 number of imported entries    21.5%
- stdlib                                 tactic execution               3.5%      (75.9 σ)
+ stdlib                                 task-clock                    -3.6%    (-129.8 σ)
+ stdlib                                 type checking                 -1.6%     (-20.3 σ)
- stdlib size                            bytes .olean                   5.5%
+ stdlib size                            lines C                      -18.9%
+ stdlib size                            max dynamic symbols          -12.8%
- tests/bench/ interpreted               instructions                   1.8%      (99.6 σ)
+ tests/bench/ interpreted               maxrss                       -13.4%    (-924.5 σ)
- tests/bench/ interpreted               task-clock                     7.0%     (121.0 σ)
+ tests/compiler                         sum binary sizes              -9.8%
+ unionfind                              instructions                  -2.6%    (-785.5 σ)
+ workspaceSymbols                       instructions                 -81.4% (-181653.9 σ)
+ workspaceSymbols                       maxrss                       -16.0%   (-1438.0 σ)
+ workspaceSymbols                       task-clock                   -80.1%    (-173.7 σ)
+ workspaceSymbols                       wall-clock                   -80.1%    (-172.6 σ)

zwarich · 2025-06-19T23:21:18Z

I was unable to push to the mathlib4 branch for this PR, so I made my own copy with the required changes: https://github.com/zwarich/mathlib4/tree/lean-pr-testing-8577

The longer name was chosen to avoid clashes with the old compiler.

This makes it easier to distinguish tests that are actually failing while we work on the new codegen.

* chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <[email protected]> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Kim Morrison <[email protected]> * Update lean-toolchain for testing leanprover/lean4#8577 * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8804 * Update lean-toolchain for testing leanprover/lean4#8699 * bump Qq and batteries * meta adaptations * bump aesop * fix * fix (adaptation note) * Update lean-toolchain for leanprover/lean4#8699 * shake * chore: bump to nightly-2025-06-19 * fix * Update lean-toolchain for leanprover/lean4#8699 * fix: correct memoFix's use of unsafe code * fix: adjust noncomputable annotations for new compiler * fix: replace use of `open private _ in` with `open private _ from` The implementation of `open private _ from` relies on specific internals of the old compiler and will no longer work. * remove mul_hmul * chore: adjust one maxHeartbeats for the new compiler * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 * Update lean-toolchain for testing leanprover/lean4#8914 * chore: bump to nightly-2025-06-21 * fix * fixes * fixes * fixes * updated lake manifest * comment out tests * chore: fix for nightly-testing (leanprover-community#26246) * fix * fix * fix grind typeclasses * chore: adaptations for nightly-2025-06-20 * lake update * Update lean-toolchain for leanprover/lean4#8914 * fix grind instance * chore: bump to nightly-2025-06-22 * chore: bump to nightly-2025-06-23 * chore: rm unused `Lean.Util.Paths` import & use updated batteries * Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist) * merge lean-pr-testing-8804 * Bump dependencies and silence linter. * Fixes (Now `elabSimpArgs` already handles `*`, so we can delete the associated code.) * lake update; disable unusedSimpArgs in Batteries * lkae update aesop * disable unusedSimpArgs in MathlibTest * fix grind instance priorities * comment out MathlibTest/zmod with adaptation note * touch for CI * chore: bump to nightly-2025-06-24 * Kick CI * Bump batteries * Guessing adaption for leanprover/lean4#8929 * chore: bump to nightly-2025-06-25 * fix: workflow merging master into nightly-testing * fix * chore: cache get uses tracking remote * touch for new CI * restart CI * chore: bump to nightly-2025-06-26 * Update lean-toolchain for testing leanprover/lean4#8928 * Teach Mathlib about `mrefine` * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8980 * chore: update linter warning test outputs * chore: remove excess line break in deprecation lint now that notes add their own line breaks * chore: more test cleanup * . * cleanup adaptation notes * fix * fix * chore: bump to nightly-2025-06-27 * Merge master into nightly-testing * Merge master into nightly-testing * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * fix tests * chore: bump to nightly-2025-06-28 * Merge master into nightly-testing * lintining * lint --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Cameron Zwarich <[email protected]> Co-authored-by: Mac Malone <[email protected]> Co-authored-by: Anne C.A. Baanen <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: Sebastian Graf <[email protected]> Co-authored-by: Joseph Rotella <[email protected]>

* cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Kim Morrison <[email protected]> * Update lean-toolchain for testing leanprover/lean4#8577 * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8804 * Update lean-toolchain for testing leanprover/lean4#8699 * bump Qq and batteries * meta adaptations * bump aesop * fix * fix (adaptation note) * Update lean-toolchain for leanprover/lean4#8699 * shake * chore: bump to nightly-2025-06-19 * fix * Update lean-toolchain for leanprover/lean4#8699 * fix: correct memoFix's use of unsafe code * fix: adjust noncomputable annotations for new compiler * fix: replace use of `open private _ in` with `open private _ from` The implementation of `open private _ from` relies on specific internals of the old compiler and will no longer work. * remove mul_hmul * chore: adjust one maxHeartbeats for the new compiler * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 * Update lean-toolchain for testing leanprover/lean4#8914 * chore: bump to nightly-2025-06-21 * fix * fixes * fixes * fixes * updated lake manifest * comment out tests * chore: fix for nightly-testing (leanprover-community#26246) * fix * fix * fix grind typeclasses * chore: adaptations for nightly-2025-06-20 * lake update * Update lean-toolchain for leanprover/lean4#8914 * fix grind instance * chore: bump to nightly-2025-06-22 * chore: bump to nightly-2025-06-23 * chore: rm unused `Lean.Util.Paths` import & use updated batteries * Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist) * merge lean-pr-testing-8804 * Bump dependencies and silence linter. * Fixes (Now `elabSimpArgs` already handles `*`, so we can delete the associated code.) * lake update; disable unusedSimpArgs in Batteries * lkae update aesop * disable unusedSimpArgs in MathlibTest * fix grind instance priorities * comment out MathlibTest/zmod with adaptation note * touch for CI * chore: bump to nightly-2025-06-24 * Kick CI * Bump batteries * Guessing adaption for leanprover/lean4#8929 * chore: bump to nightly-2025-06-25 * fix: workflow merging master into nightly-testing * fix * chore: cache get uses tracking remote * touch for new CI * restart CI * chore: bump to nightly-2025-06-26 * Update lean-toolchain for testing leanprover/lean4#8928 * Teach Mathlib about `mrefine` * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8980 * chore: update linter warning test outputs * chore: remove excess line break in deprecation lint now that notes add their own line breaks * chore: more test cleanup * . * cleanup adaptation notes * fix * fix * chore: bump to nightly-2025-06-27 * Merge master into nightly-testing * Merge master into nightly-testing * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * fix tests * chore: bump to nightly-2025-06-28 * Merge master into nightly-testing * lintining * Merge master into nightly-testing * unused simp args * chore: bump to nightly-2025-06-29 * chore: adaptations for nightly-2025-06-29 * Merge master into nightly-testing * chore: robustify `open Mathlib` benchmark * deprecations * Update lean-toolchain for testing leanprover/lean4#9086 * Merge master into nightly-testing * fixes * chore: bump to nightly-2025-06-30 * lake update * lake update * lake update * lake update * lake update * . --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Cameron Zwarich <[email protected]> Co-authored-by: Mac Malone <[email protected]> Co-authored-by: Anne C.A. Baanen <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: Sebastian Graf <[email protected]> Co-authored-by: Joseph Rotella <[email protected]>

@Kha

* fix * fixes * chore: adaptations for nightly-2025-06-16 (leanprover-community#25994) * chore: bump to nightly-2025-06-03 * fix * fix * Update lean-toolchain for testing leanprover/lean4#8610 * fix * revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <[email protected]> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: Jovan Gerbscheid <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: Mario Carneiro <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 (leanprover-community#26043) * revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <[email protected]> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 --------- Co-authored-by: Jovan Gerbscheid <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Mario Carneiro <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Rob23oba <[email protected]> * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Kim Morrison <[email protected]> * Update lean-toolchain for testing leanprover/lean4#8577 * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8804 * Update lean-toolchain for testing leanprover/lean4#8699 * bump Qq and batteries * meta adaptations * bump aesop * fix * fix (adaptation note) * Update lean-toolchain for leanprover/lean4#8699 * shake * chore: adaptations for nightly-2025-06-18 (leanprover-community#26077) * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <[email protected]> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Kim Morrison <[email protected]> * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: Jovan Gerbscheid <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Mario Carneiro <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> * chore: bump to nightly-2025-06-19 * feat: add algebra shims for Grind.Nat/IntModule (leanprover-community#26133) This PR adds shims so `grind` will understand Mathlib's `AddCommMonoid` and `AddCommGroup`. (Subsequent shims will connect up the order structures for modules and rings.) * fix * Update lean-toolchain for leanprover/lean4#8699 * fix: correct memoFix's use of unsafe code * fix: adjust noncomputable annotations for new compiler * fix: replace use of `open private _ in` with `open private _ from` The implementation of `open private _ from` relies on specific internals of the old compiler and will no longer work. * remove mul_hmul * chore: adjust one maxHeartbeats for the new compiler * linter * feat: generalize grind algebra shims (leanprover-community#26131) This PR extends the shims converting from Mathlib to `Lean.Grind` typeclasses, now that `grind` knows about (non-commutative)-(semi)-rings. * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 (leanprover-community#26209) * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <[email protected]> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Kim Morrison <[email protected]> * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * chore: bump to nightly-2025-06-19 * fix * remove mul_hmul * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Mario Carneiro <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> * Update lean-toolchain for testing leanprover/lean4#8914 * chore: bump to nightly-2025-06-21 * fix * fixes * fixes * fixes * updated lake manifest * comment out tests * chore: fix for nightly-testing (leanprover-community#26246) * fix * fix * fix grind typeclasses * chore: adaptations for nightly-2025-06-20 * lake update * Update lean-toolchain for leanprover/lean4#8914 * fix grind instance * chore: bump to nightly-2025-06-22 * chore: bump to nightly-2025-06-23 * chore: rm unused `Lean.Util.Paths` import & use updated batteries * Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist) * merge lean-pr-testing-8804 * Bump dependencies and silence linter. * Fixes (Now `elabSimpArgs` already handles `*`, so we can delete the associated code.) * lake update; disable unusedSimpArgs in Batteries * lkae update aesop * disable unusedSimpArgs in MathlibTest * fix grind instance priorities * comment out MathlibTest/zmod with adaptation note * touch for CI * chore: bump to nightly-2025-06-24 * Kick CI * Bump batteries * Guessing adaption for leanprover/lean4#8929 * chore: bump to nightly-2025-06-25 * fix: workflow merging master into nightly-testing * fix * chore: cache get uses tracking remote * touch for new CI * restart CI * chore: bump to nightly-2025-06-26 * Update lean-toolchain for testing leanprover/lean4#8928 * Teach Mathlib about `mrefine` * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8980 * chore: update linter warning test outputs * chore: remove excess line break in deprecation lint now that notes add their own line breaks * chore: more test cleanup * . * cleanup adaptation notes * fix * fix * chore: bump to nightly-2025-06-27 * chore: adaptations for nightly-2025-06-26 (#2) * Merge master into nightly-testing * Merge master into nightly-testing * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * chore: adaptations for nightly-2025-06-27 (#3) * fix tests * chore: bump to nightly-2025-06-28 * Merge master into nightly-testing * lintining * Merge master into nightly-testing * unused simp args * chore: bump to nightly-2025-06-29 * chore: adaptations for nightly-2025-06-29 * chore: adaptations for nightly-2025-06-28 (#5) * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <[email protected]> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Kim Morrison <[email protected]> * Update lean-toolchain for testing leanprover/lean4#8577 * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8804 * Update lean-toolchain for testing leanprover/lean4#8699 * bump Qq and batteries * meta adaptations * bump aesop * fix * fix (adaptation note) * Update lean-toolchain for leanprover/lean4#8699 * shake * chore: bump to nightly-2025-06-19 * fix * Update lean-toolchain for leanprover/lean4#8699 * fix: correct memoFix's use of unsafe code * fix: adjust noncomputable annotations for new compiler * fix: replace use of `open private _ in` with `open private _ from` The implementation of `open private _ from` relies on specific internals of the old compiler and will no longer work. * remove mul_hmul * chore: adjust one maxHeartbeats for the new compiler * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 * Update lean-toolchain for testing leanprover/lean4#8914 * chore: bump to nightly-2025-06-21 * fix * fixes * fixes * fixes * updated lake manifest * comment out tests * chore: fix for nightly-testing (leanprover-community#26246) * fix * fix * fix grind typeclasses * chore: adaptations for nightly-2025-06-20 * lake update * Update lean-toolchain for leanprover/lean4#8914 * fix grind instance * chore: bump to nightly-2025-06-22 * chore: bump to nightly-2025-06-23 * chore: rm unused `Lean.Util.Paths` import & use updated batteries * Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist) * merge lean-pr-testing-8804 * Bump dependencies and silence linter. * Fixes (Now `elabSimpArgs` already handles `*`, so we can delete the associated code.) * lake update; disable unusedSimpArgs in Batteries * lkae update aesop * disable unusedSimpArgs in MathlibTest * fix grind instance priorities * comment out MathlibTest/zmod with adaptation note * touch for CI * chore: bump to nightly-2025-06-24 * Kick CI * Bump batteries * Guessing adaption for leanprover/lean4#8929 * chore: bump to nightly-2025-06-25 * fix: workflow merging master into nightly-testing * fix * chore: cache get uses tracking remote * touch for new CI * restart CI * chore: bump to nightly-2025-06-26 * Update lean-toolchain for testing leanprover/lean4#8928 * Teach Mathlib about `mrefine` * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8980 * chore: update linter warning test outputs * chore: remove excess line break in deprecation lint now that notes add their own line breaks * chore: more test cleanup * . * cleanup adaptation notes * fix * fix * chore: bump to nightly-2025-06-27 * Merge master into nightly-testing * Merge master into nightly-testing * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * fix tests * chore: bump to nightly-2025-06-28 * Merge master into nightly-testing * lintining * lint --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Cameron Zwarich <[email protected]> Co-authored-by: Mac Malone <[email protected]> Co-authored-by: Anne C.A. Baanen <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: Sebastian Graf <[email protected]> Co-authored-by: Joseph Rotella <[email protected]> * Merge master into nightly-testing * chore: robustify `open Mathlib` benchmark * deprecations * Update lean-toolchain for testing leanprover/lean4#9086 * Merge master into nightly-testing * fixes * chore: bump to nightly-2025-06-30 * lake update * lake update * lake update * lake update * lake update * . * Merge master into nightly-testing * Merge master into nightly-testing * Merge master into nightly-testing * Merge master into nightly-testing * cleanup * unusedSimpArgs * bump toolchain * lake update * Merge master into nightly-testing * Merge master into nightly-testing * chore: adaptations for nightly-2025-07-01 * add adaptation note * add adaptation note * chore: bump to nightly-2025-07-02 * fixes * Merge master into nightly-testing * fixes * update test output * Merge master into nightly-testing * Merge master into nightly-testing * chore: bump to nightly-2025-07-03 * chore: adaptations for nightly-2025-07-03 --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: github-actions <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: Jovan Gerbscheid <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: Mario Carneiro <[email protected]> Co-authored-by: sgouezel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Christian Merten <[email protected]> Co-authored-by: Kenny Lau <[email protected]> Co-authored-by: Fabrizio Barroero <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Cameron Zwarich <[email protected]> Co-authored-by: Mac Malone <[email protected]> Co-authored-by: Anne C.A. Baanen <[email protected]> Co-authored-by: Sebastian Graf <[email protected]> Co-authored-by: Joseph Rotella <[email protected]>

zwarich requested a review from leodemoura as a code owner June 1, 2025 19:50

zwarich added the changelog-compiler Compiler, runtime, and FFI label Jun 1, 2025

zwarich marked this pull request as draft June 1, 2025 19:51

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jun 1, 2025

zwarich force-pushed the new_codegen_mathlib branch 2 times, most recently from 70cf3e5 to 52cfb7c Compare June 1, 2025 20:51

zwarich added the force-mathlib-ci label Jun 1, 2025

tobiasgrosser mentioned this pull request Jun 2, 2025

use Lean's new code generator rems-project/sail#1329

Merged

zwarich removed the force-mathlib-ci label Jun 11, 2025

zwarich force-pushed the new_codegen_mathlib branch from 52cfb7c to 5ec19d8 Compare June 14, 2025 15:00

zwarich force-pushed the new_codegen_mathlib branch 2 times, most recently from 30bf42a to 820593b Compare June 15, 2025 21:31

zwarich force-pushed the new_codegen_mathlib branch from 820593b to 656e8e1 Compare June 17, 2025 20:58

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 17, 2025

Update lean-toolchain for testing leanprover/lean4#8577

ebc5b6e

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 17, 2025

Update lean-toolchain for testing leanprover/lean4#8577

7a4bf74

leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jun 17, 2025

zwarich closed this Jun 17, 2025

zwarich reopened this Jun 17, 2025

zwarich force-pushed the new_codegen_mathlib branch 2 times, most recently from 656e8e1 to abfcb61 Compare June 19, 2025 22:11

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 19, 2025

Update lean-toolchain for leanprover/lean4#8577

ac36960

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 19, 2025

Update lean-toolchain for leanprover/lean4#8577

e535f02

zwarich marked this pull request as ready for review June 19, 2025 23:20

zwarich added release-ci Enable all CI checks for a PR, like is done for releases merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. and removed release-ci Enable all CI checks for a PR, like is done for releases labels Jun 19, 2025

zwarich force-pushed the new_codegen_mathlib branch from abfcb61 to f888317 Compare June 20, 2025 13:18

zwarich changed the title ~~feat: enable the new compiler by default~~ feat: enable the new compiler Jun 20, 2025

zwarich added 7 commits June 20, 2025 06:47

feat: enable the new compiler

e43c524

chore: rename closed term suffix from _closedTerm to _closed

fa5a371

The longer name was chosen to avoid clashes with the old compiler.

chore: update expected test outputs

c8f8ff8

This makes it easier to distinguish tests that are actually failing while we work on the new codegen.

chore: reenable subset of new-compiler tests and delete others

c4bf5f7

chore: add an extra test case to lean/run/noncomp.lean

2a4111f

chore: add new tests for noncomputable

b6674b2

chore: update stage0

1a80f32

zwarich force-pushed the new_codegen_mathlib branch from f888317 to 1a80f32 Compare June 20, 2025 13:50

zwarich added release-ci Enable all CI checks for a PR, like is done for releases and removed merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. labels Jun 20, 2025

nomeata merged commit 26b7e49 into leanprover:master Jun 20, 2025
24 of 30 checks passed

feat: enable the new compiler #8577

feat: enable the new compiler #8577

Uh oh!

Conversation

zwarich commented Jun 1, 2025

Uh oh!

zwarich commented Jun 1, 2025

Uh oh!

leanprover-community-bot commented Jun 1, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Jun 1, 2025

Uh oh!

zwarich commented Jun 1, 2025

Uh oh!

zwarich commented Jun 14, 2025

Uh oh!

zwarich commented Jun 14, 2025

Uh oh!

leanprover-bot commented Jun 14, 2025

Uh oh!

zwarich commented Jun 14, 2025

Uh oh!

zwarich commented Jun 15, 2025

Uh oh!

zwarich commented Jun 15, 2025

Uh oh!

leanprover-bot commented Jun 15, 2025

Uh oh!

tobiasgrosser commented Jun 17, 2025

Uh oh!

zwarich commented Jun 17, 2025

Uh oh!

zwarich commented Jun 17, 2025

Uh oh!

zwarich commented Jun 17, 2025

Uh oh!

zwarich commented Jun 17, 2025

Uh oh!

leanprover-bot commented Jun 17, 2025

Uh oh!

zwarich commented Jun 19, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

leanprover-community-bot commented Jun 1, 2025 •

edited

Loading