Commit 2025-10-22 14:25 2521caa7

View on Github →

chore: revert #30740 and #30748 (#30788) cf. #mathlib4 > Build error in Tactic file @ 💬

Estimated changes

Modified .github/workflows/nightly-docgen.yml

Modified Cache/IO.lean

modified def Cache.IO.rootHashGeneration

Modified Cache/Requests.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/StrictPositivity.lean

Modified Mathlib/Algebra/BigOperators/Group/List/Basic.lean

Modified Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean

Modified Mathlib/Algebra/Notation/Defs.lean

added theorem SMul.smul_eq_hSMul

Modified Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean

Modified Mathlib/Algebra/Polynomial/RuleOfSigns.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

Modified Mathlib/Computability/DFA.lean

Modified Mathlib/Computability/RegularExpressions.lean

Modified Mathlib/Control/Monad/Cont.lean

Modified Mathlib/Data/Finsupp/Notation.lean

Modified Mathlib/Data/Fintype/EquivFin.lean

Modified Mathlib/Data/Int/LeastGreatest.lean

Modified Mathlib/Data/List/Chain.lean

Modified Mathlib/Data/List/Flatten.lean

Modified Mathlib/Data/List/SplitOn.lean

Modified Mathlib/Data/Nat/Digits/Defs.lean

modified theorem Nat.repr_length

Modified Mathlib/Data/Set/Insert.lean

Modified Mathlib/Data/String/Basic.lean

added theorem List.asString_inj

added theorem List.length_asString

modified theorem List.toList_asString

modified theorem String.asString_toList

added theorem String.endPos_empty

added theorem String.length_data

deleted theorem String.ltb_cons_addChar'

modified theorem String.ltb_cons_addChar

modified theorem String.toList_inj

Modified Mathlib/Data/String/Defs.lean

Modified Mathlib/Data/String/Lemmas.lean

modified theorem String.congr_append

Deleted Mathlib/Lean/Elab/InfoTree.lean

deleted def Lean.Elab.collectTryThisSuggestions

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean

Modified Mathlib/SetTheory/PGame/Basic.lean

Modified Mathlib/Tactic/Basic.lean

deleted structure Mathlib.Tactic.withResetServerInfo.Result

deleted def Mathlib.Tactic.withResetServerInfo

Modified Mathlib/Tactic/DeclarationNames.lean

modified def Mathlib.Linter.getNamesFrom

Modified Mathlib/Tactic/Hint.lean

modified def Mathlib.Tactic.Hint.suggestion

added def Mathlib.Tactic.Hint.withMessageLog

added def Mathlib.Tactic.Hint.withoutInfoTrees

Modified Mathlib/Tactic/Linter/CommandRanges.lean

Modified Mathlib/Tactic/Linter/CommandStart.lean

modified def Mathlib.Linter.CommandStart.endPos

Modified Mathlib/Tactic/Linter/DocString.lean

Modified Mathlib/Tactic/Linter/FindDeprecations.lean

modified def Mathlib.Tactic.getPosAfterImports

modified def Mathlib.Tactic.parseLine

Modified Mathlib/Tactic/Linter/HashCommandLinter.lean

Modified Mathlib/Tactic/Linter/Header.lean

modified def Mathlib.Linter.authorsLineChecks

modified def Mathlib.Linter.parseUpToHere

modified def Mathlib.Linter.toSyntax

Modified Mathlib/Tactic/Linter/PPRoundtrip.lean

Modified Mathlib/Tactic/Linter/TextBased.lean

Modified Mathlib/Tactic/Linter/UpstreamableDecl.lean

Modified Mathlib/Tactic/Says.lean

added def Mathlib.Tactic.Says.evalTacticCapturingInfo

added def Mathlib.Tactic.Says.evalTacticCapturingMessages

Modified Mathlib/Tactic/SuccessIfFailWithMsg.lean

Modified Mathlib/Tactic/ToAdditive/Frontend.lean

Modified Mathlib/Tactic/ToAdditive/GuessName.lean

Modified Mathlib/Tactic/ToExpr.lean

Modified Mathlib/Tactic/Widget/Calc.lean

Modified Mathlib/Tactic/Widget/CongrM.lean

Modified Mathlib/Tactic/Widget/Conv.lean

Modified Mathlib/Tactic/Widget/GCongr.lean

Modified Mathlib/Tactic/Widget/InteractiveUnfold.lean

Modified Mathlib/Tactic/Widget/LibraryRewrite.lean

Modified Mathlib/Tactic/Widget/SelectPanelUtils.lean

Modified Mathlib/Util/CompileInductive.lean

Modified Mathlib/Util/Superscript.lean

Modified MathlibTest/CalcQuestionMark.lean

Modified MathlibTest/Change.lean

Modified MathlibTest/DeprecateTo.lean

Modified MathlibTest/FieldSimp.lean

Modified MathlibTest/FindSyntax.lean

Modified MathlibTest/LibraryRewrite.lean

Modified MathlibTest/LibrarySearch/basic.lean

Modified MathlibTest/LibrarySearch/mathlib.lean

Modified MathlibTest/LibrarySearch/observe.lean

Modified MathlibTest/Subsingleton.lean

Modified MathlibTest/Use.lean

Modified MathlibTest/Util/PrintSorries.lean

Modified MathlibTest/Variable.lean

Modified MathlibTest/fast_instance.lean

Modified MathlibTest/hint.lean

Modified MathlibTest/propose.lean

Modified MathlibTest/rewrites.lean

Modified MathlibTest/ring.lean

Modified MathlibTest/says.lean

Modified MathlibTest/says_whitespace.lean

Modified MathlibTest/success_if_fail_with_msg.lean

Modified MathlibTest/toAdditive.lean

Modified lake-manifest.json

Modified lakefile.lean

Modified lean-toolchain

Modified scripts/check-yaml.lean

Modified scripts/noshake.json