mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
ff9c35d6ef
This PR implements the `#grind_lint` command, a diagnostic tool for analyzing the behavior of theorems annotated for theorem instantiation. The command helps identify problematic theorems that produce excessive or unbounded instance generation during E-matching, which can lead to performance issues. The main entry point is: ``` #grind_lint check ``` which analyzes all theorems marked with the `@[grind]` attribute. For each theorem, it creates an artificial goal and runs `grind`, collecting statistics about the number of instances produced. Results are summarized using info messages, and detailed breakdowns are shown for lemmas exceeding a configurable threshold. Additional subcommands are provided for targeted inspection and control: * `#grind_lint inspect thm`: analyzes one or more specific theorems in detail * `#grind_lint mute thm`: excludes a theorem from instantiation during analysis * `#grind_lint skip thm`: omits a theorem from being analyzed by `#grind_lint check`