Tactic block caching example

Stream: general

[Keeley Hoek]

Hey everyone, first day back (after a whiiile) and I finally put together an example for the tactic-block caching stuff that people can try out. All you have to do is clone https://github.com/khoek/leancache-example.git (and make sure you have elan), and examine the somemaths-xxx.lean file in src. The files in there are shamelessly stolen from lean-category-theory and has a few statements which take a full 1- or 2-seconds to recompile normally (at least on my machine). You can turn caching on and off in the file by including tactic.tcache.enable (as stated there), as well as clear the cache and/or turn on some tracing to compare the performance with and without caching the proofs.

Full disclosure: leancache as implemented uses a 50-line changed fork of lean 3.4.2 (which will be auto-fetched by elan and is why it's necessary). It doesn't have to do this at all (as in, I've got an implementation which runs in vanilla lean too), but using the fork leads to a factor of 500-1000 performance speedup, so I think it's a pretty good idea. This is compared to a simple in-lean serializer which is also in that repo and I can explain how to try out if people want.

[Keeley Hoek]

To be clear, the fork just provides IO and serializing help, and does not have anything to do with saving and restoring the proofs. The addition to lean in the fork is simply the following: I add two functions in the io namespace called io.serialize and io.deserialize which write and read an expr to a file (respectively). This lets us leverage lean's already existing serialization facility (which is C++ and fast), and also avoids problems doing IO inside lean, especially manipulating char buffers which it turns out is very difficult and definitely hacky if you don't want to be slow (I've spent quite a lot of time trying to get this latter thing fast actually, but my attempts have been quite fruitless compared to just using the existing C++ code).

[Mario Carneiro]

aha, this sounds similar to my own experience with the olean reader in lean

[Mario Carneiro]

deserialization is still hella slow

[Keeley Hoek]

Yeah... :( Turns out (at least for me) parsing using a string.iterator is slower that using pattern-matching to munch byte-by-byte, too!

[Mario Carneiro]

I should mention that with the recent move for mathlib I've returned to seriously considering a lean fork (a.k.a LTS for lean 3)

[Keeley Hoek]

Mario... if we did that... god forbid we would be able to do all this new stuff... legit-ly

[Keeley Hoek]

:D

[Kevin Buzzard]

My impression is that when 3.4.2 came out, the community (at least those at my end) just upgraded Lean and got on with it. In fact the moment mathlib head switched to 3.4.2 the users basically had no choice, but with elan the upgrade procedure can be pretty painless, and Scott's videos seem to make sense to people.

[Chris Hughes]

With elan you don't even notice the change.