Refactor OutputManager

mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala

@@ -56,9 +56,8 @@ object Tool extends LazyLogging {
     }
     _ <- Try(OutputManager.configure(initialization))
   } yield {
-    initialization.source.foreach(OutputManager.initSourceLines)
     println(s"Output directory: ${OutputManager.runDir.normalize()}")
-    OutputManager.withWriterInRunDir(OutputManager.Names.RunFile)(
+    OutputManager.withWriterInRunDir(OutputManager.RunFile)(
         _.println(s"${cmd.env} ${cmd.label} ${cmd.invocation}")
     )
 
@@ -70,7 +69,7 @@ object Tool extends LazyLogging {
     }
 
     // force our programmatic logback configuration, as the autoconfiguration works unpredictably
-    new LogbackConfigurator(OutputManager.runDirPathOpt, OutputManager.customRunDirPathOpt).configureDefaultContext()
+    new LogbackConfigurator(Some(OutputManager.runDir), OutputManager.additionalRunDir).configureDefaultContext()
     // TODO: update workers when the multicore branch is integrated
     logger.info(s"# APALACHE version: ${BuildInfo.version} | build: ${BuildInfo.build}")
 
@@ -164,7 +163,7 @@ object Tool extends LazyLogging {
   }
 
   // Execute the program specified by the subcommand cmd, handling errors as needed
-  private def runCommand(cmd: ApalacheCommand, config: ApalacheConfig): ExitCodes.TExitCode =
+  private def runCommand(cmd: ApalacheCommand, config: ApalacheConfig): ExitCodes.TExitCode = {
     try {
       cmd.run(config) match {
         case Left((errorCode, failMsg)) => { logger.info(failMsg); errorCode }
@@ -174,7 +173,9 @@ object Tool extends LazyLogging {
       case e: AdaptedException =>
         e.err match {
           case NormalErrorMessage(text) => logger.error(text)
-          case FailureMessage(text)     => { logger.error(text, e); generateBugReport(e, cmd) }
+          case FailureMessage(text)     =>
+            logger.error(text, e)
+            generateBugReport(e, cmd, config.source.flatMap(_.readUtf8.value))
         }
         ExitCodes.ERROR
 
@@ -185,9 +186,10 @@ object Tool extends LazyLogging {
 
       case e: Throwable =>
         logger.error("Unhandled exception", e)
-        generateBugReport(e, cmd)
+        generateBugReport(e, cmd, config.source.flatMap(_.readUtf8.value))
         ExitCodes.ERROR
     }
+  }
 
   private def printTimeDiff(startTime: LocalDateTime): Unit = {
     val endTime = LocalDateTime.now()
@@ -242,8 +244,9 @@ object Tool extends LazyLogging {
     }
   }
 
-  private def generateBugReport(e: Throwable, cmd: ApalacheCommand): Unit = {
+  private def generateBugReport(e: Throwable, cmd: ApalacheCommand, sourceText: Option[String]): Unit = {
     val absPath = ReportGenerator.prepareReportFile(
+        sourceText,
         cmd.invocation.split(" ").dropRight(1).mkString(" "),
         s"${BuildInfo.version} build ${BuildInfo.build}",
     )

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/TranspileCmd.scala

@@ -12,11 +12,7 @@ class TranspileCmd extends AbstractCheckerCmd(name = TRANSPILE, description = "T
 
   override def run(config: ApalacheConfig): Either[(TExitCode, String), String] = {
     runWithOptions(ApalacheConfigResolver.resolveCheck(config)) { options =>
-      val outFilePath = OutputManager.runDirPathOpt
-        .map { p =>
-          p.resolve(TlaExToVMTWriter.outFileName).toAbsolutePath
-        }
-        .getOrElse(TlaExToVMTWriter.outFileName)
+      val outFilePath = OutputManager.pathInRunDir(TlaExToVMTWriter.outFileName).toAbsolutePath
 
       PassChainExecutor(new ReTLAToVMTModule(options)).run() match {
         case Right(_)      => Right(s"VMT constraints successfully generated at\n$outFilePath")

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rewriter/MetricProfilerListener.scala

@@ -66,7 +66,7 @@ class MetricProfilerListener(sourceStore: SourceStore, changeListener: ChangeLis
 
     logger
       .info("%d profile entries to be found in %s".format(sortedEntries.size,
-              OutputManager.runDir.resolve(profileFileName)))
+              OutputManager.pathInRunDir(profileFileName)))
   }
 
   private def stringOfEntry(entry: (UID, SolverContextMetrics)): String = {

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Cvc5SolverContext.scala

@@ -221,12 +221,7 @@ class Cvc5SolverContext(val config: SolverConfig) extends SolverContext with Laz
 
   private def initLogs(): Iterable[PrintWriter] = {
     val filePart = s"log$id.smt"
-    val writers =
-      if (OutputManager.isBound) {
-        (OutputManager.runDirPathOpt ++ OutputManager.customRunDirPathOpt).map(OutputManager.printWriter(_, filePart))
-      } else {
-        Iterable.empty
-      }
+    val writers = OutputManager.openLongLivedWritersInRunDirs(filePart)
 
     if (!config.debug) {
       writers.foreach { writer =>

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala

@@ -428,12 +428,7 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL
    */
   private def initLogs(): Iterable[PrintWriter] = {
     val filePart = s"log$id.smt"
-    val writers =
-      if (OutputManager.isBound) {
-        (OutputManager.runDirPathOpt ++ OutputManager.customRunDirPathOpt).map(OutputManager.printWriter(_, filePart))
-      } else {
-        Iterable.empty
-      }
+    val writers = OutputManager.openLongLivedWritersInRunDirs(filePart)
 
     if (!config.debug) {
       writers.foreach { writer =>