lean4
lean4 copied to clipboard
refactor: migrate all usages of old slice notation
This PR replaces all usages of [:] slice notation in src with the new [...] notation.
Mathlib CI status (docs):
- ❗ Batteries CI can not be attempted yet, as the
nightly-testing-2025-06-24tag does not exist there yet. We will retry when you push more commits. If you rebase your branch ontonightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using theforce-mathlib-cilabel. (2025-06-25 19:07:07) - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the
nightly-with-mathlibbranch. Trygit rebase 40d2c9946319716228b414e501e71b7f959e1619 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force Mathlib CI using theforce-mathlib-cilabel. (2025-06-26 12:03:49) - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the
nightly-with-mathlibbranch. Trygit rebase b1a306cf696ead9724e9d3879885d4e119800fe6 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force Mathlib CI using theforce-mathlib-cilabel. (2025-06-26 21:50:45) - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the
nightly-with-mathlibbranch. Trygit rebase fe1b40703131756bb6af786f4c2c131a09bf0a01 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force Mathlib CI using theforce-mathlib-cilabel. (2025-06-27 12:55:43)
!bench
Here are the benchmark results for commit 4783d35d3fba6eda1fddb2d8906b9d25ccdcb0b1.Found no runs to compare against.
!bench
Here are the benchmark results for commit 551b19ac5b24349df8eff1b7f2fb5ac48e8f78c4.Found no runs to compare against.
!bench
Here are the benchmark results for commit 34634b63282b3595990f89bee60528061f7128e7.Found no runs to compare against.
!bench
Here are the benchmark results for commit de7ce99557a83f349510fc5b98f8716ee04206d3. There were significant changes against commit b1a306cf696ead9724e9d3879885d4e119800fe6:
Benchmark Metric Change
=========================================================================
+ bv_decide_large_aig.lean task-clock -11.1% (-115.8 σ)
+ bv_decide_large_aig.lean wall-clock -11.0% (-87.3 σ)
+ qsort task-clock -8.9% (-20.5 σ)
+ qsort wall-clock -8.8% (-21.1 σ)
+ stdlib grind canon -2.1% (-27.7 σ)
- stdlib instructions 2.8% (2336.1 σ)
- stdlib number of imported bytes 4.7%
- stdlib number of imported consts 3.3%
- stdlib number of imported entries 2.3%
- stdlib task-clock 3.3% (22.6 σ)
- tests/bench/ interpreted wall-clock 2.6% (73.6 σ)
!bench
Here are the benchmark results for commit de7ce99557a83f349510fc5b98f8716ee04206d3. There were significant changes against commit b1a306cf696ead9724e9d3879885d4e119800fe6:
Benchmark Metric Change
=========================================================================
+ bv_decide_large_aig.lean task-clock -11.1% (-115.8 σ)
+ bv_decide_large_aig.lean wall-clock -11.0% (-87.3 σ)
+ qsort task-clock -8.9% (-20.5 σ)
+ qsort wall-clock -8.8% (-21.1 σ)
+ stdlib grind canon -2.1% (-27.7 σ)
- stdlib instructions 2.8% (2336.1 σ)
- stdlib number of imported bytes 4.7%
- stdlib number of imported consts 3.3%
- stdlib number of imported entries 2.3%
- stdlib task-clock 3.3% (22.6 σ)
- tests/bench/ interpreted wall-clock 2.6% (73.6 σ)
!bench
!bench
Here are the benchmark results for commit 4a707ff756edf06a7686c71c6a031a87d0904344. The entire run failed. Found no significant differences.
Here are the benchmark results for commit 7423776a3b3808d4c1dcfbe7dbf2f9c5f5eb9fc9. There were significant changes against commit b1a306cf696ead9724e9d3879885d4e119800fe6:
Benchmark Metric Change
=============================================================
- channel.lean bounded0_spsc 3.8% (26.5 σ)
+ stdlib grind canon -2.9% (-20.8 σ)
- stdlib instructions 2.7% (1343.7 σ)
- stdlib number of imported bytes 5.0%
- stdlib number of imported consts 3.5%
- stdlib number of imported entries 2.4%
- stdlib tactic execution 7.1% (54.3 σ)
!bench
Here are the benchmark results for commit 3c07c1b752ce17f300f12d5678a6f40df0bf6ea5. There were significant changes against commit b1a306cf696ead9724e9d3879885d4e119800fe6:
Benchmark Metric Change
=========================================================
+ bv_decide_inequality.lean task-clock -4.0% (-22.6 σ)
+ bv_decide_inequality.lean wall-clock -4.0% (-40.9 σ)
!bench
Here are the benchmark results for commit aa82327492b46daeaa148065cda1f1b33963cfd7. There were significant changes against commit fe1b40703131756bb6af786f4c2c131a09bf0a01:
Benchmark Metric Change
=========================================
+ stdlib task-clock -1.3% (-39.2 σ)