tactic caching

Stream: general

[Notification Bot]

21 messages were moved here from #CI > build time bot by Scott Morrison.

[Bolton Bailey]

About simp only and mathlib speed improvement: A quick investigation of a few randomly selected simp only calls shows that many of them can be replaced by a simp_rw call, as long as you order the list of lemmas right. If we make this change wherever possible, it could improve

1. Speed (since presumably it's better to handle simplifications one at a time rather than to look through all of the lemmas again to check that there are no further simplifications)
2. Readability (since you can see the order in which the simplifications are being applied, and even step through the proof state after each of them.
3. Code size (since simp_rw is two characters shorter than simp only)

One could write a script to make this change by trying to extract simp_only lemmas into a preceding simp_rw one at a time and only. You could even guarantee not making anything worse by checking the profiler before and after and reverting changes that hurt performance.

[Mario Carneiro]

Speed (since presumably it's better to handle simplifications one at a time rather than to look through all of the lemmas again to check that there are no further simplifications)

Actually I would expect the opposite. One of the more expensive tasks of simp is creating a customized simp set with a matcher which can efficiently handle all the subexpression matching. Changing the simp set all the time means you have to do several expression traversals, which regular simp doesn't have to do.

[Bolton Bailey]

I see, interesting.

[Eric Wieser]

\2. still feels like a strong argument

[Mario Carneiro]

incidentally, lean 4 simp? will automatically order the lemmas in the order they were used as rewrite rules

[Floris van Doorn]

There is a 4th point that I like simp_rw a lot more than simp only, and it's maintainability. If a simp only [lots of lemmas] tactic call breaks, I have no idea where to look for the culprit. If it is a simp_rw [lots of lemmas] tactic call, then you can find out which step breaks, and get a much better idea what the problem is.

[Johan Commelin]

So... can we get a sense of what the speed impact would be? I still imagine that simp_rw will be a lot faster than a bare simp. But it would be good if we can get some actual data.

[Bolton Bailey]

I did a few more random samples on the grep of all simp onlys last night. Mario was right, it does seem to be slightly slower to use simp_rw, but the change usually wasn't more than 10% of the runtime. Funnily enough, sometimes it got faster, but not necessarily because simp_rw was faster - a few of the simp only calls included unnecessary lemmas.

[Bolton Bailey]

I'll write a script to do this a bit more rigorously

[Bolton Bailey]

Ok I started #17062, still not complete and likely very buggy. Before I go further, is there any more convenient way in Python to get profiler data than calling lean --make --profile and parsing the output?

[Bolton Bailey]

Also, I was getting tripped up by some commas that didn't have spaces after them. Is there any reason I couldn't add a rule saying commas must be followed by whitespace or a newline to the linter?

[Eric Wieser]

M →ₗ⁅R,L⁆ N is used by the pretty-printer but has a comma followed by no space

[Eric Wieser]

Also, at the extreme end you don't want to ban commas of that form in docstrings or tactic error messages

[Eric Wieser]

Consider /-- We write lists with `,`s between items -/

[Eric Wieser]

I wonder if a better (but way harder) way to measure this style is by inspecting the AST

[Eric Wieser]

(to be clear, I'm in favor of linting this if we can do so without too many false positives)

[Bolton Bailey]

I think that would likely be better, yes. This also feels like another QoL improvement that might be better done after the port.