Commit 2023-05-07 08:35 acf194c9

View on Github →

feat: speedup library_search by using two DiscrTrees (#3771) Previously, library_search used a single DiscrTree. There is a cached DiscrTree covering the whole library (and which is cached to disk), and then when we call library_search, we traverse the declarations in the current file, adding those into that DiscrTree. This PR speeds up that process by using a second independent DiscrTree for the declarations in the current file. This means that the cached tree for the library does not need to be "edited in place", and so we save some time. On the test file on my computer this speeds up from around 10.0s to around 8.2s. When calling library_search low down in a large file we should expect larger gains. The PR also does some refactoring work on DeclCache, which will be useful if/when we install global caching for other lookup tactics such as propose or rewrites.

Estimated changes