Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: switch to Std.HashMap and Std.HashSet almost everywhere #4917

Merged
merged 5 commits into from
Aug 7, 2024

Conversation

TwoFX
Copy link
Member

@TwoFX TwoFX commented Aug 5, 2024

This removes every use except for ShareCommon which I will do as a follow-up.

This is very likely to break some users of the Lean API downstream.

@github-actions github-actions bot added changes-stage0 Contains stage0 changes, merge manually using rebase toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Aug 5, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Aug 5, 2024

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-08-05 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. (2024-08-05 14:30:53)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 14d59b3599d0b4fbfaf147e7ede2d82cbad7a1e7 --onto 647a5e94925791f6a16b629b6c16ffad60a7f478. (2024-08-06 08:29:38)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a29bca7f0074457679bc1709d384abdbc25ba103 --onto 647a5e94925791f6a16b629b6c16ffad60a7f478. (2024-08-07 15:14:34)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 240ebff549a2cf557f9abe9568f5de885f13e50d --onto 647a5e94925791f6a16b629b6c16ffad60a7f478. (2024-08-07 16:02:02)

@TwoFX TwoFX force-pushed the switch-to-std-hashmap branch from d2dced7 to d2d92a7 Compare August 6, 2024 08:12
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 6, 2024 08:24 Inactive
@TwoFX
Copy link
Member Author

TwoFX commented Aug 6, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit d2d92a7.
There were significant changes against commit 14d59b3:

  Benchmark                  Metric                    Change
  ======================================================================
+ import Lean                branches                   -3.7% (-145.9 σ)
+ import Lean                instructions               -4.1% (-137.2 σ)
- import Lean                maxrss                      3.4%  (127.2 σ)
+ lake build clean           instructions               -1.7%  (-34.7 σ)
- lake build no-op           maxrss                      2.7%  (162.4 σ)
+ lake config elab           instructions               -1.2%  (-56.9 σ)
- lake config elab           maxrss                      3.7%  (158.6 σ)
+ lake config import         instructions               -3.1%  (-62.0 σ)
- lake config import         maxrss                      4.0%  (246.6 σ)
+ lake config tree           instructions               -2.9%  (-68.3 σ)
- lake config tree           maxrss                      4.0%  (218.8 σ)
+ lake env                   instructions               -3.0%  (-67.0 σ)
- lake env                   maxrss                      4.0%  (233.9 σ)
- language server startup    maxrss                      5.4%  (359.5 σ)
- libleanshared.so           binary size                 1.2%
- reduceMatch                maxrss                      3.0%  (516.7 σ)
- stdlib                     instructions                1.5%  (672.0 σ)
- stdlib                     maxrss                      3.2%  (156.4 σ)
+ stdlib                     process pre-definitions    -1.3%  (-17.1 σ)
+ stdlib                     type checking              -2.0%  (-18.3 σ)
- stdlib                     wall-clock                 15.9%   (33.6 σ)
- stdlib size                bytes .olean                1.9%
- stdlib size                lines C                     1.9%
+ stdlib size                max dynamic symbols        -1.1%
- tests/bench/ interpreted   maxrss                      2.9%  (449.2 σ)
- tests/compiler             sum binary sizes            1.0%
- workspaceSymbols           maxrss                      3.2%  (388.5 σ)

@TwoFX TwoFX force-pushed the switch-to-std-hashmap branch from 78f6d2a to d55c416 Compare August 7, 2024 08:35
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 7, 2024 08:47 Inactive
@TwoFX
Copy link
Member Author

TwoFX commented Aug 7, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit d55c416.
There were significant changes against commit 14d59b3:

  Benchmark                  Metric                Change
  ==================================================================
