tryAtEachStep
tryAtEachStep is a tool that runs a tactic at every proof step in
a given Lean 4 file, reporting cases where the tactic closes the goal.
With a tactic like exact? and rw_search, this can help to
find ways in which your existing proofs can be improved.
howto
Add this to your lakefile.lean:
require tryAtEachStep from git "https://github.com/dwrensha/tryAtEachStep" @ "main"
Then do this:
$ lake exe tryAtEachStep exact? Foo/Bar.lean
Example findings:
- mathlib#13335
- mathlib#13334
- mathlib#12715
- mathlib#12678
- mathlib#11093
- mathlib@4900a2c5
- mathlib@866dfe56
- mathlib@a6f77074
- compfiles@cd250e72
- compfiles@9a9eb697
- compfiles@0a02194e
- compfiles@22eaf558
- compfiles@8ee4ce58
- compfiles@8fd2ff0a
- compfiles@fdf0f9a0
- compfiles@b8068381
- compfiles@f76ad21b
- compfiles@8650fb4a
- compfiles@fe99e1e9
- compfiles@6c3272cb
TODO
- Tests
- Run in parallel on all
.leanfiles in a project. - Support tactics that aren't imported by the input file.
- Better handling of situations where there are multiple active goals.
- Report performance statistics of existing and new tactic.
- Operate on terms. (Currently only operates on the tactic steps of the given file.)