Skip to content

fix: avoid destroying reuse potential in LCNF simp#12388

Draft
hargoniX wants to merge 7 commits intomasterfrom
hbv/simp_cases_weaker
Draft

fix: avoid destroying reuse potential in LCNF simp#12388
hargoniX wants to merge 7 commits intomasterfrom
hbv/simp_cases_weaker

Conversation

@hargoniX
Copy link
Copy Markdown
Contributor

@hargoniX hargoniX commented Feb 9, 2026

  • fix: LCNF casesOnCtor can only act if type correct
  • fix: this PR makes LCNF simp more tame to not destroy reuse information

@hargoniX
Copy link
Copy Markdown
Contributor Author

hargoniX commented Feb 9, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Feb 9, 2026 •
edited
Loading

Benchmark results for d476a31 against 5ba467d are in! @hargoniX

  • 🟥 build//instructions: +7.1G (+0.06%)

Large changes (1✅, 2🟥)

  • ✅ big_do//instructions: -137.7M (-0.53%)
  • 🟥 iterators (compiled)//instructions: +44.6M (+9.14%)
  • 🟥 iterators (interpreted)//instructions: +80.8M (+0.23%)

Medium changes (1🟥)

  • 🟥 build/module/Lean.Meta.Tactic.FunInd//instructions: +1.2G (+1.54%)

Small changes (1✅, 27🟥)

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

@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 Feb 9, 2026
@hargoniX
Copy link
Copy Markdown
Contributor Author

hargoniX commented Feb 9, 2026

!bench

@hargoniX hargoniX force-pushed the hbv/simp_cases_weaker branch from d476a31 to 1c00ced Compare February 9, 2026 12:17
@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Feb 9, 2026 •
edited
Loading

Benchmark results for 1c00ced against 5ba467d are in! @hargoniX

  • 🟥 build//instructions: +2.4G (+0.02%)

Large changes (1✅)

  • ✅ big_do//instructions: -133.5M (-0.52%)

Medium changes (1🟥)

  • 🟥 build/module/Lean.Meta.Tactic.FunInd//instructions: +1.2G (+1.49%)

Small changes (1✅, 23🟥)

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

@hargoniX
Copy link
Copy Markdown
Contributor Author

hargoniX commented Feb 9, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Feb 9, 2026 •
edited
Loading

Benchmark results for 1e87a54 against 5ba467d are in! @hargoniX

  • 🟥 build//instructions: +94.6G (+0.74%)

Large changes (2✅, 7🟥)

  • ✅ big_do//instructions: -140.1M (-0.54%)
  • ✅ deriv//instructions: -45.7M (-0.61%)
  • 🟥 identifier auto-completion//instructions: +9.6G (+13.02%)
  • 🟥 ilean roundtrip//instructions: +4.7G (+17.68%)
  • 🟥 lake build no-op//instructions: +551.5M (+8.82%)
  • 🟥 language server startup with ileans//instructions: +5.7G (+22.58%)
  • 🟥 parser//instructions: +1.4G (+3.44%)
  • 🟥 riscv-ast.lean//instructions: +5.5G (+5.32%)
  • 🟥 size/all/.olean.private//bytes: +9MiB (+0.84%)

Medium changes (24🟥)

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

Small changes (8✅, 1877🟥)

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

@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing Bot commented Feb 9, 2026

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5ba467d920da2d093676024cbca38a5525abd517 --onto 39c26fce1da321b24eaf949d0d7d028ba589e4e1. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-09 14:20:58)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Feb 9, 2026

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5ba467d920da2d093676024cbca38a5525abd517 --onto 75d7f7eb227bc54dc6ea3d8ead090ee4180debaf. You can force reference manual CI using the force-manual-ci label. (2026-02-09 14:21:01)

hargoniX and others added 6 commits February 9, 2026 15:53
@hargoniX
fin
d71bfce
@TwoFX @hargoniX
feat: LawfulForwardPatternModel for string patterns (#12360)
ffa17dc 
This PR provides a `LawfulForwardPatternModel` instance for string
patterns, i.e., it proves correctness of the `dropPrefix?` and
`startsWith` functions for string patterns.

Note that this is "just" the correctness proof; there isn't a way to
actually use it yet. API lemmas will follow.
@hargoniX
fix: LCNF casesOnCtor can only act if type correct
d7f77d5
@hargoniX
tweak tweak tweak
be7255d
@hargoniX
fix: this PR makes LCNF simp more tame to not destroy reuse information
9efded8
@hargoniX
let's see
8311242
@hargoniX hargoniX force-pushed the hbv/simp_cases_weaker branch from 1e87a54 to 8311242 Compare February 9, 2026 16:00
@hargoniX
Copy link
Copy Markdown
Contributor Author

hargoniX commented Feb 9, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Feb 9, 2026 •
edited
Loading

Benchmark results for 8311242 against d2c738c are in! @hargoniX

  • 🟥 build//instructions: +101.0G (+0.79%)

Large changes (2✅, 7🟥)

  • ✅ big_do//instructions: -140.8M (-0.54%)
  • ✅ deriv//instructions: -45.7M (-0.61%)
  • 🟥 identifier auto-completion//instructions: +9.6G (+13.07%)
  • 🟥 ilean roundtrip//instructions: +4.6G (+17.67%)
  • 🟥 lake build no-op//instructions: +565.4M (+9.05%)
  • 🟥 language server startup with ileans//instructions: +5.7G (+22.67%)
  • 🟥 parser//instructions: +1.4G (+3.44%)
  • 🟥 riscv-ast.lean//instructions: +5.3G (+5.11%)
  • 🟥 size/all/.olean.private//bytes: +10MiB (+0.90%)

Medium changes (3✅, 28🟥)

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

Small changes (16✅, 1925🟥)

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

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 will be requested when the pull request is marked ready for review kim-em is a code owner

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura will be requested when the pull request is marked ready for review leodemoura is a code owner

Assignees

No one assigned

Labels

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.

4 participants

@hargoniX @leanprover-radar @leanprover-bot @TwoFX