cached tactics

Stream: new members

[Xiyu Zhai]

This might be a very stupid question. But I want to see how to cache intermediate results in tactics.

For example, I might have a big first "first | t1 | ... | tn" with n very large, in the first run of lean compiler, it finds that tk just works. How to directly cache this so that next time it directly just tries tk?

I ask this because otherwise one has to manually reduce the big first to tk for compilation efficiency. Having a cached version completely nukes the problem. There will be no scaling problem with using big tactics.

[Vasilii Nesterov]

There is a docs#Lean.Parser.Tactic.save tactic that caches the tactic state. It helps when you're working on a heavy proof and don't want to wait for the entire proof above the cursor to be processed again every time you change something.

[Vasilii Nesterov]

But this tactic is for proof development, and has nothing to do with compilation efficiency. During compilation, each theorem is compiled only once, so no cache is needed.

[Xiyu Zhai]

Thanks a lot! That's very interesting!

I'm tailored to believe the design of a tactic system has a lot to with specific use cases. I came across the thought on cached tactics in thinking about AI completing lean proofs.