feat(tactic): tactic block caching

[semorrison]

This is all @khoek's work, I'm just putting it here to make it easy to try out and discuss.

This PR adds tactic block caching to Lean. To turn it on, simply

import tactic.tcache.enable

in some Lean file. Make edits, and observe that the rest of the file magically compiles faster...

There does appear to be one bug: by X; Y blocks cause it to produce error messages. Likely this is easy to fix, but I didn't look into it. (Changing them to the preferred by { X, Y } does solve this problem.)

[semorrison]

There's also:

-- Trace which declarations have blocks being cached
set_option trace.tcache true

-- Uncomment to clear the cache (recomment afterword)
-- #clear tcache

[khoek]

One thing to note is that now that community lean is in use, the serialization/deserialization is like 100x faster using the native calls I added ages ago.

[semorrison]

One thing to note is that now that community lean is in use, the serialization/deserialization is like 100x faster using the native calls I added ages ago.

@khoek, is there a version of this available somewhere that uses the core serialization functions?

[khoek]

Ok, so it is in a workable state now.

In this branch it is included into tactic.core, so to try it go into some files and just type cache_file? just under the imports (the question mark gives you nice annotations on everything that was cached). Random files I tried to find with long-ish tidy proofs were significantly improved---random example is colim_coyoneda at the end of limits.lean.

The first time you do it the cache will have to be generated obviously, and you'll see annotations saying "regenerating proof". Then if you comment out cache_file? and then uncomment everything should pop-back speedily. (clear_cache will erase the entire cache directory, so you can try again afterward.)

Random observations:

1. Some slow definitions load instantly when cached, others take an appreciable amount of time still, probably the latter are doing work which we aren't capturing (right now we cache only any explicit begin ... end/by block or anything which invokes obviously---I didn't wrap tidy directly).
2. Very occasionally a definition can't load from the cache, giving an error---this is a bug in my metavariable/universe managing code, and there is no reason tcache can't be changed to silently drop such errors and just recompute the proof again---but for right now this is nice because you can pinpoint what is failing. (Actually, another possibility for such errors is that the goal hashing function is giving a collision due to not discriminating between exprs well enough, but I think all of those type problems have been squashed.)

[khoek]

If you want to cache only what a specific tactic does in a big long interactive proof (say that tactic was rewrite_search or tidy), but without enabling global caching, you do tc <tac> or tcache <tac> instead of tac.

Also, this can be helpful even when your whole file is being cached---if you are trying to write a begin ... end block and you're halfway through, and you've already called an expensive tactic above, you can tc <tac> the expensive tactic so every time you type you don't have to wait for it to run to see the new state.

Obvious candidates for other things to tcache automatically are things like omega, I guess. Also, I don't know what happened to the vampire pull request, but it wouldn't need to emit a "certificate" file to store its proofs this way---it would just emit an expr in lean which would get passed to tcache.

[khoek]

In order to make this completely usable while working, we need one more patch to core lean, or the vscode plugin (the way I see it). The problem is that when you edit a begin ... end block after a successful proof has been generated, while caching is enabled, the old cached proof will still be recalled and you can totally screw up the block (as long as it still compiles) without an error being raised.

There either needs to be a) a simple extension to the interactor.executor function which passes execute_with an optional boolean indicating that the begin ... end or by ... block being passed is being executed due to manual intervention, compared to automatic reading a file (the elegant solution), or (the hack) the vscode plugin detects (presumably by hacky methods) what you are doing when you are editing a begin ... end block, and deletes the corresponding cache file silently.

[semorrison]

a simple extension to the interactor.executor function which passes execute_with an optional boolean indicating that the begin ... end or by ... block being passed is being executed due to manual intervention, compared to automatic reading a file (the elegant solution)

How about we make a tracking issue for this?

At the same time, I would love if execute_with were also passed the pos of the begin and end keywords, so that the executor can position messages on them.

[jcommelin]

I think a tracking issue is a great idea. I would love to get this into mathlib... this PR shouldn't rot away.

[gebner]

Remove

[gebner]

Remove

[gebner]

Please replace by undefined_core.

[robertylewis]

This could certainly use module docs/some kind of high-level overview of what's going on. The command docs could also be expanded; someone looking over the doc pages wouldn't learn much from what's there now.