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` |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||