7a6c59a357
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>
13 lines
371 B
Bash
13 lines
371 B
Bash
# IO.Process.exit (used by the file worker) seems to be incompatible with LSAN
|
|
# TODO: investigate or work around
|
|
export ASAN_OPTIONS=detect_leaks=0
|
|
|
|
source_init "$1"
|
|
|
|
# these tests don't have to succeed
|
|
capture_only "$1" \
|
|
lean -Dlinter.all=false --run run_test.lean "$1"
|
|
normalize_mvar_suffixes
|
|
normalize_reference_urls
|
|
check_out_file
|
|
check_exit_is "${TEST_EXIT:-0}"
|