experiment: replace tauto with grind

kim-em · kim-em · commit 8e6693ed0f1a · 2025-10-17T10:37:24.000+11:00
diff --git a/lakefile.lean b/lakefile.lean
@@ -30,6 +30,7 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[
   ⟨`linter.allScriptsDocumented, true⟩,
   ⟨`linter.pythonStyle, true⟩,
   ⟨`linter.style.longFile, .ofNat 1500⟩,
+  ⟨`linter.tacticAnalysis.tautoToGrind, 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
`@@ -30,6 +30,7 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[`
`30`	`30`	⟨`linter.allScriptsDocumented, true⟩,
`31`	`31`	⟨`linter.pythonStyle, true⟩,
`32`	`32`	⟨`linter.style.longFile, .ofNat 1500⟩,
	`33`	+ ⟨`linter.tacticAnalysis.tautoToGrind, true⟩,
`33`	`34`	-- ⟨`linter.nightlyRegressionSet, true⟩,
`34`	`35`	-- `latest_import.yml` uses this comment: if you edit it, make sure that the workflow still works
`35`	`36`	`]`