max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/server_interactive
History
Joachim Breitner 7a6c59a357
fix: abort waitFor server_interactive tests promptly on file worker fatal error (#13710) 
This PR makes the test-only `waitForMessage` helper abort promptly
when the Lean language server reports a fatalError, instead of
blocking until the outer test framework's timeout kills the process.

`waitForMessage` is used to implement the `waitFor` directive in
`tests/server_interactive` tests: it reads server messages in a loop
and returns when it sees a `textDocument/publishDiagnostics`
notification containing a given message. It has no pending request,
so the watchdog's `responseError` (which already terminates
`collectDiagnostics` and `waitForILeans` on a fatalError) doesn't
help here, and it would silently discard `$/lean/fileProgress`
notifications. When the file worker crashes or its header processing
fails fatally (e.g. an unresolved import), the awaited diagnostic
will never be emitted -- so `waitForMessage` would block indefinitely
and report nothing useful, which made several CI failures of
server_interactive tests look like generic 1500s timeouts. With this
change, `waitForMessage` also reacts to `$/lean/fileProgress` with
`fatalError` kind and throws a descriptive error.

The detection is scoped to `waitForMessage` only, not the underlying
`Ipc.readMessage`, so that other IPC paths (notably
`importCompletion.lean`, which intentionally elaborates a file with
an incomplete `import` line and observes the resulting fatalError
fileProgress while still using the alive worker for completion
requests) keep working unchanged. As part of this PR, `waitForMessage`
has been moved out of `Lean.Lsp.Ipc` and into
`Lean.Server.Test.Runner` next to its sole caller `processWaitFor`,
since it is a test-driver helper rather than a general-purpose IPC
primitive (it discards all unrelated messages, which would be unsafe
outside of a test driver).

