Zulip Chat Archive

Stream: general

Topic: tactic caching


Notification Bot (Oct 16 2022 at 06:38):

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

Bolton Bailey (Oct 18 2022 at 00:23):

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 (Oct 18 2022 at 00:24):

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 (Oct 18 2022 at 00:31):

I see, interesting.

Eric Wieser (Oct 18 2022 at 04:01):

\2. still feels like a strong argument

Mario Carneiro (Oct 18 2022 at 04:03):

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

Floris van Doorn (Oct 18 2022 at 06:58):

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 (Oct 18 2022 at 08:31):

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 (Oct 18 2022 at 18:53):

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 (Oct 18 2022 at 19:05):

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

Bolton Bailey (Oct 19 2022 at 23:08):

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 (Oct 19 2022 at 23:08):

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 (Oct 20 2022 at 01:41):

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

Eric Wieser (Oct 20 2022 at 01:41):

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

Eric Wieser (Oct 20 2022 at 01:42):

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

Eric Wieser (Oct 20 2022 at 01:42):

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

Eric Wieser (Oct 20 2022 at 01:43):

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

Bolton Bailey (Oct 20 2022 at 01:44):

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


Last updated: Dec 20 2023 at 11:08 UTC