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

perf: use C23's free_sized when available #6598

Open
wants to merge 3 commits into
base: master
Choose a base branch
from

Conversation

eric-wieser
Copy link
Contributor

See https://www.open-std.org/jtc1/sc22/wg14/www/docs/n2699.htm for an explanation of this feature.

This only has an effect on systems with a default allocator where `free_sized` is faster than `free`.

See https://www.open-std.org/jtc1/sc22/wg14/www/docs/n2699.htm for an explanation of this feature.

Co-authored-by: Eric Wieser <[email protected]>
@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 Jan 10, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jan 10, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2c9641f621f8aecf69d8644d5b7f99c96cb947fa --onto d2c4471cfa4611977bf4927b5cd849df1a4272b7. (2025-01-10 14:40:18)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2c9641f621f8aecf69d8644d5b7f99c96cb947fa --onto e3fd954318fb23038455e27a193cd63d8dad432d. (2025-01-17 16:04:38)

@Kha
Copy link
Member

Kha commented Jan 14, 2025

@eric-wieser Are you not using the small allocator?

@eric-wieser
Copy link
Contributor Author

eric-wieser commented Jan 14, 2025

Our hope was that https://github.com/google/tcmalloc might be just as good for our use case, but this would only be the case if tcmalloc actually gets access to the same size information that the small allocator has (through free_sized)!

@Kha
Copy link
Member

Kha commented Jan 14, 2025

@eric-wieser Thanks for the explanation. I assume you tested it successfully with a compiler supporting it :) ?

@eric-wieser
Copy link
Contributor Author

@Kha: yes, I tested this patch applied to lean v4.14.0 and it happy builds mathlib.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
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