Expose output configuration via CLI arguments (#1062)

* Fix documentation to indicate the correct config file

* Expose output configuration via CLI arguments

- Followup to #1025
- Required for #1059

This plumbs configuration of the OutputManager's settings
for the out-dir and write-intermediate fields through to the CLI.

It's is needed for us to control the location and kind of output for the
benchmark tests, and was planned in #1025

* Rework docker wrapper scripts to create files using the same user and group ID of the user who invoked the script, fixing incorrect file permissions on files generated within the docker container.

.github/workflows/main.yml

@@ -143,9 +143,10 @@ jobs:
       - name: Build dev-shell
         run: nix develop -c bash -c exit
       - name: Build the docker image
-        run: docker build -t informalsystems/apalache:ci .
+        run: docker build -t ghcr.io/informalsystems/apalache:ci .
       - name: Run integration tests in docker container
-        run: nix develop -c bash -c "source ./test/.envrc && make integration"
+        run: |
+          nix develop -c bash -c "source ./test/.envrc && test/mdx-test.py --debug"
         env:
           USE_DOCKER: true
           APALACHE_TAG: ci

Dockerfile

@@ -63,5 +63,8 @@ ENV PATH="/usr/local/openjdk-16/bin/:/opt/apalache/bin:${PATH}"
 # In case the directory was not bind-mounted, we create one
 RUN mkdir /var/apalache 2>/dev/null
 
+# We need sudo to run apalache using the user (created in the entrypoint script)
+RUN apt update && apt install sudo
+
 # what to run
 ENTRYPOINT ["/opt/apalache/bin/run-in-docker-container"]

UNRELEASED.md

@@ -13,4 +13,4 @@
 ### Features
 
  * Add smt-encoding option to CLI check command, see #1053
- * Added outputs ADR and assoicated `OutputManager`, see #1025, #1036
+ * Added outputs ADR and associated `OutputManager`, see #1025, #1036, #1062

bin/run-in-docker-container

@@ -3,10 +3,34 @@
 # This script is used as the entrypoint for running apalache inside of the
 # docker container defined in ../Dockerfile
 
+# Create a user and group matching the invoking user, this is a
+# doppelganger of the user running the container, if they have passed
+# in the required environment variables
+#
+# This is critical to avoid generating files with bad permissions
+USER_ID=${USER_ID:-1000}
+GROUP_ID=${GROUP_ID:-1000}
+groupadd --gid "$GROUP_ID" --non-unique apalache
+useradd --create-home --shell /bin/bash --uid "$USER_ID" --non-unique --gid "$GROUP_ID" apalache
+
 echo 'Assuming you bind-mounted your local directory into /var/apalache...'
 cd /var/apalache
 if [ "$(ls -A *.tla 2>/dev/null)" == "" ]; then
       echo 'WARNING: no .tla files found in /var/apalache'
 fi
-exec /opt/apalache/bin/apalache-mc $@
 
+# Run apalache as the invoking user doppelganger
+# We need to also thread the environment along to the doppelganger
+# NOTE:
+#  - Invoking sudo with `--preserve-env` works for all envvars **except** the PATH
+#  - Unless we explicitly give it `=PATH`
+#  - We need to `--set-home`, so it doesn't inherent the home of the root user
+#  - Finally, we need to invoke our command with `env` to get the environment propagated
+#    to the apalache invocation itself
+exec sudo \
+      --preserve-env \
+      --preserve-env=PATH \
+      --set-home \
+      --user=apalache \
+      env \
+      /opt/apalache/bin/apalache-mc $@

docs/src/apalache/config.md

@@ -2,7 +2,11 @@
 Apalache allows you to specify certain parameters, governing outputs produced by it, as described in [ADR-009](../adr/009adr-outputs.md).
 
 You can create a global configuration file named `apalache-global-config.yml` in `$HOME/.tlaplus/` and populate it with values for the following flags, in YAML format:
-  - `out-dir` (String): The value of `out-dir` defines a path to the directory, in which all Apalache runs write their outputs. Each run will produce a unique subdirectory inside `out-dir` using the following convention: `<SPECNAME>_yyyy-MM-dd_HH-mm-ss_<UNIQUEID>`. The use of `~` in the path specification is permitted. The directory need not already exist, however, its parent directory must.
+  - `out-dir` (String): The value of `out-dir` defines a path to the directory,
+  in which all Apalache runs write their outputs. Each run will produce a unique
+  subdirectory inside `out-dir` using the following convention:
+  `<SPECNAME>_yyyy-MM-dd_HH-mm-ss_<UNIQUEID>`. The use of `~` in the path
+  specification is permitted. The directory path need not already exist.
   Example value: `'~/apalache-out'`.
   If this value is not defined in `apalache-global-config.yml`, Apalache will, for each individual run, define it to be equal to `CWD/_apalache-out/`, where `CWD` is the current working directory.
   - `profiling` (Bool): This flag governs the creation of `profile-rules.txt` used in [profiling](profiling.md). The file is only created if `profiling` is set to `True`.  Setting `profiling` to `False` is incompatible with the `--smtprof` flag.

docs/src/apalache/running.md

@@ -13,6 +13,8 @@ $ apalache check [--config=filename] [--init=Init] [--cinit=ConstInit] \
     [--next=Next] [--inv=Inv] [--length=10] [--algo=(incremental|offline)] \
     [--discard-disabled] [--no-deadlock] [--tuning=filename] [--tune-here=options] \
     [--smt-encoding=(oopsla19|arrays)] \
+    [--out-dir=./path/to/dir] \
+    [--write-intermediate=(true|false)] \
     <myspec>.tla
 ```
 
@@ -36,13 +38,17 @@ The arguments are as follows:
     - `--discard-disabled` does a pre-check on transitions and discard the disabled ones at every step. If you know that
       many transitions are always enabled, set it to false. Sometimes, this pre-check may be slower than checking the
       invariant. Default: true.
-    - `--max-error <n>` instructs the search to stop after `n` errors, see [Enumeration of counterexamples][]. Default: 1.  
+    - `--max-error <n>` instructs the search to stop after `n` errors, see [Enumeration of counterexamples][]. Default: 1.
     - `--view <name>` sets the state view to `<name>`, see [Enumeration of counterexamples][].
     - `--no-deadlock` disables deadlock-checking, when `--discard-disabled=false` is on. When `--discard-disabled=true`,
       deadlocks are found in any case.
     - `--tuning` specifies the properties file that stores the options for
       [fine tuning](tuning.md)
-    - `--tuning-options=key1=val1:key2=val2:...` pass the tuning options right in the command line as a single string.
+    - `--out-dir` set location for outputting any generated logs or artifacts,
+      *`./_apalache-out` by default*
+    - `--write-intermediate` if `true`, then additional output is generated. See
+      [Detailed output](#detailed-output). *`false` by default*
+
       The options that are passed with the option `--tuning-options`
       have priority over the options that are passed with the option `--tuning`.
 
@@ -52,8 +58,8 @@ the command line, the command line parameters take precedence over those in the
 In case conflicting arguments are passed for the same parameter, the following precedence order is followed:
 
 1. Command-line value
-2. Configuration file value
-3. Environment variable value
+2. Environment variable value
+3. Configuration file value
 
 ### Supplying JVM arguments
 
@@ -236,8 +242,10 @@ the [TLA+ Community Modules](https://github.com/tlaplus/CommunityModules).
 
 The tool will display only important messages on stdout, but a detailed log can be found in `detailed.log`.
 
-Additionally, if enabled in `apalache.cfg` (see [configuration instructions](config.md)) each pass of the model checker produces an intermediate TLA+ file in the run-specific
-directory:
+Additionally, if the flag `--write-intermediate=true` is set or this option is
+enabled in the `apalache-global-config.yml` (see [configuration
+instructions](config.md)) each pass of the model checker produces an
+intermediate TLA+ file in the run-specific directory:
 
 - File `out-parser.tla` is produced as a result of parsing and importing into the intermediate representation, Apalache
   TLA IR.

flake.nix

@@ -46,6 +46,10 @@
               shellHook = ''
                 # Add common project environment variables
                 source ./.envrc
+
+                # Required to avoid polluting the dev-shell's ocaml environment with
+                # dynamically liked libs from the host environment
+                unset CAML_LD_LIBRARY_PATH
               '';
 
 

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

@@ -23,6 +23,7 @@ import util.ExecutionStatisticsCollector.Selection
 
 import scala.collection.JavaConverters._
 import scala.util.Random
+import at.forsyte.apalache.infra.passes.WriteablePassOptions
 
 /**
  * Command line access to the APALACHE tools.
@@ -51,21 +52,19 @@ object Tool extends LazyLogging {
     System.exit(exitcode)
   }
 
-  def mkRunFile(cmd: General): Unit = OutputManager.runDirPathOpt.foreach { runDir =>
-    println(s"Output directory: ${runDir.toFile}")
-    val outFile = new File(runDir.toFile, OutputManager.Names.RunFile)
-    val writer = new PrintWriter(new FileWriter(outFile, false))
-    try {
-      writer.println(s"${cmd.env} ${cmd.label} ${cmd.invocation}")
-    } finally {
-      writer.close()
-    }
-  }
-
   private def outputAndLogConfig(runDirNamePrefix: String, cmd: General): Unit = {
-    OutputManager.syncFromGlobalConfig()
+    OutputManager.configure(cmd)
     OutputManager.createRunDirectory(runDirNamePrefix)
-    mkRunFile(cmd)
+    OutputManager.runDirPathOpt.foreach { runDir =>
+      println(s"Output directory: ${runDir.toFile}")
+      val outFile = new File(runDir.toFile, OutputManager.Names.RunFile)
+      val writer = new PrintWriter(new FileWriter(outFile, false))
+      try {
+        writer.println(s"${cmd.env} ${cmd.label} ${cmd.invocation}")
+      } finally {
+        writer.close()
+      }
+    }
     // force our programmatic logback configuration, as the autoconfiguration works unpredictably
     new LogbackConfigurator(OutputManager.runDirPathOpt).configureDefaultContext()
     // TODO: update workers when the multicore branch is integrated
@@ -137,6 +136,13 @@ object Tool extends LazyLogging {
           .format(ChronoUnit.SECONDS.between(startTime, endTime), ChronoUnit.MILLIS.between(startTime, endTime) % 1000))
   }
 
+  // Set the pass options from the cli configs shared between all commands
+  private def setCommonOptions(cli: General, options: WriteablePassOptions): Unit = {
+    options.set("general.debug", cli.debug)
+    options.set("smt.prof", cli.smtprof)
+    OutputManager.syncWithOptions(options)
+  }
+
   private def runParse(injector: => Injector, parse: ParseCmd): Int = {
     // here, we implement a terminal pass to get the parse results
     val executor = injector.getInstance(classOf[PassChainExecutor])
@@ -148,7 +154,10 @@ object Tool extends LazyLogging {
     executor.options.set("parser.filename", parse.file.getAbsolutePath)
     executor.options.set("parser.output", parse.output)
 
-    executor.options.set("io.outdir", createOutputDir(executor.options))
+    // NOTE Must go after all other options are set due to side-effecting
+    // behavior of current OutmputManager configuration
+    setCommonOptions(parse, executor.options)
+
     val result = executor.run()
     if (result.isDefined) {
       logger.info("Parsed successfully")
@@ -175,8 +184,6 @@ object Tool extends LazyLogging {
     logger.info("Tuning: " + tuning.toList.map { case (k, v) => s"$k=$v" }.mkString(":"))
 
     executor.options.set("general.tuning", tuning)
-    executor.options.set("general.debug", check.debug)
-    executor.options.set("smt.prof", check.smtprof)
     executor.options.set("parser.filename", check.file.getAbsolutePath)
     if (check.config != "")
       executor.options.set("checker.config", check.config)
@@ -199,7 +206,9 @@ object Tool extends LazyLogging {
       executor.options.set("checker.view", check.view)
     // for now, enable polymorphic types. We probably want to disable this option for the type checker
     executor.options.set("typechecker.inferPoly", true)
-    executor.options.set("io.outdir", createOutputDir(executor.options))
+    // NOTE Must go after all other options are set due to side-effecting
+    // behavior of current OutmputManager configuration
+    setCommonOptions(check, executor.options)
 
     val result = executor.run()
     if (result.isDefined) {
@@ -228,8 +237,6 @@ object Tool extends LazyLogging {
     logger.info("Tuning: " + tuning.toList.map { case (k, v) => s"$k=$v" }.mkString(":"))
 
     executor.options.set("general.tuning", tuning)
-    executor.options.set("general.debug", test.debug)
-    executor.options.set("smt.prof", test.smtprof)
     executor.options.set("parser.filename", test.file.getAbsolutePath)
     executor.options.set("checker.init", test.before)
     executor.options.set("checker.next", test.action)
@@ -247,7 +254,9 @@ object Tool extends LazyLogging {
     executor.options.set("checker.algo", "offline")
     // for now, enable polymorphic types. We probably want to disable this option for the type checker
     executor.options.set("typechecker.inferPoly", true)
-    executor.options.set("io.outdir", createOutputDir(executor.options))
+    // NOTE Must go after all other options are set due to side-effecting
+    // behavior of current OutmputManager configuration
+    setCommonOptions(test, executor.options)
 
     val result = executor.run()
     if (result.isDefined) {
@@ -269,7 +278,10 @@ object Tool extends LazyLogging {
     executor.options.set("parser.filename", typecheck.file.getAbsolutePath)
     executor.options.set("typechecker.inferPoly", typecheck.inferPoly)
 
-    executor.options.set("io.outdir", createOutputDir(executor.options))
+    // NOTE Must go after all other options are set due to side-effecting
+    // behavior of current OutmputManager configuration
+    setCommonOptions(typecheck, executor.options)
+
     executor.run() match {
       case None =>
         logger.info("Type checker [FAILED]")
@@ -322,11 +334,6 @@ object Tool extends LazyLogging {
     props ++ hereProps
   }
 
-  private def createOutputDir(options: PassOptions): Path = {
-    OutputManager.syncFromOptions(options)
-    OutputManager.runDirPathOpt.get
-  }
-
   private def injectorFactory(cmd: Command): Injector = {
     cmd match {
       case _: ParseCmd     => Guice.createInjector(new ParserModule)

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

@@ -17,7 +17,8 @@ class CheckCmd extends Command(name = "check", description = "Check a TLA+ speci
   var algo: String = opt[String](name = "algo", default = "incremental",
       description = "the search algorithm: offline, incremental, parallel (soon), default: incremental")
   var smtEncoding: Option[String] = opt[Option[String]](name = "smt-encoding", useEnv = true,
-      description = "the SMT encoding: oopsla19, arrays (experimental), default: oopsla19")
+      description =
+        "the SMT encoding: oopsla19, arrays (experimental), default: oopsla19 (overrides envvar SMT_ENCODING)")
   var config: String = opt[String](name = "config", default = "",
       description = "configuration file in TLC format,\n" +
         "default: <file>.cfg, or none if <file>.cfg not present")

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

@@ -1,6 +1,10 @@
 package at.forsyte.apalache.tla.tooling.opt
 
+import at.forsyte.apalache.io.{OutputManagerConfig, OutputManager}
+
+import java.io.File
 import org.backuity.clist._
+import at.forsyte.apalache.io.OutputManager
 
 /**
  * The general commands.
@@ -9,9 +13,16 @@ import org.backuity.clist._
  *
  * @author Igor Konnov
  */
-trait General extends Command {
+trait General extends Command with OutputManagerConfig {
   var debug = opt[Boolean](description = "extensive logging in detailed.log and log.smt, default: false")
   var smtprof = opt[Boolean](description = "profile SMT constraints in log.smt, default: false")
+  var outDir = opt[Option[File]](name = OutputManager.Names.OutdirNameInCfg,
+      description = "where output files will be written, default: ./_apalache-out (overrides envvar OUT_DIR)",
+      useEnv = true)
+  var writeIntermediate = opt[Option[Boolean]](name = OutputManager.Names.IntermediateFlag,
+      description =
+        "write intermediate output files to `out-dir`, default: false (overrides envvar WRITE_INTERMEDIATE)",
+      useEnv = true)
 
   private var _invocation = ""
   private var _env = ""

script/run-docker.sh

@@ -14,11 +14,18 @@ if [ -z "$APALACHE_TAG" ]
 then
     >&2 echo "# No docker image supplied. Defaulting to '$default_tag'"
     >&2 echo "# To run a specific docker tag set APALACHE_TAG."
-    img="informalsystems/apalache:${default_tag}"
+    img="ghcr.io/informalsystems/apalache:${default_tag}"
 else
-    img="informalsystems/apalache:${APALACHE_TAG}"
+    img="ghcr.io/informalsystems/apalache:${APALACHE_TAG}"
 fi
 
-cmd="docker run -e TLA_PATH -e JVM_ARGS --rm -v $(pwd):/var/apalache ${img} ${@}"
+# TODO Programmatically generate envars to expose here
+# We pass through the calling user id and group id to prevent
+# invalid user permissions on generated files
+cmd="docker run \
+    -e OUT_DIR -e WRITE_INTERMEDIATE -e SMT_ENCODING \
+    -e TLA_PATH -e JVM_ARGS \
+    -e USER_ID=$(id -u) -e GROUP_ID=$(id -g) \
+    --rm -v $(pwd):/var/apalache ${img} ${*}"
 >&2 echo "# running command: ${cmd}"
 $cmd