Removes Akka and refactors around this removal

build.sbt

@@ -25,12 +25,16 @@ lazy val server = (project in file("."))
         fork := true,
 
         libraryDependencies += "net.liftweb" %% "lift-json" % "3.5.0",
-        libraryDependencies += "com.typesafe.akka" %% "akka-actor" % "2.6.10",
-        libraryDependencies += "com.typesafe.akka" %% "akka-http-spray-json" % "10.2.1",
-        libraryDependencies += "com.typesafe.akka" %% "akka-stream" % "2.6.10",
-        libraryDependencies += "com.typesafe.akka" %% "akka-stream-testkit" % "2.6.10" % Test,
-        libraryDependencies += "com.typesafe.akka" %% "akka-http-testkit" % "10.2.1" % Test,
         libraryDependencies += "org.eclipse.lsp4j" % "org.eclipse.lsp4j" % "0.20.1", // Java implementation of language server protocol
+        libraryDependencies += "com.lihaoyi" %% "cask" % "0.9.5", // Lightweight HTTP server (replaces Akka HTTP)
+        libraryDependencies += "io.spray" %% "spray-json" % "1.3.6", // JSON AST and serialization (existing marshallers)
+        // upickle is pulled transitively by cask. Silver depends on an older
+        // upickle so allow the newer version (cask's) to win.
+        libraryDependencySchemes += "com.lihaoyi" %% "upickle" % "always",
+        libraryDependencySchemes += "com.lihaoyi" %% "upickle-core" % "always",
+        libraryDependencySchemes += "com.lihaoyi" %% "upickle-implicits" % "always",
+        libraryDependencySchemes += "com.lihaoyi" %% "ujson" % "always",
+        libraryDependencySchemes += "com.lihaoyi" %% "geny" % "always",
 
         silicon / excludeFilter := "logback.xml", /* Ignore Silicon's Logback configuration */
         carbon / excludeFilter := "logback.xml", /* Ignore Carbon's Logback configuration */

src/main/scala/viper/server/ViperConfig.scala

@@ -119,15 +119,6 @@ class ViperConfig(args: Seq[String]) extends ScallopConf(args) {
     noshort = false,
     hidden = false)
 
