Closed jneem closed 3 weeks ago
@yannham I've implemented the solution we discussed yesterday, where the full recursive invalidation happens in the cache.
It occurred to me that there's still some possibility for misuse in the cache API, since replace_string
deletes the cached term without invalidating things that import it. Maybe replace_string
should do the invalidation automatically? I didn't do that here because it's more invasive...
It occurred to me that there's still some possibility for misuse in the cache API, since replace_string deletes the cached term without invalidating things that import it. Maybe replace_string should do the invalidation automatically? I didn't do that here because it's more invasive...
Hmm, I'm not entirely set on this. On one hand you're right that this has the same risk of kinda inconsistent state lying around. On the other hand replace_string
is used in practice for like queries and error message snippets, which shouldn't be imported from anywhere. Well then maybe it's virtually free to invalidate the reverse dependencies, because in practice there shouldn't be any?
Well then maybe it's virtually free to invalidate the reverse dependencies, because in practice there shouldn't be any?
That's probably right, I just didn't want this bugfix to have unintended consequences...
In nls, if
main.ncl
importsdep.ncl
anddep.ncl
changes, we need to invalidate some cached data aboutmain.ncl
and re-check it. Previously we were simply resettingmain.ncl
to the "parsed" state in the cache, but this isn't sufficient because our cached term formain.ncl
might depend ondep.ncl
. Specifically, import resolution ofmain.ncl
transforms the term in a way that depends on whetherdep.ncl
parsed.This PR does the most inefficient (but easiest to get correct) thing: throwing out all the parsed data and re-parsing from scratch. This can be optimized, but it probably isn't too much slower than the status quo, because we were re-typechecking from scratch anyway.
Fixes #1943 and maybe also #1942 and #1935. There are still some bugs related to cache state in the background worker, which I will investigate next.