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: harden markPersistent uses #6257

Merged
merged 2 commits into from
Nov 29, 2024
Merged

Conversation

Kha
Copy link
Member

@Kha Kha commented Nov 29, 2024

This API may or may not have been a footgun, better to be safe than sorry

@Kha Kha enabled auto-merge November 29, 2024 13:01
@Kha Kha added the release-ci Enable all CI checks for a PR, like is done for releases label Nov 29, 2024
@Kha Kha disabled auto-merge November 29, 2024 13:02
@Kha
Copy link
Member Author

Kha commented Nov 29, 2024

!bench

@leanprover-bot
Copy link
Collaborator

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

@Kha Kha force-pushed the push-nvprzvksukzs branch from 832f568 to 3cd5f18 Compare November 29, 2024 13:18
@Kha
Copy link
Member Author

Kha commented Nov 29, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 3cd5f18.
There were significant changes against commit 5f1ff42:

  Benchmark                  Metric                    Change
  =====================================================================
- big_do                     branches                    1.8%  (71.9 σ)
- big_do                     instructions                1.7%  (72.6 σ)
+ big_omega.lean             branch-misses              -3.9% (-14.8 σ)
- big_omega.lean             branches                    1.6%  (39.0 σ)
- big_omega.lean             instructions                1.4%  (48.7 σ)
+ bv_decide_mul              branch-misses              -2.2% (-10.6 σ)
- lake env                   task-clock                  7.7%  (30.6 σ)
- lake env                   wall-clock                  7.6%  (37.8 σ)
- parser                     task-clock                  5.2%  (35.1 σ)
- parser                     wall-clock                  5.2%  (35.6 σ)
- stdlib                     attribute application       2.6%  (18.5 σ)
- stdlib                     instructions                1.2% (512.5 σ)
- stdlib                     process pre-definitions     2.3%  (10.7 σ)
- tests/bench/ interpreted   instructions                1.9% (883.4 σ)
- tests/bench/ interpreted   task-clock                 30.2%  (26.3 σ)
- tests/bench/ interpreted   wall-clock                 13.3%  (22.8 σ)

@Kha Kha added this pull request to the merge queue Nov 29, 2024
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 29, 2024
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5f1ff42a15eec6fb7696435f86bae82500bd3de5 --onto 6d495586a1836da3e12efb4fbf9946bd9088ac5f. (2024-11-29 14:36:10)

Merged via the queue into leanprover:master with commit 86f3037 Nov 29, 2024
22 checks passed
@Kha Kha deleted the push-nvprzvksukzs branch November 29, 2024 15:10
@Kha Kha restored the push-nvprzvksukzs branch November 29, 2024 15:11
@Kha Kha deleted the push-nvprzvksukzs branch November 29, 2024 15:11
@kim-em kim-em added the changelog-compiler Compiler, runtime, and FFI label Jan 4, 2025
JovanGerb pushed a commit to JovanGerb/lean4 that referenced this pull request Jan 21, 2025
This API may or may not have been a footgun, better to be safe than
`sorry`
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
changelog-compiler Compiler, runtime, and FFI release-ci Enable all CI checks for a PR, like is done for releases 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