Marc Huisinga 2ede81fe10 fix: search path related bugs (#7873) ... 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>		2025-04-09 15:37:49 +00:00
..
533.lean
533.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
863.lean
863.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
1031.lean
1031.lean.expected.out
1265.lean
1265.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
1403.lean
1403.lean.expected.out	feat: update omega/solve_by_elim to use new tactic syntax, use new tactic syntax (#5932)	2024-11-03 16:23:37 +00:00
1525.lean
1525.lean.expected.out
1659.lean
1659.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
2058.lean	feat: localize universe metavariable errors at let bindings and fun binders (#5402)	2024-09-24 05:30:42 +00:00
2058.lean.expected.out	feat: localize universe metavariable errors at let bindings and fun binders (#5402)	2024-09-24 05:30:42 +00:00
2881.lean	fix: some goal state issues (#5677)	2024-10-17 12:09:54 +00:00
2881.lean.expected.out	fix: some goal state issues (#5677)	2024-10-17 12:09:54 +00:00
4078.lean	fix: hovers on binders with metavariables (#4192)	2024-05-21 10:34:58 +00:00
4078.lean.expected.out	fix: hovers on binders with metavariables (#4192)	2024-05-21 10:34:58 +00:00
4880.lean	fix: ensure autoparam errors have correct positions (#4926)	2024-08-06 22:27:51 +00:00
4880.lean.expected.out	feat: 'unsolved goals' & 'goals accomplished' diagnostics (#7366)	2025-03-07 13:50:56 +00:00
5659.lean	fix: proper "excess binders" error locations for rintro and intro (#6565)	2025-01-08 08:36:45 +00:00
5659.lean.expected.out	fix: proper "excess binders" error locations for rintro and intro (#6565)	2025-01-08 08:36:45 +00:00
6594.lean	fix: incremental goal state requests select incomplete snapshot (#6887)	2025-02-14 11:53:24 +00:00
6594.lean.expected.out	fix: incremental goal state requests select incomplete snapshot (#6887)	2025-02-14 11:53:24 +00:00
amb.lean
amb.lean.expected.out
anonHyp.lean
anonHyp.lean.expected.out
autoBoundIssue.lean	feat: upstream definition of Vector from Batteries (#6197)	2024-11-24 23:01:32 +00:00
autoBoundIssue.lean.expected.out	feat: upstream definition of Vector from Batteries (#6197)	2024-11-24 23:01:32 +00:00
builtinCodeactions.lean	fix: line break in simp? output (#6048)	2024-11-13 15:49:11 +00:00
builtinCodeactions.lean.expected.out	fix: line break in simp? output (#6048)	2024-11-13 15:49:11 +00:00
cancellation.lean	fix: cancel computations within command elaboration as soon as reuse is ruled out (#7241)	2025-03-03 10:37:10 +00:00
cancellation.lean.expected.out	fix: cancel computations within command elaboration as soon as reuse is ruled out (#7241)	2025-03-03 10:37:10 +00:00
catHover.lean	chore: fix spelling mistakes in tests (#5439)	2024-09-24 03:22:53 +00:00
catHover.lean.expected.out	chore: fix spelling mistakes in tests (#5439)	2024-09-24 03:22:53 +00:00
codeaction.lean
codeaction.lean.expected.out
compHeader.lean
compHeader.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completion.lean
completion.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completion2.lean
completion2.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completion3.lean
completion3.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completion4.lean
completion4.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completion5.lean
completion5.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completion6.lean
completion6.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completion7.lean
completion7.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completionAtPrint.lean	feat: Environment.addConstAsync (#6691)	2025-01-19 02:00:16 +00:00
completionAtPrint.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completionBracketedDot.lean	fix: travelling auto-completion (#5257)	2024-09-10 07:26:44 +00:00
completionBracketedDot.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completionCheck.lean
completionCheck.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completionDanglingDot.lean	fix: don't issue atomic id completions when there is a dangling dot (#5837)	2024-11-19 12:23:41 +00:00
completionDanglingDot.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completionDeprecation.lean	feat: denote deprecations in completion items (#5707)	2024-10-14 13:05:16 +00:00
completionDeprecation.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completionEOF.lean
completionEOF.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completionFallback.lean	feat: completion fallback (#5299)	2024-09-12 16:09:20 +00:00
completionFallback.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completionFromExpectedType.lean
completionFromExpectedType.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completionIStr.lean
completionIStr.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completionOpenNamespaces.lean
completionOpenNamespaces.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completionOption.lean
completionOption.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completionPrefixIssue.lean
completionPrefixIssue.lean.expected.out	feat: grind internal CommRing class (#7797)	2025-04-03 08:30:19 +00:00
completionPrivateTypes.lean
completionPrivateTypes.lean.expected.out	fix: search path related bugs (#7873)	2025-04-09 15:37:49 +00:00
completionPrv.lean	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completionPrv.lean.expected.out	fix: search path related bugs (#7873)	2025-04-09 15:37:49 +00:00
completionStructureInstance.lean	fix: use sensible notion of indentation in structure instance field completion (#6279)	2024-12-02 09:37:12 +00:00
completionStructureInstance.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
completionTactics.lean	fix: use sensible notion of indentation in structure instance field completion (#6279)	2024-12-02 09:37:12 +00:00
completionTactics.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
compNamespace.lean	feat: IntX operations and conversion theory (#7592)	2025-03-27 15:17:56 +00:00
compNamespace.lean.expected.out	feat: IntX operations and conversion theory (#7592)	2025-03-27 15:17:56 +00:00
definition.lean
definition.lean.expected.out
Diff.lean
Diff.lean.expected.out	feat: pretty print props with → only if domain is prop, add pp.foralls (#7812)	2025-04-04 02:55:47 +00:00
discrsIssue.lean
discrsIssue.lean.expected.out
docstringLinksExamples.lean	feat: language reference links and examples in docstrings (#7240)	2025-03-12 09:17:27 +00:00
docstringLinksExamples.lean.expected.out	feat: language reference links and examples in docstrings (#7240)	2025-03-12 09:17:27 +00:00
dotIdCompletion.lean
dotIdCompletion.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
editAfterError.lean	feat: incremental elaboration of definition headers, bodies, and tactics (#3940)	2024-05-22 13:23:30 +00:00
editAfterError.lean.expected.out	feat: incremental elaboration of definition headers, bodies, and tactics (#3940)	2024-05-22 13:23:30 +00:00
editCompletion.lean	feat: incremental elaboration of definition headers, bodies, and tactics (#3940)	2024-05-22 13:23:30 +00:00
editCompletion.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
expectedTypeAsGoal.lean
expectedTypeAsGoal.lean.expected.out
explicitAppInstHole.lean	fix: refine how named arguments suppress explicit arguments (#5283)	2024-09-27 20:14:29 +00:00
explicitAppInstHole.lean.expected.out	feat: add option pp.mvars.delayed (#5643)	2024-10-08 17:48:52 +00:00
foldingRange.lean
foldingRange.lean.expected.out
ghostGoals.lean	fix: ghost goals in autoparam tactic block (#6408)	2024-12-17 20:57:39 +00:00
ghostGoals.lean.expected.out	fix: ghost goals in autoparam tactic block (#6408)	2024-12-17 20:57:39 +00:00
goalEOF.lean
goalEOF.lean.expected.out
goalIssue.lean
goalIssue.lean.expected.out
goTo.lean	fix: search path related bugs (#7873)	2025-04-09 15:37:49 +00:00
goTo.lean.expected.out	fix: search path related bugs (#7873)	2025-04-09 15:37:49 +00:00
goTo2.lean	fix: search path related bugs (#7873)	2025-04-09 15:37:49 +00:00
goTo2.lean.expected.out	fix: search path related bugs (#7873)	2025-04-09 15:37:49 +00:00
haveInfo.lean	feat: incremental have (#4308)	2024-06-04 09:12:27 +00:00
haveInfo.lean.expected.out	feat: 'unsolved goals' & 'goals accomplished' diagnostics (#7366)	2025-03-07 13:50:56 +00:00
highlight.lean	fix: do not cancel async elaboration tasks (#7175)	2025-02-21 17:24:36 +00:00
highlight.lean.expected.out	fix: avoid new term info around def bodies (#6031)	2024-11-11 14:54:59 +00:00
hover.lean	fix: search path related bugs (#7873)	2025-04-09 15:37:49 +00:00
hover.lean.expected.out	fix: search path related bugs (#7873)	2025-04-09 15:37:49 +00:00
hoverAt.lean
hoverAt.lean.expected.out
hoverBinderUndescore.lean
hoverBinderUndescore.lean.expected.out	feat: add option pp.mvars.delayed (#5643)	2024-10-08 17:48:52 +00:00
hoverDot.lean
hoverDot.lean.expected.out	chore: normalize URLs to the language reference in test results (#7782)	2025-04-02 06:17:31 +00:00
hoverException.lean
hoverException.lean.expected.out	feat: @[builtin_doc] attribute (part 2) (#3918)	2024-09-13 08:05:10 +00:00
hoverTacticExt.lean	feat: more infrastructure for tactic documentation (#4490)	2024-06-21 12:49:30 +00:00
hoverTacticExt.lean.expected.out	feat: more infrastructure for tactic documentation (#4490)	2024-06-21 12:49:30 +00:00
incrementalCombinator.lean	fix: disable incrementality in case .. | .. (#5090)	2024-08-19 09:17:03 +00:00
incrementalCombinator.lean.expected.out	feat: 'unsolved goals' & 'goals accomplished' diagnostics (#7366)	2025-03-07 13:50:56 +00:00
incrementalCommand.lean	fix: do not cancel async elaboration tasks (#7175)	2025-02-21 17:24:36 +00:00
incrementalCommand.lean.expected.out	fix: reparsing may need to backtrack two commands (#6236)	2024-11-27 13:06:57 +00:00
incrementalInduction.lean	feat: incremental elaboration of definition headers, bodies, and tactics (#3940)	2024-05-22 13:23:30 +00:00
incrementalInduction.lean.expected.out	feat: incremental elaboration of definition headers, bodies, and tactics (#3940)	2024-05-22 13:23:30 +00:00
incrementalMutual.lean	fix: calculate error suppression per snapshot (#4657)	2024-07-08 09:54:43 +00:00
incrementalMutual.lean.expected.out	fix: calculate error suppression per snapshot (#4657)	2024-07-08 09:54:43 +00:00
incrementalTactic.lean	fix: calculate error suppression per snapshot (#4657)	2024-07-08 09:54:43 +00:00
incrementalTactic.lean.expected.out	feat: pretty print props with → only if domain is prop, add pp.foralls (#7812)	2025-04-04 02:55:47 +00:00
infoIssues.lean
infoIssues.lean.expected.out
internalNamesIssue.lean
internalNamesIssue.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
inWordCompletion.lean	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
inWordCompletion.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
issue4527.lean	fix: cdot parser error message range (#4528)	2024-06-21 15:06:07 +00:00
issue4527.lean.expected.out	feat: 'unsolved goals' & 'goals accomplished' diagnostics (#7366)	2025-03-07 13:50:56 +00:00
issue5021.lean	fix: hover text over _ in ?_ (#5118)	2024-08-21 20:47:19 +00:00
issue5021.lean.expected.out	chore: fix spelling mistakes (#7328)	2025-04-07 01:15:48 +00:00
issue5597.lean	fix: declareSimpLikeTactic macro to use mkSynthetic (#5838)	2024-10-30 14:27:56 +00:00
issue5597.lean.expected.out	fix: declareSimpLikeTactic macro to use mkSynthetic (#5838)	2024-10-30 14:27:56 +00:00
jumpMutual.lean	fix: search path related bugs (#7873)	2025-04-09 15:37:49 +00:00
jumpMutual.lean.expected.out	fix: search path related bugs (#7873)	2025-04-09 15:37:49 +00:00
keywordCompletion.lean
keywordCompletion.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
lean3HoverIssue.lean
lean3HoverIssue.lean.expected.out
macroGoalIssue.lean
macroGoalIssue.lean.expected.out
match.lean
match.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
matchPatternHover.lean
matchPatternHover.lean.expected.out
matchStxCompletion.lean
matchStxCompletion.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
partialNamespace.lean
partialNamespace.lean.expected.out
plainGoal.lean
plainGoal.lean.expected.out	feat: pretty print props with → only if domain is prop, add pp.foralls (#7812)	2025-04-04 02:55:47 +00:00
plainTermGoal.lean
plainTermGoal.lean.expected.out
rename.lean
rename.lean.expected.out
run.lean	test: avoid re-elaboration of interactive runner (#7177)	2025-02-22 10:36:25 +00:00
stdOutput.lean
stdOutput.lean.expected.out
structNameParentProj.lean	feat: make structure parent projections nameable (#7100)	2025-02-18 07:38:13 +00:00
structNameParentProj.lean.expected.out	feat: make structure parent projections nameable (#7100)	2025-02-18 07:38:13 +00:00
terminationBySuggestion.lean	feat: termination_by structural (#4542)	2024-07-01 16:51:30 +00:00
terminationBySuggestion.lean.expected.out	feat: termination_by structural (#4542)	2024-07-01 16:51:30 +00:00
test_single.sh
travellingCompletions.lean	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
travellingCompletions.lean.expected.out	feat: faster auto-completion (#7134)	2025-02-19 10:05:18 +00:00
unterminatedDocComment.lean	feat: incremental elaboration of definition headers, bodies, and tactics (#3940)	2024-05-22 13:23:30 +00:00
unterminatedDocComment.lean.expected.out	feat: incremental elaboration of definition headers, bodies, and tactics (#3940)	2024-05-22 13:23:30 +00:00
userWidget.lean
userWidget.lean.expected.out