grind performance questions

Stream: general

[Chris Henson]

In general, is there a "startup cost" to calling the grind tactic that makes it better to combine calls when possible? E.g. if I have

have := foo (by grind)
have := bar (by grind)
grind

and I know that

have := foo
have := bar
grind

would also work, is there a preference between them? Or is the work done by grind incrementally stored in a way that makes this irrelevant?

[Chris Henson]

This is somewhat related to the discussion at #lean4 > grind_calc, i.e. the question how to consider:
Frédéric Dupuis said:

unless there's a caching mechanism I'm not aware of, basically restarts grind everytime on more or less the same proof state.

in terms of performance.

[Jovan Gerbscheid]

What's wrong with grind [foo, bar]?

[Jovan Gerbscheid]

To answer your actual question, yes there is a startup cost to calling grind, though presumably this is only significant if your local context is complicated.

In general you can use the interactive mode grind => in order to only pay the startup cost a single time.

[Jovan Gerbscheid]

If you're unfamiliar with grind =>, I'd suggest watching the Lean together talk by Kim Morrison which does a good job at presenting this feature.

[Alex Meiburg]

Jovan Gerbscheid said:

What's wrong with grind [foo, bar]?

I've definitely encountered cases where have := foo; grind works but grind [foo] doesn't, fwiw! Would that be an issue and worth reporting?

[Chris Henson]

Jovan Gerbscheid said:

What's wrong with grind [foo, bar]?

I'd have to do a bit of work to minimize this from CSLib, but there are some situations where for performance reasons I'd pass some additional parameters to these theorems, making this not exactly the same.

Jovan Gerbscheid said:

To answer your actual question, yes there is a startup cost to calling grind, though presumably this is only significant if your local context is complicated.

In general you can use the interactive mode grind => in order to only pay the startup cost a single time.

Good to confirm, thanks! I just wanted to double check my intuition about startup cost before suggesting this in CSLib. I am familiar with the interactive mode and watched Kim's talk. (In fact I just opened up a PR to Mathlib that I think makes good use of it in addressing the weekly mergeWithGrind linting!)

[Jovan Gerbscheid]

Alex Meiburg said:

I've definitely encountered cases where have := foo; grind works but grind [foo] doesn't, fwiw! Would that be an issue and worth reporting?

grind [foo] for an arbitrary proof foo is a relatively new feature. Maybe you were on an older version? I'd expect this to always work, yes.