experiment: which linarith can not be replaced with grind?

kim-em · kim-em · commit c6cdc43e1d7e · 2025-12-10T02:04:04.000Z
diff --git a/lakefile.lean b/lakefile.lean
@@ -34,6 +34,7 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[
   ⟨`linter.allScriptsDocumented, true⟩,
   ⟨`linter.pythonStyle, true⟩,
   ⟨`linter.style.longFile, .ofNat 1500⟩,
+  ⟨`linter.tacticAnalysis.regressions.linarithToGrind, true⟩,
   -- ⟨`linter.nightlyRegressionSet, true⟩,
   -- `latest_import.yml` uses this comment: if you edit it, make sure that the workflow still works
 ]

Original file line number	Diff line number	Diff line change
`@@ -34,6 +34,7 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[`
`34`	`34`	⟨`linter.allScriptsDocumented, true⟩,
`35`	`35`	⟨`linter.pythonStyle, true⟩,
`36`	`36`	⟨`linter.style.longFile, .ofNat 1500⟩,
	`37`	+ ⟨`linter.tacticAnalysis.regressions.linarithToGrind, true⟩,
`37`	`38`	-- ⟨`linter.nightlyRegressionSet, true⟩,
`38`	`39`	-- `latest_import.yml` uses this comment: if you edit it, make sure that the workflow still works
`39`	`40`	`]`