Skip to content

fix: make String.toList semireducible - #14294

Merged
datokrat merged 1 commit into
leanprover:masterfrom
datokrat:paul/string-tolist-semireducible
Jul 15, 2026
Merged

fix: make String.toList semireducible#14294
datokrat merged 1 commit into
leanprover:masterfrom
datokrat:paul/string-tolist-semireducible

Conversation

@datokrat

@datokrat datokrat commented Jul 6, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

This PR makes String.toList semireducible because unfolding it throws the definitional equality checker deep into the weeds of its internal implementation.

@datokrat

datokrat commented Jul 6, 2026

Copy link
Copy Markdown
Contributor Author

!radar

@leanprover-radar

leanprover-radar commented Jul 6, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 1b8e97b against 1db9c0d are in. No significant results found. @datokrat

  • 🟥 build//instructions: +1.1G (+0.01%)

Small changes (1✅, 3🟥)

  • ✅ build/module/Init.Data.String.Lemmas.Pattern.Split.Char//instructions: -47.3M (-2.63%)
  • 🟥 interpreted/iterators//task-clock: +107ms (+7.80%)
  • 🟥 interpreted/iterators//wall-clock: +108ms (+8.20%)
  • 🟥 lake/inundation/env//maxrss: +3MiB (+0.31%)

@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 Jul 6, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Jul 6, 2026 •
edited
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-07-06 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. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-06 14:08:52)
  • ✅ Mathlib branch lean-pr-testing-14294 has successfully built against this PR. (2026-07-10 14:00:06) View Log

@leanprover-bot

leanprover-bot commented Jul 6, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-07-06 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-07-06 14:08:53)
  • ✅ Reference manual branch lean-pr-testing-14294 has successfully built against this PR. (2026-07-10 13:01:37) View Log
  • 🟡 Reference manual branch lean-pr-testing-14294 build against this PR didn't complete normally. (2026-07-10 13:04:13) View Log

@datokrat
datokrat force-pushed the paul/string-tolist-semireducible branch from 1b8e97b to 4f70696 Compare July 8, 2026 07:28
@datokrat
datokrat force-pushed the paul/string-tolist-semireducible branch from 4f70696 to 8087b28 Compare July 10, 2026 12:27
@datokrat datokrat changed the title String.toList semireducible fix: String.toList semireducible Jul 10, 2026
@datokrat datokrat added the changelog-no Do not include this PR in the release changelog label Jul 10, 2026
@datokrat datokrat changed the title fix: String.toList semireducible fix: make String.toList semireducible Jul 10, 2026
@github-actions github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Jul 10, 2026
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Jul 10, 2026
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Jul 10, 2026
@datokrat
datokrat marked this pull request as ready for review July 15, 2026 13:28
@datokrat
datokrat requested a review from kim-em as a code owner July 15, 2026 13:28
@datokrat datokrat added changelog-library Library and removed changelog-no Do not include this PR in the release changelog labels Jul 15, 2026
@datokrat
datokrat added this pull request to the merge queue Jul 15, 2026
Merged via the queue into leanprover:master with commit d3b9c57 Jul 15, 2026
56 of 58 checks passed
robsimmons pushed a commit that referenced this pull request Jul 29, 2026
@datokrat @robsimmons
fix: make String.toList semireducible (#14294)
097b803 
This PR makes `String.toList` semireducible because unfolding it throws
the definitional equality checker deep into the weeds of its internal
implementation.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

No one assigned

Labels

builds-manual CI has verified that the Lean Language Reference builds against this PR builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@datokrat @leanprover-radar @leanprover-bot