Commit 2024-09-29 03:27 d244ef26

View on Github →

fix: call checkSystem in linarith and ring (#16666) Without this change, linarith calls on large states can substantially overrun On the web editor, the test fails with

Tactic took much more than 750ms (1272ms)
Tactic took much more than 1000ms (1267ms)
Tactic took much more than 2250ms (2679ms)

Estimated changes

Modified Mathlib/Tactic/Linarith/Oracle/FourierMotzkin.lean

Modified Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Gauss.lean

modified def Linarith.SimplexAlgorithm.Gauss.getTableau

Modified Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/PositiveVector.lean

Modified Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/SimplexAlgorithm.lean

Modified Mathlib/Tactic/Linarith/Verification.lean

Modified Mathlib/Tactic/Ring/Basic.lean

modified def Mathlib.Tactic.Ring.evalMul

modified def Mathlib.Tactic.Ring.evalMul₁

modified def Mathlib.Tactic.Ring.evalNeg

modified def Mathlib.Tactic.Ring.evalNegProd

Created test/tactic_timeout.lean

added def Meta.tryCatchAll

added def Tactic.tryCatchAll

added def Tactic.withTimeout

added def Term.tryCatchAll

added theorem linear_combination_with_10_terms