Merge pull request #2811 from fan-tom/strip-startup-error-stacktraces

Strip long ZIO traces on startup error

.unreleased/bug-fixes/2811-server-bind-error.md

@@ -0,0 +1,2 @@
+When expected server port is already bound, report clean user error instead of
+crashing with a traceback  (#2676).

shai/src/main/scala/at/forsyte/apalache/shai/v1/RpcServer.scala

@@ -1,13 +1,16 @@
 package at.forsyte.apalache.shai.v1
 
-import zio.{console, Ref, ZEnv, ZIO}
+import zio.{console, ExitCode, Ref, ZEnv, ZIO}
 
 import java.util.UUID
 import scalapb.zio_grpc.ServerMain
 import scalapb.zio_grpc.ServiceList
 import com.typesafe.scalalogging.LazyLogging
 import io.grpc.ServerBuilder
 
+import java.io.IOException
+import java.net.BindException
+
 /**
  * The Shai RPC server handling gRPC requests to interact with the model checker
  *
@@ -39,10 +42,24 @@ class RpcServer(override val port: Int) extends ServerMain with LazyLogging {
   // https://github.com/informalsystems/apalache/issues/2622
   override def builder: (x0) forSome { type x0 <: ServerBuilder[x0] } =
     super.builder.maxInboundMessageSize(8 * 1024 * 1024)
+
+  override def run(args: List[String]) = {
+    myAppLogic.catchAll { t =>
+      t match {
+        // treat "post already in use" error specially
+        case e: IOException if e.getCause.isInstanceOf[BindException] =>
+          logger.error(s"${RpcServer.STARTUP_ERROR_PROMPT} ${e.getMessage}: ${e.getCause.getMessage}")
+        case _ =>
+          logger.error(RpcServer.STARTUP_ERROR_PROMPT, t)
+      }
+      ZIO.succeed(ExitCode.failure)
+    }
+  }
 }
 
 object RpcServer {
   val DEFAULT_PORT = 8822
+  val STARTUP_ERROR_PROMPT = "Error while starting Apalache server:"
 
   def apply(port: Int = DEFAULT_PORT) = new RpcServer(port)
 }

test/tla/cli-integration-tests.md

@@ -3999,6 +3999,38 @@ The Apalache server is running on port 8888. Press Ctrl-C to stop.
 ...
 ```
 
+### server mode: error is nicely reported when port is already in use
+
+NOTE: These tests are skipped because the would complicate our CI process
+more than is warranted by the functionality they test. To enable these tests,
+remove the `$MDX skip` annotations.
+
+Start socat in the background to occupy the port, save its pid and wait a second to let binding happen
+<!-- $MDX skip -->
+```sh
+$ socat TCP-L:8888,fork,reuseaddr - & echo $! > pid.pid && sleep 1
+```
+
+Try to start the Apalache server on the occupied port,
+redirect its output to the file,
+save its exit code,
+strip logger prompt 
+and exit with status code of the server
+<!-- $MDX skip -->
+```sh
+$ apalache-mc server --port=8888 1>out 2>out; ext=$? && cat out | sed -E 's/E@.*$//' && exit $ext
+...
+Error while starting Apalache server: Failed to bind to address 0.0.0.0/0.0.0.0:8888: Address already in use
+[1]
+```
+
+Cleanup: kill socat and delete temporary files
+<!-- $MDX skip -->
+```sh
+$ cat pid.pid | xargs kill -9
+$ rm pid.pid out
+```
+
 ## quint input
 
 ### quint input: quint spec can be checked