Skip to content

perf: optimize String.compare#13796

Merged
hargoniX merged 1 commit into
masterfrom
hbv/compare_step2
May 20, 2026
Merged

perf: optimize String.compare#13796
hargoniX merged 1 commit into
masterfrom
hbv/compare_step2

Conversation

@hargoniX
Copy link
Copy Markdown
Contributor

@hargoniX hargoniX commented May 20, 2026

This PR optimizes String.compare to turn it into 1 instead of 2 memcmp calls.

@hargoniX hargoniX requested a review from kim-em as a code owner May 20, 2026 12:39
@hargoniX
Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented May 20, 2026

Benchmark results for 9bbe198 against 34df732 are in. There are significant results. @hargoniX

  • build//instructions: -20.1G (-0.18%)

Large changes (1✅)

  • compiled/ilean_roundtrip//instructions: -624.9M (-2.68%)

Medium changes (2✅)

  • compiled/watchdogRss//instructions: -288.1M (-1.14%)
  • interpreted/identifier_completion//instructions: -941.1M (-1.41%)

Small changes (26✅)

Too many entries to display here. View the full report on radar instead.

@hargoniX hargoniX added the changelog-compiler Compiler, runtime, and FFI label May 20, 2026
@hargoniX hargoniX added this pull request to the merge queue May 20, 2026
Merged via the queue into master with commit a3fff15 May 20, 2026
24 checks passed
@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 May 20, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 34df7320668250fa586c2bbb706637896581a3f9 --onto 43ef70db63e2c1c1720b84fd153125c96a00c5d2. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-20 13:33:22)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 34df7320668250fa586c2bbb706637896581a3f9 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-20 13:33:24)

@hargoniX hargoniX deleted the hbv/compare_step2 branch May 20, 2026 13:45
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 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.

3 participants