1643fd7532
This PR ensures that solver propagation steps are necessary in the generated tactic script to close the goal. It produces more compact proof scripts, but this is not just an optimization, if we include an unnecessary step, we may fail to replay the generated script when `cases` steps are pruned using non-chronological backtracking (NCB). For example, when executing `finish?`, we may have performed a `cases #<anchor>` step that enabled `ring` to propagate a new fact. If this fact is not used in the final proof, and the corresponding `cases #<anchor>` step is pruned by NCB, the `ring` step will fail during replay. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||