Merge pull request #2038 from informalsystems/1174/ApalacheConfigs-ar…

…e-options

Prepare the ApalacheConfig trait to communicate the override values of the options traits from `ApalacheCommand`

mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala

@@ -1,15 +1,27 @@
 package at.forsyte.apalache.infra.passes.options
 
-import at.forsyte.apalache.tla.lir.Feature
+// TODO: Use either File or Path consistently (preference for File)
+import java.io.File
 import java.nio.file.Path
+import at.forsyte.apalache.tla.lir.Feature
 
 /**
- * Collects the passoptions supported for configuring Apalache's various passes
+ * Collects the options supported for configuring Apalache's various modes of execution
  *
  * @author
  *   Shon Feder
  */
 
+/** The application's configurable values, along with their base defaults */
+case class ApalacheConfig(
+    file: Option[File] = None,
+    outDir: File = new File(System.getProperty("user.dir"), "_apalache-out"),
+    runDir: Option[File] = None,
+    configFile: Option[File] = None,
+    writeIntermediate: Boolean = false,
+    profiling: Boolean = false,
+    features: Seq[Feature] = Seq())
+
 /** Defines the data sources supported */
 sealed abstract class SourceOption
 

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

@@ -4,7 +4,7 @@ package at.forsyte.apalache.tla
 import apalache.BuildInfo
 import at.forsyte.apalache.infra._
 import at.forsyte.apalache.infra.log.LogbackConfigurator
-import at.forsyte.apalache.io.{ConfigManager, ConfigurationError, OutputManager, ReportGenerator}
+import at.forsyte.apalache.io.{ConfigurationError, OutputManager, ReportGenerator}
 import at.forsyte.apalache.tla.tooling.opt._
 import com.typesafe.scalalogging.LazyLogging
 import org.backuity.clist.Cli
@@ -48,7 +48,7 @@ object Tool extends LazyLogging {
 
   // Returns `Left(errmsg)` in case of configuration errors
   private def outputAndLogConfig(cmd: ApalacheCommand): Either[String, Unit] = {
-    ConfigManager(cmd).map { cfg =>
+    cmd.configuration.map { cfg =>
       try {
         OutputManager.configure(cfg)
       } catch {

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/General.scala → mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ApalacheCommand.scala

@@ -1,12 +1,14 @@
 package at.forsyte.apalache.tla.tooling.opt
 
+import at.forsyte.apalache.infra.ExitCodes
 import at.forsyte.apalache.io.CliConfig
 import at.forsyte.apalache.tla.lir.Feature
-import at.forsyte.apalache.infra.ExitCodes
 
 import java.io.File
 import org.backuity.clist._
 import org.backuity.clist.util.Read
+import at.forsyte.apalache.infra.passes.options.ApalacheConfig
+import at.forsyte.apalache.io.ConfigManager
 
 /**
  * The base class used by all Apalache CLI subcommands.
@@ -56,6 +58,7 @@ abstract class ApalacheCommand(name: String, description: String)
 
   private var _invocation = ""
   private var _env = ""
+  private var _configure: Either[String, ApalacheConfig] = Left("UNCONFIGURED")
 
   // A comma separated name of supported features
   private val featureList = Feature.all.map(_.name).mkString(", ")
@@ -84,6 +87,15 @@ abstract class ApalacheCommand(name: String, description: String)
   /** CLI options that are set through environment variables */
   def env: String = _env
 
+  /**
+   * The application configuration, derived by loading all configuration sources, concluding with the CLI options
+   *
+   * See [[at.forsyte.apalache.infra.passes.options.ApalacheConfig ApalacheConfig]] for details.
+   *
+   * TODO: Ultimately, we would like all application configuration to be derived from this value
+   */
+  def configuration = _configure
+
   override def read(args: List[String]) = {
     _env = super.options
       .filter(_.useEnv.getOrElse(false))
@@ -93,5 +105,8 @@ abstract class ApalacheCommand(name: String, description: String)
     _invocation = args.mkString(" ")
 
     super.read(args)
+
+    // This must be invoked after we parse the CLI args
+    _configure = ConfigManager(this)
   }
 }

tla-io/src/main/scala/at/forsyte/apalache/io/ConfigManager.scala

@@ -5,6 +5,7 @@ import pureconfig.generic.auto._
 import java.io.File
 import java.nio.file.{Files, Path, Paths}
 import at.forsyte.apalache.tla.lir.Feature
+import at.forsyte.apalache.infra.passes.options.ApalacheConfig
 
 // Provides implicit conversions used when deserializing into configurable values.
 private object Converters {
@@ -27,7 +28,8 @@ private object Converters {
 /**
  * The configuration values that can be overriden based on CLI arguments
  *
- * For documentation on the use and meaning of these fields, see `at.forsyte.apalache.tla.tooling.opt.General`.
+ * For documentation on the use and meaning of these fields as CLI paramter, see
+ * `at.forsyte.apalache.tla.tooling.opt.General`.
  */
 trait CliConfig {
 
@@ -41,16 +43,12 @@ trait CliConfig {
   def features: Seq[Feature]
 }
 
-/** The application's configurable values, along with their base defaults */
-case class ApalacheConfig(
-    file: Option[File] = None,
-    outDir: File = new File(System.getProperty("user.dir"), "_apalache-out"),
-    runDir: Option[File] = None,
-    configFile: Option[File] = None,
-    writeIntermediate: Boolean = false,
-    profiling: Boolean = false,
-    features: Seq[Feature] = Seq())
-
+/**
+ * Manage cascade loading program configurations from the supported sources
+ *
+ * @param cmd
+ *   The configurations supplied via CLI
+ */
 case class ConfigManager(cmd: CliConfig) {
   private val TLA_PLUS_DIR = ".tlaplus"
   private val APALACHE_CFG = "apalache.cfg"
@@ -75,10 +73,14 @@ case class ConfigManager(cmd: CliConfig) {
   /**
    * Load the application configuration from all sources supported by apalache
    *
-   * The following precedence is maintained, wherein lower numbered items override highest numbered items:
+   * The following precedence is maintained, wherein configured values found from lower numbered sources override values
+   * from higher numbered sources:
    *
-   *   1. CLI arguments 2. Environment variables (Overiding is taken care of by CLI parsing library) 3. Local config
-   *      file 4. Globacl config file 5. `ApalacheConfig` defaults (as specified in the case class definition)
+   *   1. CLI arguments
+   *   1. Environment variables (Overiding is taken care of by the CLI parsing library)
+   *   1. Local config file
+   *   1. Global config file
+   *   1. `ApalacheConfig` defaults (as specified in the case class definition)
    */
   def load(): ConfigReader.Result[ApalacheConfig] = {
 

tla-io/src/main/scala/at/forsyte/apalache/io/OutputManager.scala

@@ -6,6 +6,7 @@ import java.io.{File, FileWriter, PrintWriter}
 import java.nio.file.{Files, Path, Paths}
 import java.time.LocalDateTime
 import java.time.format.DateTimeFormatter
+import at.forsyte.apalache.infra.passes.options.ApalacheConfig
 
 import scala.io.Source