This PR fixes a regression where elaboration of a previous document
version is not cancelled on changes to the document.
Done by removing the default from `SnapshotTask.cancelTk?` and
consistently passing the current thread's token for synchronous
elaboration steps.
This PR fixes a number of bugs related to the handling of the source
search path in the language server, where deleting files could cause
several features to stop functioning and both untitled files and files
that don't exist on disc could have conflicting module names.
In detail, it makes the following adjustments:
- The URI <-> module name conversion was adjusted to produce no name
collisions.
- File URIs in the search path yield a module name relative to the
search path, as before.
- File URIs not in the search path, non-file URIs and non-`.lean` files
yield a `«external:<full uri>»` module name.
- To avoid the issue of the URI -> module name conversion failing when a
file is deleted from disc, we now cache the result of this conversion in
the watchdog and the file worker when the file is first opened.
- All of the URI <-> module name conversions now consistently go through
`Server.documentUriFromModule?` and `moduleFromDocumentUri` to ensure
that we don't have minor deviations for this conversion all over the
place.
- The threading of the source search path through the file worker (from
`lake setup-file`) is removed. It turns out that `lake serve` already
sets the correct source search path in the environment, so we can just
always use the search path from the environment.
- Since we can now answer more requests that need the .ileans in
untitled files, a lot of the tests that test 'Go to definition' needed
to be adjusted so that they use the information from the watchdog, not
the file worker. As we load references asynchronously, this PR adds an
internal `$/lean/waitForILeans` request that tests can use to wait for
all .ilean files to be loaded and for the ilean references from the file
worker for the current document version to be finalized.
- As part of this PR, we noticed that the .ileans aren't available in
the NixOS setup, so @Kha adjusted the Nix CI to fix this.
### Breaking changes
- `Server.documentUriFromModule` has been renamed to
`Server.documentUriFromModule?` and doesn't take a `SearchPath` argument
anymore, as the `SearchPath` is now computed from the `LEAN_SRC_PATH`
environment variable. It has also been moved from `Lean.Server.GoTo` to
`Lean.Server.Utils`.
- `Server.moduleFromDocumentUri` does not take a `SearchPath` argument
anymore and won't return an `Option` anymore. It has also been moved
from `Lean.Server.GoTo` to `Lean.Server.Utils`.
- The `System.SearchPath.searchModuleNameOfUri` function has been
removed. It is recommended to use `Server.moduleFromDocumentUri`
instead.
- The `initSrcSearchPath` function has been renamed to
`getSrcSearchPath` and has been moved from `Lean.Util.Paths` to
`Lean.Util.Path`. It also doesn't need to take a `pkgSearchPath`
argument anymore.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Before/after:
```
make -C build/release test ARGS="-j$(nproc) -R interactive" 208.10s user 20.93s system 1982% cpu 11.552 total
make -C build/release test ARGS="-j$(nproc) -R interactive" 87.22s user 22.58s system 1454% cpu 7.548 total
```
This PR fixes an `Elab.async` regression where elaboration tasks are
cancelled on document edit even though their result may be reused in the
new document version, reporting an incomplete result.
While this PR fixes the functional regression, it does so as an
over-approximation by never cancelling such tasks. A follow-up PR will
implement the correct behavior of only cancelling the tasks that are not
reused.
