fix: reduceNat? match terms with free or meta variables#3139
Merged
leodemoura merged 2 commits intomasterfrom Jan 5, 2024
Merged
fix: reduceNat? match terms with free or meta variables#3139leodemoura merged 2 commits intomasterfrom
leodemoura merged 2 commits intomasterfrom
Conversation
|
Member
|
@joehendrix Thanks for catching this issue. Could you please add new tests using |
3f83693 to
dd153ba
Compare
Contributor
Author
|
Yes, I validated on my machine, and reordered the commits too so hopefully the CI will report the first commit fails. |
Contributor
Author
|
Oh, I'm not sure if it ran the tests after all, but the commit shows a failure. If there's something else that needs to be done with this, let me know. |
Contributor
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit d0d3678. Benchmark Metric Change
=========================================
+ stdlib wall-clock -1.1% (-34.9 σ) |
leodemoura
approved these changes
Jan 5, 2024
Collaborator
|
Uh oh, this has caused a bunch of timeouts in Mathlib. I wish that we had tested Mathlib first before merging! (Per the bot's instructions above, this requires basing the Lean PR off |
joehendrix
added a commit
that referenced
this pull request
Jan 7, 2024
This removes checks in `Lean.Meta.reduceNat?` that caused it to fail on terms it could handle because they contain meta variables in arguments. This lead to those operations being reduced using their equational definitions and slow performance on large patterns: ``` set_option profiler true set_option profiler.threshold 1 def testMod (x:Nat) := match x with | 128 % 1024 => true | _ => false -- elaboration took 3.02ms def testMul (x:Nat) := match x with | 128 * 1 => true | _ => false -- type checking took 11.1ms -- compilation of testMul.match_1 took 313ms -- compilation of testMul took 65.7ms -- elaboration took 58.9ms ``` Performance is slower on `testMul` than `testMod` because `whnf` ends up evaluateing `128 * 1` using Peano arithmetic while `128 % 1024` is able to avoid that treatment since `128 < 1024`.
leodemoura
added a commit
that referenced
this pull request
Jan 7, 2024
mathlib-bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jan 8, 2024
This proof has been causing timeouts for both leanprover/lean4#3124 and leanprover/lean4#3139 (and its in-progress fixes), so I'm just fixing it pre-emptively here. (Fix due to @joehendrix.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Kha
pushed a commit
that referenced
this pull request
Jan 9, 2024
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This removes checks in
Lean.Meta.reduceNat?that caused it to fail on terms it could handle because they contain meta variables in arguments. This lead to those operations being reduced using their equational definitions and slow performance on large patterns:Performance is slower on
testMulthantestModbecausewhnfends up evaluateing128 * 1using Peano arithmetic while128 % 1024is able to avoid that treatment since128 < 1024.