chore: bump Lean to v4.9.0 #119
Conversation
Smt/Reconstruct/Real/Polynorm.lean
Outdated
| @@ -5,7 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. | |||
| Authors: Abdalrhman Mohamed | |||
| -/ | |||
|
|
|||
| import Mathlib.Data.Real.Basic | |||
| import Mathlib.Data.Real.Star | |||
There was a problem hiding this comment.
This change is needed as Real.Basic as per 4.8.0 has been split up to Real.Basic and Real.Star as per 4.9.0. Reverting this results in the following error when tests are run:
Test/linarith.lean:146:2: error: [arithPolyNorm]: could not prove x - y = -x + y
There was a problem hiding this comment.
Is the error above the only one caused by the version change? If so, then let's keep import Mathlib.Data.Real.Basic. This error message is an instance of a bigger issue that will be resolved with once cvc5/#10911 is merged.
There was a problem hiding this comment.
Yep, this is the only failing test case caused by the version change. As per your suggestion, I have in dff5fb8 reverted import Mathlib.Data.Real.Star to import Mathlib.Data.Real.Basic, and updated the aforementioned test case to account for that error.
Also, thank you for mentioning the related cvc5 issue. I found this test case breakage to be rather puzzling, and suspected that there may be something deeper going on here.
There was a problem hiding this comment.
Hi @joewatt95! Thanks for the PR! It looks good to me. I left just one minor comment.
Smt/Reconstruct/Real/Polynorm.lean
Outdated
| @@ -5,7 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. | |||
| Authors: Abdalrhman Mohamed | |||
| -/ | |||
|
|
|||
| import Mathlib.Data.Real.Basic | |||
| import Mathlib.Data.Real.Star | |||
There was a problem hiding this comment.
Is the error above the only one caused by the version change? If so, then let's keep import Mathlib.Data.Real.Basic. This error message is an instance of a bigger issue that will be resolved with once cvc5/#10911 is merged.
* bump Lean to v4.9.0 * Fix compilation of Smt.Real * Fix expected outputs of most test cases * import Real.Star instead of Real.Basic * Revert import Real.Star -> Real.Basic, update test case to reflect failure
This bumps Lean and Mathlib to the latest (as of 2024-7-6) stable version.