Cacheless library search

Stream: std4

[Joe Hendrix]

Hi, I am working on improving the efficiency of initializing a library search database. This is in std4#421. I thought I'd start a topic here to get feedback.

To do this, I have a "lazy" discriminator tree. It uses the logic of the existing Lean discriminator tree and doesn't explore any of the higher order features of this discussion. However, that is largely orthogonal and there's a primitive mechanism for swapping out the exact? and apply? candidate selection operation.

Performance seem to be about 4-5x faster. It takes about 8.5 seconds for Lean to process a file that imports Mathlib and calls exact? on a simple lemma. Without the new discriminator tree, the same test takes 41 seconds. Projects not using Mathlib should see sub second responses, but I have a relatively fast machine so more testing is needed.

One other difference is that the cache-less approach doesn't know about names that aren't in the current environment. For exact? and apply? this shouldn't matter. There may be other tactics in Mathlib that use library_search and would want all names though.