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>
The tests need to run with certain environment variables set that only
cmake really knows and that differ between stages. Cmake could just set
the variables directly when running the tests and benchmarks, but that
would leave no good way to manually run a single benchmark. So cmake
generates some stage-specific scripts instead that set the required
environment variables.
Previously, those scripts were sourced directly by the individual
`run_*` scripts, so the env scripts of different stages would overwrite
each other. This PR changes the setup so they can instead be generated
next to each other. This also simplifies the `run_*` scripts themselves
a bit, and makes `tests/bench/build` less of a hack.
2026-03-16 15:20:03 +00:00
Renamed from tests/server_interactive/run_test (Browse further)
