Commit 2025-12-05 09:09 1843876c

feat(TacticAnalysis): add generic env var-based tryAtEachStep linter (#32416)

Summary

Adds a generic tryAtEachStepFromEnv tactic analysis linter that reads the tactic to try from environment variables. This allows hammer-bench and similar tools to test arbitrary tactics without requiring Mathlib code changes.

• TRY_AT_EACH_STEP_TACTIC: The tactic syntax to try (e.g., "grind +suggestions")
• TRY_AT_EACH_STEP_LABEL: Human-readable label for output (optional) Uses captureException with tacticSeq.fn to parse tactic strings, following Kenny Lau's suggestion from Zulip. This enables support for tactic sequences like "simp; grind". Also removes the unnecessary Mathlib.Init import from ParseCommand.lean to avoid import cycles. 🤖 Prepared with Claude Code