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 --outfile /tmp/out.json
Progress will be displayed via stderr as it happens.
Upon completion, /tmp/out.json will contain JSON describing the results.
running on all files in a directory
The tryAtEachStepInDirectory tool runs tryAtEachStep on all .lean files
under a given directory. For example:
$ lake exe tryAtEachStepInDirectory "with_reducible exact?" YourLibrary -j 31
The -j 31 argument specifies that 31 jobs should be run in parallel.
Results are written as JSON in a directory with name tryAtEachStep-out-XXXXXXXX,
where the X's get filled in randomly.
You can specify a different output directory via --outdir.
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
- 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.)