-  val actorCommunicationTimeout: ScallopOption[Int] = opt[Int]("actorCommunicationTimeout", 'a',
-    descr = ("Specifies the maximal amount of time that actors will wait when communicating requesting messages from other actors."
-      + s"The number is of unit milliseconds and must be positive integer."
-      + "If the option is omitted, a default timeout of 5000 milliseconds will be set."),
-    default = Some(5000),
-    noshort = false,
-    hidden = true
-  )
-
   val maximumActiveJobs: ScallopOption[Int] = opt[Int]("maximumActiveJobs", 'm',
     descr = ("Specifies the maximal amount of jobs that may run concurrently."
       + s"The number must be positive integer."

src/main/scala/viper/server/ViperServerRunner.scala

@@ -23,6 +23,7 @@ object ViperServerRunner {
   var viperServerHttp: ViperHttpServer = _
 
   def main(args: Array[String]): Unit = {
+    // Banner emitted before the server (and thus its logger) is constructed.
     println(s"${BuildInfo.projectName} ${BuildInfo.projectVersionExtended}")
     val config = new ViperConfig(args.toIndexedSeq)
     val executor = new DefaultVerificationExecutionContext(threadPoolSize = Some(config.nThreads()))
@@ -43,9 +44,9 @@ object ViperServerRunner {
     viperServerHttp.start()
     // wait until server has been stopped:
     Await.ready(viperServerHttp.stopped(), Duration.Inf)
-    println("HTTP server has been stopped")
+    viperServerHttp.globalLogger.info("HTTP server has been stopped")
     executor.terminate()
-    println("executor service has been shut down")
+    viperServerHttp.globalLogger.info("executor service has been shut down")
     // the following `exit` call is required such that the server eventually terminates for `longDuration.vpr` in the
     // test suite of viper-ide
     System.exit(0)
@@ -55,26 +56,29 @@ object ViperServerRunner {
     * Run VCS in LSP mode.
     */
   private def runLspServer(config: ViperConfig)(implicit executor: VerificationExecutionContext): Unit = {
+    var serverOpt: Option[ViperServerService] = None
     try {
       val done = startServer(config)
         .flatMap { case (serverSocket, server) =>
+          serverOpt = Some(server)
           val url = serverSocket.getInetAddress.getHostAddress
           val port = serverSocket.getLocalPort
           val serverUrl = s"$url:$port"
           announcePort(port)
-          println(s"going to listen on port $port for LSP")
+          server.globalLogger.info(s"going to listen on port $port for LSP")
           processRequests(config, serverSocket, server, serverUrl)
         }
 
       // wait until server is done:
       Await.result(done, Duration.Inf)
-      println("all clients have been processed")
+      serverOpt.foreach(_.globalLogger.info("all clients have been processed"))
       executor.terminate()
-      println("executor service has been shut down")
+      serverOpt.foreach(_.globalLogger.info("executor service has been shut down"))
       System.exit(0)
     } catch {
       case e: IOException =>
-        println(s"IOException occurred: ${e.toString}")
+        // Logger may not exist yet if startup itself failed; use stderr.
+        System.err.println(s"IOException occurred: ${e.toString}")
         System.exit(1)
     }
   }
@@ -87,9 +91,8 @@ object ViperServerRunner {
   }
 
   private def announcePort(port: Int): Unit = {
-    // write port number in a predefined format to standard output such that clients can parse it
-    // do not change this format without adapting clients such as the Viper-IDE client
-    // regex for parsing: "<ViperServerPort:(\d+)>"
+    // Machine-parsed contract — must stay on stdout in this exact format.
+    // Clients (e.g. Viper-IDE) match the regex "<ViperServerPort:(\d+)>".
     println(s"<ViperServerPort:$port>")
   }
 
@@ -110,14 +113,14 @@ object ViperServerRunner {
     * The returned future completes when stream is closed.
     */
   private def handleClient(config: ViperConfig, server: ViperServerService, socket: Socket, serverUrl: String)(implicit executor: VerificationExecutionContext): Future[Unit] = {
-    println(s"client connected: ${socket.toString}")
+    server.globalLogger.info(s"client connected: ${socket.toString}")
     val receiver: CustomReceiver = new CustomReceiver(config, server, serverUrl)
     val launcher = createLauncher(receiver, socket)(executor)
     receiver.connect(launcher.getRemoteProxy)
     // convert Java Future to Scala Future:
     Future {
       launcher.startListening().get()
-      println(s"client disconnected: ${socket.toString}")
+      server.globalLogger.info(s"client disconnected: ${socket.toString}")
       receiver.disconnected()
       socket.close()
     }

src/main/scala/viper/server/core/AstWorker.scala

@@ -34,7 +34,7 @@ class AstWorker(val file: String,
 
   private def constructAst(args: Seq[String]): Option[Program] = {
 
-    val reporter = new ActorReporter("AstGenerationReporter")
+    val reporter = new StreamingReporter("AstGenerationReporter")
     val astGen = new ViperAstGenerator(logger, reporter, args, disablePlugins = config.disablePlugins())
 
     val ast_option: Option[Program] = try {

src/main/scala/viper/server/core/MessageReportingTask.scala

@@ -6,30 +6,23 @@
 
 package viper.server.core
 
-import ch.qos.logback.classic.Logger
 import viper.server.vsi.MessageStreamingTask
-import viper.silver.reporter.{Entity, EntityFailureMessage, EntitySuccessMessage, Message, PluginAwareReporter, Time, VerificationResultMessage}
-import viper.silver.verifier.{Success, VerificationResult}
+import viper.silver.reporter.{EntityFailureMessage, EntitySuccessMessage, Message, PluginAwareReporter}
 
 trait MessageReportingTask[T] extends MessageStreamingTask[T] with ViperPost {
 
   def executor: VerificationExecutionContext
-  def logger: Logger
 
   protected def enqueueMessage(msg: Message): Unit = {
-    super.enqueueMessage(pack(msg), logger)
-  }
-
-  protected def registerTaskEnd(success: Boolean): Unit = {
-    super.registerTaskEnd(success, logger)
+    super.enqueueMessage(pack(msg))
   }
 
   // Implementation of the Reporter interface used by the backend.
-  class ActorReporter(tag: String) extends PluginAwareReporter {
+  class StreamingReporter(tag: String) extends PluginAwareReporter {
     val name = s"ViperServer_$tag"
 
     def doReport(msg: Message): Unit = {
-      logger.trace(s"ActorReport received msg $msg")
+      logger.trace(s"StreamingReporter received msg $msg")
       msg match {
         case m: EntityFailureMessage if m.concerning.info.isCached =>
         case m: EntitySuccessMessage if m.concerning.info.isCached =>

src/main/scala/viper/server/core/VerificationExecutionContext.scala

@@ -6,45 +6,33 @@
 
 package viper.server.core
 
-import java.util.concurrent.{ExecutorService, Executors, ThreadFactory, TimeUnit}
+import java.util.concurrent.{ExecutorService, Executors, ScheduledExecutorService, ThreadFactory, TimeUnit}
 import java.util.{concurrent => java_concurrent}
 
-import akka.actor.ActorSystem
-
-import scala.concurrent.duration.FiniteDuration
-import scala.concurrent.{Await, ExecutionContext, ExecutionContextExecutorService, Future}
+import scala.concurrent.{ExecutionContext, ExecutionContextExecutorService}
 
 trait VerificationExecutionContext extends ExecutionContext {
   def executorService: ExecutorService
-  def actorSystem: ActorSystem
+  def scheduler: ScheduledExecutorService
   def submit(r: Runnable): java_concurrent.Future[_]
-  /** terminate executor and actor system */
+  /** Terminate executor and scheduler. */
   def terminate(timeoutMSec: Long = 1000): Unit
-  /** restart actor system */
-  def restart(): Future[Unit]
 }
 
 object DefaultVerificationExecutionContext {
-  // at least 3 threads seem to be needed if the actor system is also using the same thread pool. Otherwise, if the actor
-  // system is started using its own (default) executor, a different number of thread might be sufficient.
-  // actor system with the default executor like `ActorSystem(actorSystemName)`)
-  /** minimum number of threads needed for the thread pool in the DefaultVerificationExecutionContext */
+  /** Minimum number of threads needed for the thread pool. */
   val minNumberOfThreads: Int = 3
 }
 
 /**
-  * This class provides a default verification execution context based on a fixed thread pool. The actor system is
-  * not using that thread pool but is using akka's default executor. (There have been issues starting the (default)
-  * akka logger in the unit tests because of some blocking behavior of the thread pool when sharing the same thread
-  * pool.)
-  * The thread pool uses as many threads as there are processors available (but at least 2). Each started thread
-  * gets a stack of 128MB.
-  * The purpose of a verification execution context is that it can be passed to ViperServer and ViperServer will
-  * use the provided verification execution context whenever an actor or any task requiring a separate thread is
-  * executed.
+  * Default verification execution context backed by a fixed thread pool.
+  *
+  * The pool uses as many threads as there are processors available (but at
+  * least 2). Each started thread gets a stack of 128MB. A separate
+  * single-threaded daemon `ScheduledExecutorService` handles delayed
+  * callbacks (used to be Akka schedulers).
   */
-class DefaultVerificationExecutionContext(actorSystemName: String = "Actor_System",
-                                          threadNamePrefix: String = "thread",
+class DefaultVerificationExecutionContext(threadNamePrefix: String = "thread",
                                           threadPoolSize: Option[Int] = None) extends VerificationExecutionContext {
   protected lazy val nThreads: Int = threadPoolSize.getOrElse(
     Math.max(DefaultVerificationExecutionContext.minNumberOfThreads, Runtime.getRuntime.availableProcessors()))
@@ -62,33 +50,28 @@ class DefaultVerificationExecutionContext(actorSystemName: String = "Actor_Syste
     })
   override def executorService: ExecutorService = service
 
+  private lazy val schedulerService: ScheduledExecutorService = Executors.newSingleThreadScheduledExecutor(new ThreadFactory {
+    private val mCount = new java.util.concurrent.atomic.AtomicInteger(1)
+    override def newThread(runnable: Runnable): Thread = {
+      val t = new Thread(runnable, s"$threadNamePrefix-scheduler-${mCount.getAndIncrement()}")
+      t.setDaemon(true)
+      t
+    }
+  })
+  override def scheduler: ScheduledExecutorService = schedulerService
+
   private lazy val context: ExecutionContextExecutorService = ExecutionContext.fromExecutorService(executorService)
 
   override def execute(runnable: Runnable): Unit = context.execute(runnable)
 
   override def reportFailure(cause: Throwable): Unit = context.reportFailure(cause)
 
-  private var system: Option[ActorSystem] = Some(ActorSystem(actorSystemName))
-  override def actorSystem: ActorSystem = system.getOrElse(throw new IllegalStateException(s"actor system has been terminated"))
-
   override def submit(r: Runnable): java_concurrent.Future[_] = context.submit(r)
 
   @throws(classOf[InterruptedException])
   override def terminate(timeoutMSec: Long = 1000): Unit = {
-    val oldSystem = actorSystem
-    system = None
-    Await.ready(oldSystem.terminate(), FiniteDuration(timeoutMSec, TimeUnit.MILLISECONDS))
+    schedulerService.shutdownNow()
     executorService.shutdown()
     executorService.awaitTermination(timeoutMSec, TimeUnit.MILLISECONDS)
   }
-
-  override def restart(): Future[Unit] = {
-    // the executor service stays untouched, i.e. only the actor system is restarted
-    val oldSystem = actorSystem
-    system = None
-    oldSystem.terminate().map(_ => {
-      // set new actor system:
-      system = Some(ActorSystem(actorSystemName))
-    })(this)
-  }
 }

src/main/scala/viper/server/core/VerificationWorker.scala

@@ -65,17 +65,17 @@ class VerificationWorker(private val command: List[String],
       command match {
         case "silicon" :: args =>
           logger.info("Creating new Silicon verification backend.")
-          backend = new ViperBackend("silicon", new SiliconFrontend(new ActorReporter("silicon"), logger), programId, program, disablePlugins = config.disablePlugins())
+          backend = new ViperBackend("silicon", new SiliconFrontend(new StreamingReporter("silicon"), logger), programId, program, disablePlugins = config.disablePlugins())
           backend.execute(args)
           success = true
         case "carbon" :: args =>
           logger.info("Creating new Carbon verification backend.")
-          backend = new ViperBackend("carbon", new CarbonFrontend(new ActorReporter("carbon"), logger), programId, program, disablePlugins = config.disablePlugins())
+          backend = new ViperBackend("carbon", new CarbonFrontend(new StreamingReporter("carbon"), logger), programId, program, disablePlugins = config.disablePlugins())
           backend.execute(args)
           success = true
         case "custom" :: custom :: args =>
           logger.info(s"Creating new verification backend based on class $custom.")
-          backend = new ViperBackend(custom, resolveCustomBackend(custom, new ActorReporter(custom)).get, programId, program, disablePlugins = config.disablePlugins())
+          backend = new ViperBackend(custom, resolveCustomBackend(custom, new StreamingReporter(custom)).get, programId, program, disablePlugins = config.disablePlugins())
           backend.execute(args)
           success = true
         case args =>