lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

refactor: migrate all usages of old slice notation

Open datokrat opened this issue 4 months ago • 7 comments
trafficstars

This PR replaces all usages of [:] slice notation in src with the new [...] notation.

datokrat avatar Jun 25 '25 17:06 datokrat

Mathlib CI status (docs):

  • ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-06-24 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-25 19:07:07)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 40d2c9946319716228b414e501e71b7f959e1619 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-26 12:03:49)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b1a306cf696ead9724e9d3879885d4e119800fe6 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-26 21:50:45)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase fe1b40703131756bb6af786f4c2c131a09bf0a01 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-27 12:55:43)

!bench

datokrat avatar Jun 25 '25 19:06 datokrat

Here are the benchmark results for commit 4783d35d3fba6eda1fddb2d8906b9d25ccdcb0b1.Found no runs to compare against.

leanprover-bot avatar Jun 25 '25 19:06 leanprover-bot

!bench

datokrat avatar Jun 25 '25 19:06 datokrat

Here are the benchmark results for commit 551b19ac5b24349df8eff1b7f2fb5ac48e8f78c4.Found no runs to compare against.

leanprover-bot avatar Jun 25 '25 20:06 leanprover-bot

!bench

datokrat avatar Jun 25 '25 20:06 datokrat

Here are the benchmark results for commit 34634b63282b3595990f89bee60528061f7128e7.Found no runs to compare against.

leanprover-bot avatar Jun 25 '25 21:06 leanprover-bot

!bench

datokrat avatar Jun 27 '25 07:06 datokrat

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 σ)

leanprover-bot avatar Jun 27 '25 07:06 leanprover-bot

!bench

datokrat avatar Jun 27 '25 08:06 datokrat

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 σ)

leanprover-bot avatar Jun 27 '25 08:06 leanprover-bot

!bench

datokrat avatar Jun 27 '25 08:06 datokrat

!bench

datokrat avatar Jun 27 '25 09:06 datokrat

Here are the benchmark results for commit 4a707ff756edf06a7686c71c6a031a87d0904344. The entire run failed. Found no significant differences.

leanprover-bot avatar Jun 27 '25 09:06 leanprover-bot

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 σ)

leanprover-bot avatar Jun 27 '25 09:06 leanprover-bot

!bench

datokrat avatar Jun 27 '25 10:06 datokrat

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 σ)

leanprover-bot avatar Jun 27 '25 10:06 leanprover-bot

!bench

datokrat avatar Jun 27 '25 12:06 datokrat

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 σ)

leanprover-bot avatar Jun 27 '25 13:06 leanprover-bot