[ArquintL]

This PR adds interruptVerification and interruptAstConstruction to VerificationServer. Clients of a plain ViperCoreServer can thus interrupt a single job without stopping the whole server. So far, only the LSP frontend could do this, via ViperServerService.stopVerification.

Gobra needs this API so that stopping a verification in Gobra-IDE also stops the backend. Without it, the ViperServer job and its prover processes keep running to completion and keep occupying one of the server's job slots.

• Both methods return whether an active task has been interrupted. They do not discard the job: the job's message stream completes, and the job is cleaned up, once the interrupted task has finished tearing down.
• The JobActor replies to stop requests with a typed StopProcessReply(interrupted, message) instead of a string.
• Tests run with -Xss128m, as run does already. Otherwise, the new test's program overflows the stack of Silicon's worker threads on Linux.

This PR used to contain several bug fixes as well. They are now in separate PRs stacked on this one, to be merged in this order:

1. API for interrupting jobs #357 (this PR): the interrupt API
2. Fixes hangs and leaks when cancelling jobs #367: fixes hangs and leaks when cancelling jobs
3. Stops prover processes when an interrupted verification tears down #368: stops prover processes when an interrupted verification tears down
4. Lets the LSP frontend delegate job interruption to the interrupt API #369: lets the LSP frontend delegate job interruption to the interrupt API

🤖 Generated with Claude Code

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.

[rayman2000]

Looks like the test is failing deterministically, can you take a look?

[ArquintL]

I've addressed the failing CI, polished the comments, and also unified the lifetime of AST & verification jobs. @rayman2000 could you please take another look?

[ArquintL]

@rayman2000 In my own words, this PR adds interruptAstConstruction and interruptVerification to the VerificationServer trait and, thus, ViperCoreServer (which Gobra / Gobra-IDE) uses. Without this change, Gobra is unable to abort a verification job once submitted to ViperServer.
#367 & #368 address issues that have been identified around cancelling jobs and #369 changes ViperServer's LSP frontend (used by Viper-IDE) to use the new API introduced by this PR