To exercise the new behavior, `tests/server_interactive/run_test.sh`
now sources `<file>.init.sh` and uses `check_exit_is "${TEST_EXIT:-0}"`,
matching the convention in `tests/compile/`. The new
`worker_crash.lean` test forces the file worker to die via
`IO.Process.forceExit 9` from inside an `elab` command and then
issues a `waitFor` directive that can never be satisfied;
`TEST_EXIT=1` and `.out.expected` capture the abort path. Without
this PR the test would sit at the framework timeout; with this PR it
returns in well under a second.

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
2026-05-12 20:53:17 +00:00
..
533.lean
533.lean.out.expected
863.lean
863.lean.out.expected
1018unknowMVarIssue.lean
1018unknowMVarIssue.lean.out.expected
1031.lean
1265.lean
1265.lean.out.expected
1403.lean
1403.lean.out.expected
1525.lean
1659.lean
1659.lean.out.expected
2058.lean
2058.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
2881.lean
2881.lean.out.expected
4078.lean
4078.lean.out.expected
4880.lean
4880.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
5659.lean
5659.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
6594.lean
6594.lean.out.expected fix: filter assigned metavariables before computing apply subgoal tags (#13476) 2026-04-19 14:31:49 +00:00
10898.lean
10898.lean.out.expected
amb.lean
amb.lean.out.expected
anonHyp.lean
anonHyp.lean.out.expected
autoBoundIssue.lean
autoBoundIssue.lean.out.expected
builtinCodeactions.lean
builtinCodeactions.lean.out.expected
cancellation.lean
cancellation.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
cancellation_try_plain.lean feat: empty by runs try? to suggest a proof (#13430) 2026-05-11 06:31:42 +00:00
cancellation_try_plain.lean.out.expected feat: empty by runs try? to suggest a proof (#13430) 2026-05-11 06:31:42 +00:00
catHover.lean
catHover.lean.out.expected
codeaction.lean
codeaction.lean.out.expected
codeActions.lean
codeActions.lean.out.expected
compHeader.lean
compHeader.lean.out.expected
completion.lean
completion.lean.out.expected
completion2.lean
completion2.lean.out.expected
completion3.lean
completion3.lean.out.expected
completion4.lean
completion4.lean.out.expected
completion5.lean
completion5.lean.out.expected
completion6.lean
completion6.lean.out.expected
completion7.lean
completion7.lean.out.expected
completionAtPrint.lean
completionAtPrint.lean.out.expected
completionBracketedDot.lean
completionBracketedDot.lean.out.expected
completionCheck.lean
completionCheck.lean.out.expected
completionDanglingDot.lean
completionDanglingDot.lean.out.expected
completionDeprecation.lean
completionDeprecation.lean.out.expected
completionEmptyBy.lean fix: tactic completion in empty by blocks (#13348) 2026-04-15 08:39:55 +00:00
completionEmptyBy.lean.out.expected fix: tactic completion in empty by blocks (#13348) 2026-04-15 08:39:55 +00:00
completionEmptyByBracketed.lean fix: tactic completion in empty by blocks (#13348) 2026-04-15 08:39:55 +00:00
completionEmptyByBracketed.lean.out.expected fix: tactic completion in empty by blocks (#13348) 2026-04-15 08:39:55 +00:00
completionEndSection.lean
completionEndSection.lean.out.expected
completionEOF.lean
completionEOF.lean.out.expected
completionFallback.lean
completionFallback.lean.out.expected
completionFromExpectedType.lean
completionFromExpectedType.lean.out.expected
completionIStr.lean
completionIStr.lean.out.expected
completionOpenNamespaces.lean
completionOpenNamespaces.lean.out.expected
completionOption.lean
completionOption.lean.out.expected
completionPrefixIssue.lean
completionPrefixIssue.lean.out.expected
completionPrivateTypes.lean
completionPrivateTypes.lean.out.expected
completionPrv.lean
completionPrv.lean.out.expected
completionStructureInstance.lean
completionStructureInstance.lean.out.expected
completionTactics.lean fix: tactic completion in empty by blocks (#13348) 2026-04-15 08:39:55 +00:00
completionTactics.lean.out.expected fix: tactic completion in empty by blocks (#13348) 2026-04-15 08:39:55 +00:00
compNamespace.lean
compNamespace.lean.out.expected
definition.lean
definition.lean.out.expected
Diff.lean
Diff.lean.out.expected feat: update RPC wire format (#12905) 2026-03-13 23:46:16 +00:00
discrsIssue.lean
discrsIssue.lean.out.expected
docstringLinksExamples.lean
docstringLinksExamples.lean.out.expected
documentSymbols.lean
documentSymbols.lean.out.expected
dotIdCompletion.lean
dotIdCompletion.lean.out.expected
dottedIdentNotation.lean
dottedIdentNotation.lean.out.expected
editAfterError.lean
editAfterError.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
editCompletion.lean
editCompletion.lean.out.expected
errorExplanationInteractive.lean
errorExplanationInteractive.lean.out.expected
expectedTypeAsGoal.lean
expectedTypeAsGoal.lean.out.expected
explicitAppInstHole.lean
explicitAppInstHole.lean.out.expected
findReferences.lean
findReferences.lean.out.expected
foldingRange.lean
foldingRange.lean.out.expected
fvarIdCollision.lean
fvarIdCollision.lean.out.expected
ghostGoals.lean
ghostGoals.lean.out.expected
goalEOF.lean
goalEOF.lean.out.expected
goalIssue.lean
goalIssue.lean.out.expected
goalsAccomplished.lean
goalsAccomplished.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
goTo.lean
goTo.lean.out.expected
goTo2.lean
goTo2.lean.out.expected
guardMsgsCodeAction.lean
guardMsgsCodeAction.lean.out.expected
haveInfo.lean
haveInfo.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
highlight.lean
highlight.lean.out.expected
highlightMatches.lean
highlightMatches.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
hover.lean fix: preserve symbol hover for fun_induction function target (#13678) 2026-05-07 12:09:36 +00:00
hover.lean.out.expected fix: preserve symbol hover for fun_induction function target (#13678) 2026-05-07 12:09:36 +00:00
hoverAt.lean
hoverAt.lean.out.expected
hoverBinderUnderscore.lean
hoverBinderUnderscore.lean.out.expected
hoverDoForIn.lean fix: add term info for for loop variables in new do elaborator (#13399) 2026-04-13 20:29:55 +00:00
hoverDoForIn.lean.out.expected fix: add term info for for loop variables in new do elaborator (#13399) 2026-04-13 20:29:55 +00:00
hoverDot.lean
hoverDot.lean.out.expected
hoverException.lean
hoverException.lean.out.expected
hoverMatch.lean
hoverMatch.lean.out.expected
hoverTacticExt.lean
hoverTacticExt.lean.out.expected
importCompletion.lean
importCompletion.lean.out.expected
incomingCallHierarchy.lean
incomingCallHierarchy.lean.out.expected
incomingCallHierarchyWhere.lean
incomingCallHierarchyWhere.lean.out.expected
incrementalCombinator.lean
incrementalCombinator.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
incrementalCommand.lean
incrementalCommand.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
incrementalInduction.lean
incrementalInduction.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
incrementalMutual.lean
incrementalMutual.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
incrementalTactic.lean
incrementalTactic.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
infoIssues.lean
infoIssues.lean.out.expected
inlayHints.lean
inlayHints.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
interactiveDiagnostics.lean
interactiveDiagnostics.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
interactiveGoalGoToLoc.lean
interactiveGoalGoToLoc.lean.out.expected feat: update RPC wire format (#12905) 2026-03-13 23:46:16 +00:00
interactiveGoalPopups.lean
interactiveGoalPopups.lean.out.expected feat: update RPC wire format (#12905) 2026-03-13 23:46:16 +00:00
interactiveTermGoals.lean
interactiveTermGoals.lean.out.expected feat: update RPC wire format (#12905) 2026-03-13 23:46:16 +00:00
interactiveTraces.lean
interactiveTraces.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
internalNamesIssue.lean
internalNamesIssue.lean.out.expected
inWordCompletion.lean
inWordCompletion.lean.out.expected
isRflParallel.lean
issue4527.lean
issue4527.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
issue5021.lean
issue5021.lean.out.expected
issue5597.lean
issue5597.lean.out.expected
jumpMutual.lean
jumpMutual.lean.out.expected
keywordCompletion.lean
keywordCompletion.lean.out.expected
lean3HoverIssue.lean
lean3HoverIssue.lean.out.expected
macroGoalIssue.lean
macroGoalIssue.lean.out.expected
match.lean
match.lean.out.expected
matchPatternHover.lean
matchPatternHover.lean.out.expected
matchStxCompletion.lean
matchStxCompletion.lean.out.expected
moduleHierarchyImports.lean
moduleHierarchyImports.lean.out.expected
outgoingCallHierarchy.lean
outgoingCallHierarchy.lean.out.expected
partialNamespace.lean
partialNamespace.lean.out.expected
plainGoal.lean feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
plainGoal.lean.out.expected feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
plainGoalEmptyBy.lean feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
plainGoalEmptyBy.lean.out.expected feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
plainTermGoal.lean
plainTermGoal.lean.out.expected
ppShowLetValues.lean
ppShowLetValues.lean.out.expected
rename.lean
rename.lean.out.expected
run_test.lean
run_test.sh fix: abort waitFor server_interactive tests promptly on file worker fatal error (#13710) 2026-05-12 20:53:17 +00:00
rwElabConst.lean
rwElabConst.lean.out.expected
semanticTokens.lean
semanticTokens.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
semanticTokensVersoDocs.lean
semanticTokensVersoDocs.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
signatureHelp.lean
signatureHelp.lean.out.expected
stdOutput.lean
strInterpSynthError.lean
strInterpSynthError.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
structInstFieldHints.lean
structInstFieldHints.lean.out.expected
structNameParentProj.lean
structNameParentProj.lean.out.expected
tacticInduction.lean
tacticInduction.lean.out.expected
terminationBySuggestion.lean
terminationBySuggestion.lean.out.expected
travellingCompletions.lean
travellingCompletions.lean.out.expected
tryThisCodeAction.lean
tryThisCodeAction.lean.out.expected
unknownIdentifierCodeActions.lean
unknownIdentifierCodeActions.lean.out.expected
unterminatedDocComment.lean
unterminatedDocComment.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
userWidget.lean feat: update RPC wire format (#12905) 2026-03-13 23:46:16 +00:00
userWidget.lean.out.expected
worker_crash.lean fix: abort waitFor server_interactive tests promptly on file worker fatal error (#13710) 2026-05-12 20:53:17 +00:00
worker_crash.lean.init.sh fix: abort waitFor server_interactive tests promptly on file worker fatal error (#13710) 2026-05-12 20:53:17 +00:00
worker_crash.lean.out.expected fix: abort waitFor server_interactive tests promptly on file worker fatal error (#13710) 2026-05-12 20:53:17 +00:00
workspaceSymbols.lean
workspaceSymbols.lean.out.expected