+ import Lean                branches               -3.7%  (-63.1 σ)
+ import Lean                instructions           -4.2%  (-73.5 σ)
- import Lean                maxrss                  3.4%  (342.4 σ)
+ lake build clean           instructions           -1.8%  (-23.0 σ)
- lake build no-op           maxrss                  2.8%  (117.9 σ)
+ lake config elab           instructions           -1.2%  (-66.6 σ)
- lake config elab           maxrss                  3.8%  (180.4 σ)
+ lake config import         instructions           -3.0%  (-63.9 σ)
- lake config import         maxrss                  4.1%  (268.8 σ)
+ lake config tree           instructions           -2.8%  (-64.1 σ)
- lake config tree           maxrss                  4.1%  (394.5 σ)
+ lake env                   instructions           -2.9%  (-57.2 σ)
- lake env                   maxrss                  4.1%  (210.4 σ)
- language server startup    maxrss                  5.6%  (319.3 σ)
- libleanshared.so           binary size             1.2%
- reduceMatch                maxrss                  3.0%  (430.6 σ)
- stdlib                     instructions            1.5% (2116.5 σ)
- stdlib                     maxrss                  3.2% (1230.5 σ)
- stdlib                     task-clock              1.1%   (10.2 σ)
+ stdlib                     type checking          -2.2%  (-11.4 σ)
- stdlib                     wall-clock             14.9%   (71.8 σ)
- stdlib size                bytes .olean            1.9%
- stdlib size                lines C                 1.9%
+ stdlib size                max dynamic symbols    -1.1%
- tests/bench/ interpreted   maxrss                  2.8%  (436.4 σ)
- tests/compiler             sum binary sizes        1.0%
- workspaceSymbols           maxrss                  3.2%  (457.5 σ)

@TwoFX TwoFX force-pushed the switch-to-std-hashmap branch from d55c416 to d1caec0 Compare August 7, 2024 10:31
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 7, 2024 10:41 Inactive
@TwoFX
Copy link
Member Author

TwoFX commented Aug 7, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit d1caec0.
There were significant changes against commit 14d59b3:

  Benchmark                  Metric                Change
  ==================================================================
+ import Lean                branches               -4.5% (-153.6 σ)
+ import Lean                instructions           -4.9% (-151.2 σ)
- import Lean                maxrss                  2.1%   (52.9 σ)
+ lake build clean           instructions           -1.7%  (-13.4 σ)
- lake build no-op           maxrss                  1.2%   (47.0 σ)
+ lake config elab           instructions           -1.6% (-110.2 σ)
- lake config elab           maxrss                  1.6%   (81.2 σ)
+ lake config import         instructions           -4.2% (-114.4 σ)
- lake config import         maxrss                  1.7%  (101.3 σ)
+ lake config tree           instructions           -4.1% (-123.5 σ)
- lake config tree           maxrss                  1.7%   (93.9 σ)
+ lake env                   instructions           -4.2% (-103.3 σ)
- lake env                   maxrss                  1.7%   (59.8 σ)
- language server startup    maxrss                  2.1%  (135.3 σ)
- libleanshared.so           binary size             1.2%
- reduceMatch                maxrss                  1.8%  (248.0 σ)
- stdlib                     instructions            1.3%  (323.1 σ)
- stdlib                     maxrss                  2.0% (3885.6 σ)
- stdlib                     tactic execution        1.5%   (48.6 σ)
- stdlib                     wall-clock              4.6%   (20.5 σ)
- stdlib size                bytes .olean            1.9%
- stdlib size                lines C                 1.9%
+ stdlib size                max dynamic symbols    -1.1%
- tests/bench/ interpreted   maxrss                  1.8%  (161.1 σ)
- tests/compiler             sum binary sizes        1.0%
- workspaceSymbols           maxrss                  2.0%  (265.9 σ)

github-merge-queue bot pushed a commit that referenced this pull request Aug 7, 2024
#4917 will expose users of the `Lean` API to the renaming of the hash
map query methods. This PR aims to make the transition easier by adding
deprecated functions with the old names.
@TwoFX TwoFX force-pushed the switch-to-std-hashmap branch from d1caec0 to fb3090e Compare August 7, 2024 14:31
@TwoFX TwoFX marked this pull request as ready for review August 7, 2024 14:32
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 7, 2024 14:42 Inactive
@TwoFX TwoFX force-pushed the switch-to-std-hashmap branch from fb3090e to 5e052c0 Compare August 7, 2024 14:59
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 7, 2024 15:02 Inactive
@TwoFX TwoFX force-pushed the switch-to-std-hashmap branch from 5e052c0 to 56bf907 Compare August 7, 2024 15:46
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 7, 2024 15:58 Inactive
@Kha Kha merged commit 63c4de5 into master Aug 7, 2024
13 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
changes-stage0 Contains stage0 changes, merge manually using rebase toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants