Commit 2023-04-27 06:19 7a0e0252

feat: instant library_search (#3404) Well, not quite instant, but very much faster. This works by creating an extra file in the build directory containing a cache of the library_search discrimination tree.

• If you modify a file, then open another file, library_search will not see the modified declarations.
• However after a lake exe cache get or a lake env lean Extras/LibrarySearch.lean, you will see the modifications.
• In particular CI will automatically do the work of building this cache.
• This will increase the size of a lake exe cache get download (by about 20mb). To accommodate the cache file, we create a new build/extra/ directory, that can store .olean format cache files. Our cache executable now manages files in this directory too.