lean4
lean4 copied to clipboard
leanprover
chore: fix (PersistentHashMap.insert k v).size
Fixes #3029, in which (PersistentHashMap.insert k v).size is wrong if the key already exists.
I think this fix ensures linearity correctly, but I would welcome learning if I've made a mistake!
- ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-09 23:55:17)
- ✅ Mathlib branch lean-pr-testing-3046 has successfully built against this PR. (2023-12-12 00:59:24) View Log
- ❗ Mathlib CI can not be attempted yet, as the
nightly-testing-2024-04-23tag does not exist there yet. We will retry when you push more commits. If you rebase your branch ontonightly-with-mathlib, Mathlib CI should run now. (2024-04-23 10:49:26)
Here are the benchmark results for commit bd9f2a2bc4e3d978ab307cc3755c04429d159dc7. There were significant changes against commit 1b2bbe717d1260e337e0cddabef10a6a7e8ff098:
Benchmark Metric Change
============================================================
- binarytrees instructions 3.8% (4764.1 σ)
+ binarytrees maxrss -6.7% (-102.2 σ)
- binarytrees.st instructions 3.6% (2879.6 σ)
- const_fold instructions 18.3% (1516.3 σ)
- const_fold task-clock 29.0% (11.5 σ)
- const_fold wall-clock 29.1% (11.5 σ)
- deriv instructions 11.3% (682.0 σ)
- deriv task-clock 25.9% (19.5 σ)
- deriv wall-clock 26.0% (19.6 σ)
- import Lean branch-misses 637.7% (642.5 σ)
- import Lean branches 34.4% (853.7 σ)
- import Lean instructions 24.8% (787.3 σ)
- lake build clean instructions 24.1% (77.1 σ)
- lake build clean task-clock 18.5% (30.6 σ)
- lake build clean wall-clock 64.7% (24.6 σ)
+ lake build no-op maxrss -8.1% (-163.5 σ)
- lake build no-op task-clock 43.0% (27.4 σ)
- lake config elab instructions 6.1% (525.0 σ)
- lake config import instructions 24.0% (447.3 σ)
- lake config tree instructions 23.4% (416.9 σ)
- lake env instructions 24.2% (641.2 σ)
- lake startup instructions 29.9% (292.7 σ)
- liasolver instructions 2.0% (235.5 σ)
+ libleanshared.so binary size -1.5%
- parser instructions 1.6% (1258.0 σ)
- qsort instructions 1.2% (1080.1 σ)
- rbmap instructions 2.5% (478.2 σ)
- rbmap_1 instructions 22.5% (3103.8 σ)
- rbmap_1 task-clock 48.5% (26.9 σ)
- rbmap_1 wall-clock 48.5% (26.9 σ)
- rbmap_10 instructions 8.2% (1382.2 σ)
- rbmap_10 task-clock 22.7% (18.8 σ)
- rbmap_10 wall-clock 22.8% (18.9 σ)
- rbmap_fbip instructions 6.2% (2282.6 σ)
- rbmap_library instructions 5.6% (1167.1 σ)
- reduceMatch instructions 2.5% (947.5 σ)
- stdlib instructions 4.3% (2959.2 σ)
- stdlib task-clock 7.5% (37.8 σ)
+ stdlib type checking -2.4% (-14.6 σ)
- stdlib wall-clock 3.3% (11.0 σ)
- tests/bench/ interpreted task-clock 3.6% (15.6 σ)
- unionfind instructions 4.4% (5855.8 σ)
+ unionfind maxrss -2.2% (-15.8 σ)
There were some configuration changes on the speedcenter runner machine (new Spectre mitigations...?), please try benchmarking again after rebasing
Here are the benchmark results for commit 78c555c726fc84e20288f3369b1cadbe52f4ad40. There were significant changes against commit 1b2bbe717d1260e337e0cddabef10a6a7e8ff098:
Benchmark Metric Change
==============================================================
- binarytrees instructions 3.6% (3201.6 σ)
+ binarytrees maxrss -6.2% (-98.7 σ)
- binarytrees.st instructions 3.5% (3036.1 σ)
- const_fold instructions 12.5% (12.4 σ)
- deriv instructions 8.1% (313.0 σ)
- deriv task-clock 13.4% (10.9 σ)
- deriv wall-clock 13.4% (11.0 σ)
- import Lean branch-misses 22.5% (25.0 σ)
- import Lean branches 19.1% (321.4 σ)
- import Lean instructions 13.3% (284.1 σ)
- lake build clean instructions 14.9% (49.0 σ)
- lake build clean wall-clock 31.0% (10.7 σ)
+ lake build no-op maxrss -7.9% (-166.2 σ)
- lake build no-op task-clock 57.9% (15.8 σ)
+ lake build no-op wall-clock -17.5% (-14.2 σ)
- lake config elab instructions 3.8% (401.4 σ)
- lake config import instructions 14.3% (387.3 σ)
- lake config tree instructions 13.8% (340.5 σ)
- lake env instructions 14.4% (539.6 σ)
- lake startup instructions 24.1% (366.8 σ)
+ libleanshared.so binary size -4.2%
- parser instructions 1.5% (1042.8 σ)
- qsort instructions 1.2% (881.6 σ)
- rbmap instructions 1.6% (133.7 σ)
- rbmap_1 instructions 14.8% (251.8 σ)
- rbmap_1 task-clock 18.1% (11.2 σ)
- rbmap_1 wall-clock 18.1% (11.2 σ)
- rbmap_10 instructions 5.4% (248.9 σ)
- rbmap_fbip instructions 5.8% (1213.7 σ)
- rbmap_library instructions 4.4% (513.9 σ)
- reduceMatch instructions 1.7% (467.9 σ)
+ stdlib attribute application -3.6% (-135.9 σ)
- stdlib instructions 3.2% (4313.9 σ)
+ stdlib type checking -3.2% (-15.8 σ)
+ tests/compiler sum binary sizes -10.2%
- unionfind instructions 4.1% (3249.5 σ)
+ unionfind maxrss -1.4% (-14.1 σ)
@Kha, I've rebased, but it looks like the benchmark report is pretty much the same.
I don't know how significant the regressions here are.
If someone could look over these changes to try to identify a cause (nonlinearity?) that would be great.
I think the cause is most likely not linearity but the additional allocation involved in creating and using tuples. You may be able to fix this by using continuation passing style but I'm not sure.
Here are the benchmark results for commit 36bcc0336d9185cfcce8084de5a7a197efd9cb88. There were significant changes against commit 78200b309f63b30e855313a15e25391efcfe6974:
Benchmark Metric Change
===================================================
- lake config import instructions 1.2% (44.3 σ)
- lake config tree instructions 1.2% (42.2 σ)
- lake env instructions 1.1% (23.2 σ)
- lake startup instructions 1.7% (45.6 σ)
Here are the benchmark results for commit 5f3404ae535c812109b936f2e2144fb3b0e07879. There were significant changes against commit b2de43ed8841995eb36e38549cf50556277b1ace:
Benchmark Metric Change
===================================================
- import Lean branches 1.1% (18.8 σ)
- import Lean instructions 1.0% (21.0 σ)
- lake config import instructions 1.2% (31.3 σ)
- lake config tree instructions 1.2% (39.7 σ)
- lake env instructions 1.2% (25.3 σ)
- lake startup instructions 1.9% (65.6 σ)
If someone is interested in picking this up and seeing if the performance cost coming from the tuples can be avoided, please feel free to take over here.
Here are the benchmark results for commit 9a7a98d4b6be65da7ed6d521f7e3324f3dd8e2ec. There were significant changes against commit b2de43ed8841995eb36e38549cf50556277b1ace:
Benchmark Metric Change
===================================================================
- import Lean branches 3.2% (58.9 σ)
- import Lean instructions 3.8% (79.8 σ)
- lake build clean instructions 4.5% (25.5 σ)
- lake config elab instructions 2.7% (120.8 σ)
- lake config import instructions 4.6% (108.8 σ)
- lake config tree instructions 4.5% (116.5 σ)
- lake env instructions 4.5% (184.9 σ)
- lake startup instructions 7.5% (225.1 σ)
- language server startup branches 4.2% (12.0 σ)
- language server startup instructions 4.8% (13.8 σ)
+ stdlib attribute application -1.2% (-144.6 σ)
- stdlib instructions 1.9% (909.7 σ)
- stdlib task-clock 1.5% (11.0 σ)
Here are the benchmark results for commit 91441a4d608446c4f5fe4fa2cc97ec30bc57235f. There were significant changes against commit b2de43ed8841995eb36e38549cf50556277b1ace:
Benchmark Metric Change
==========================================================
- import Lean branches 4.0% (88.2 σ)
- import Lean instructions 4.0% (97.9 σ)
- lake build clean instructions 4.7% (27.8 σ)
- lake config elab instructions 2.4% (125.6 σ)
- lake config import instructions 4.8% (155.8 σ)
- lake config tree instructions 4.8% (155.2 σ)
- lake env instructions 4.7% (201.0 σ)
- lake startup instructions 8.0% (461.0 σ)
- language server startup branches 4.7% (18.1 σ)
- language server startup instructions 4.8% (18.3 σ)
- language server startup maxrss 1.2% (28.9 σ)
- libleanshared.so binary size 1.2%
- stdlib instructions 1.9% (330.8 σ)
- stdlib task-clock 1.9% (43.0 σ)
- stdlib wall-clock 2.6% (12.8 σ)
- workspaceSymbols instructions 1.7% (3367.6 σ)
Here are the benchmark results for commit 3fa93531e451c561f13b9a5af22ca1815ec50383. There were significant changes against commit b2de43ed8841995eb36e38549cf50556277b1ace:
Benchmark Metric Change
====================================================
- import Lean branches 1.0% (21.3 σ)
- import Lean instructions 1.0% (23.6 σ)
- lake config import instructions 1.2% (26.3 σ)
- lake config tree instructions 1.1% (47.7 σ)
- lake env instructions 1.2% (33.0 σ)
- lake startup instructions 1.7% (130.3 σ)
Here are the benchmark results for commit c12204144c034903a67d5e0e6e0805b577ad451e. There were significant changes against commit b2de43ed8841995eb36e38549cf50556277b1ace:
Benchmark Metric Change
=============================================================
- import Lean branches 1.7% (32.4 σ)
- import Lean instructions 1.5% (32.6 σ)
- lake build clean instructions 1.8% (12.5 σ)
- lake config import instructions 1.8% (48.8 σ)
- lake config tree instructions 1.7% (49.0 σ)
- lake env instructions 1.8% (42.2 σ)
- lake startup instructions 2.9% (33.6 σ)
+ stdlib attribute application -2.0% (-83.5 σ)