diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 4d9ead0317..293e10232b 100644 --- a/.github/workflows/main.yml +++ b/.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 diff --git a/Dockerfile b/Dockerfile index 564f0b771b..00af678993 100644 --- a/Dockerfile +++ b/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"] diff --git a/UNRELEASED.md b/UNRELEASED.md index 1042c6253e..ed42379639 100644 --- a/UNRELEASED.md +++ b/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 diff --git a/bin/run-in-docker-container b/bin/run-in-docker-container index 41a2a793aa..4e777cc8e1 100755 --- a/bin/run-in-docker-container +++ b/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 $@ diff --git a/docs/src/apalache/config.md b/docs/src/apalache/config.md index 4ce1067b65..71ca9ba8d2 100644 --- a/docs/src/apalache/config.md +++ b/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: `_yyyy-MM-dd_HH-mm-ss_`. 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: + `_yyyy-MM-dd_HH-mm-ss_`. 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. diff --git a/docs/src/apalache/running.md b/docs/src/apalache/running.md index e8dea15553..21ff4335f2 100644 --- a/docs/src/apalache/running.md +++ b/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)] \ .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 ` instructs the search to stop after `n` errors, see [Enumeration of counterexamples][]. Default: 1. + - `--max-error ` instructs the search to stop after `n` errors, see [Enumeration of counterexamples][]. Default: 1. - `--view ` sets the state view to ``, 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. diff --git a/flake.lock b/flake.lock index ee4a901dd8..722e88613b 100644 --- a/flake.lock +++ b/flake.lock @@ -2,11 +2,11 @@ "nodes": { "flake-utils": { "locked": { - "lastModified": 1631561581, - "narHash": "sha256-3VQMV5zvxaVLvqqUrNz3iJelLw30mIVSfZmAaauM3dA=", + "lastModified": 1634851050, + "narHash": "sha256-N83GlSGPJJdcqhUxSCS/WwW5pksYf3VP1M13cDRTSVA=", "owner": "numtide", "repo": "flake-utils", - "rev": "7e5bf3925f6fbdfaf50a2a7ca0be2879c4261d19", + "rev": "c91f3de5adaf1de973b797ef7485e441a65b8935", "type": "github" }, "original": { @@ -17,11 +17,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1633329294, - "narHash": "sha256-0LpQLS4KMgxslMgmDHmxG/5twFlXDBW9z4Or1iOrCvU=", + "lastModified": 1635295995, + "narHash": "sha256-sGYiXjFlxTTMNb4NSkgvX+knOOTipE6gqwPUQpxNF+c=", "owner": "nixos", "repo": "nixpkgs", - "rev": "ee084c02040e864eeeb4cf4f8538d92f7c675671", + "rev": "22a500a3f87bbce73bd8d777ef920b43a636f018", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 3943775c40..73dac443c5 100644 --- a/flake.nix +++ b/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 ''; diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala index 2391025b18..9652560d7b 100644 --- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala +++ b/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) diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala index fdf1351144..580efd575a 100644 --- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala +++ b/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: .cfg, or none if .cfg not present") diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/General.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/General.scala index 3432bca6c5..a301792b0a 100644 --- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/General.scala +++ b/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 = "" diff --git a/script/run-docker.sh b/script/run-docker.sh index aaae99c03d..eaabb53902 100755 --- a/script/run-docker.sh +++ b/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 diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md index 14760e23c9..bdc0b2e210 100644 --- a/test/tla/cli-integration-tests.md +++ b/test/tla/cli-integration-tests.md @@ -1992,3 +1992,75 @@ Statistics collection is ON. ... EXITCODE: OK ``` + +## configuring the output manager + +### set out-dir by CLI flag + +```sh +$ apalache-mc check --out-dir=./test-out-dir --length=0 Counter.tla &> /dev/null && find ./test-out-dir -type f -exec basename {} \; | ./sort.sh +detailed.log +log0.smt +run.txt +$ rm -rf ./test-out-dir +``` + +### set out-dir by envvar + +```sh +$ OUT_DIR=./test-out-dir apalache-mc check --length=0 Counter.tla &> /dev/null && find ./test-out-dir -type f -exec basename {} \; | ./sort.sh +detailed.log +log0.smt +run.txt +$ rm -rf ./test-out-dir +``` + +### setting out-dir by CLI flag overrides the envvar + +```sh +$ OUT_DIR=./not-here apalache-mc check --out-dir=./test-out-dir --length=0 Counter.tla &> /dev/null && find ./test-out-dir -type f -exec basename {} \; | ./sort.sh +detailed.log +log0.smt +run.txt +$ rm -rf ./test-out-dir +``` + +### write-intermediate files + +```sh +$ apalache-mc check --out-dir=./test-out-dir --write-intermediate=true --length=0 Counter.tla &> /dev/null && find ./test-out-dir -type f -exec basename {} \; | ./sort.sh +00_OutParser.json +00_OutParser.tla +01_out-post-TypeCheckerSnowcat.json +01_out-pre-TypeCheckerSnowcat.json +01_OutTypeCheckerSnowcat.json +01_OutTypeCheckerSnowcat.tla +02_OutConfig.json +02_OutConfig.tla +03_OutDesugarer.json +03_OutDesugarer.tla +04_OutUnroll.json +04_OutUnroll.tla +05_OutInline.json +05_OutInline.tla +06_OutPriming.json +06_OutPriming.tla +07_OutVCGen.json +07_OutVCGen.tla +08_OutPrepro.json +08_OutPrepro.tla +09_OutTransition.json +09_OutTransition.tla +10_OutOpt.json +10_OutOpt.tla +11_OutAnalysis.json +11_OutAnalysis.tla +12_out-post-PostTypeCheckerSnowcat.json +12_OutPostTypeCheckerSnowcat.json +12_OutPostTypeCheckerSnowcat.tla +12_out-pre-PostTypeCheckerSnowcat.json +detailed.log +log0.smt +run.txt +$ rm -rf ./test-out-dir +``` diff --git a/test/tla/sort.sh b/test/tla/sort.sh new file mode 100755 index 0000000000..130e863213 --- /dev/null +++ b/test/tla/sort.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash +# +# This script aims for a stable sorting accross *nix systems +# see `man sort` for information on the options. + +set -euf -o pipefail + +export LC_ALL=C + +sort --ignore-case --stable --dictionary-order diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/OutputManager.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/OutputManager.scala index 0f40987586..5045bdf657 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/io/OutputManager.scala +++ b/tla-io/src/main/scala/at/forsyte/apalache/io/OutputManager.scala @@ -1,6 +1,6 @@ package at.forsyte.apalache.io -import at.forsyte.apalache.infra.passes.PassOptions +import at.forsyte.apalache.infra.passes.WriteablePassOptions import java.io.{File, FileInputStream} import java.nio.file.{Files, Path, Paths} @@ -8,6 +8,12 @@ import java.time.LocalDateTime import java.time.format.DateTimeFormatter import org.yaml.snakeyaml.Yaml +trait OutputManagerConfig { + // TODO def debug : Boolean + def outDir: Option[File] + def writeIntermediate: Option[Boolean] +} + /** * The OutputManager is the central source of truth, for all IO related locations. * Any IO operation should request read/write target paths from this object. @@ -24,8 +30,9 @@ object OutputManager { val RunFile = "run.txt" } import Names._ - // Absolute path - private var outputDirPath: String = "" + + // outDirOpt is stored as an expanded and absolute path + private var outDirOpt: Option[Path] = None private var runDirOpt: Option[Path] = None private var flags: Map[String, Boolean] = Map( @@ -34,13 +41,38 @@ object OutputManager { ) /** If this is FALSE, outputs (of any sort) cannot happen, so the tool should exit */ - def isConfigured: Boolean = new File(outputDirPath).isDirectory + def isConfigured: Boolean = outDirOpt.nonEmpty /** Accessor, read-only */ def runDirPathOpt: Option[Path] = runDirOpt + /** + * Accessor for the configured run directory. + * + * @throws IllegalStateException if called before OutputManager is configured this is considered an implementator error + */ + def outDir: Path = { + outDirOpt.getOrElse(throw new IllegalStateException("out-dir is not configured")) + } + + private def createOutDir(): Unit = { + val f = outDir.toFile() + if (!f.exists() && !f.mkdirs()) { + throw new ConfigurationError(s"Could not find or create directory: ${f.getCanonicalPath}.") + } else if (!f.isDirectory()) { + throw new ConfigurationError(s"Configured out-dir is not a directory: ${f.getCanonicalPath}.") + } else { + outDirOpt = Some(f.toPath().toAbsolutePath()) + } + } + + private def expandedFilePath(s: String): Path = { + val home = System.getProperty("user.home") + Paths.get(if (s.startsWith("~")) s.replaceFirst("~", home) else s) + } + /** Loads the Apalache configuration file from HOME/.tlaplus */ - def syncFromGlobalConfig(): Unit = { + private def syncFromGlobalConfig(): Unit = { val home = System.getProperty("user.home") val configFile = new File(home, CfgFile) if (configFile.exists()) { @@ -48,23 +80,10 @@ object OutputManager { val configYaml: java.util.Map[String, Any] = yaml.load(new FileInputStream(configFile.getCanonicalPath)) configYaml.forEach { case (flagName, flagValue) => + // `OutdirNameInCfg` is a special flag that governs the output directory if (flagName == OutdirNameInCfg) { flagValue match { - case flagValAsString: String => - // `OutdirNameInCfg` is a special flag that governs the output directory - val replacedHome = - if (flagValAsString.startsWith("~")) flagValAsString.replaceFirst("~", home) - else flagValAsString - val outdir = new File(replacedHome) - // Try to make the dir, if it fails we skip and go to the default - if (!outdir.exists()) { - outdir.mkdir() - } - if (!outdir.exists()) { - throw new ConfigurationError(s"Could not find or create directory: ${outdir.getCanonicalPath}.") - } else { - outputDirPath = outdir.getCanonicalPath - } + case path: String => outDirOpt = Some(expandedFilePath(path)) case _ => throw new ConfigurationError( s"Flag [$flagName] in [${configFile.getAbsolutePath}] must be a directory path string.") @@ -86,20 +105,42 @@ object OutputManager { } } // If `OutdirNameInCfg` is not specified, default to making rundir = /_apalache-out/ - if (outputDirPath.isEmpty) { - outputDirPath = Paths.get(System.getProperty("user.dir"), DefaultOutdir).toString + if (outDirOpt.isEmpty) { + outDirOpt = Some(Paths.get(System.getProperty("user.dir"), DefaultOutdir)) } } + /** Configure OutputManager based on supported CLI flags */ + // TODO(shon): Perhaps we should reworking this object as a class that takes a configuration + // matching the specification of this trait? + private def syncFromCli(cli: OutputManagerConfig): Unit = { + cli.outDir.foreach(d => outDirOpt = Some(d.toPath())) + cli.writeIntermediate.foreach(flags += IntermediateFlag -> _) + } + + /** + * Configure OutputManager, with cli configuration taking precedence + * over the configuration file + */ + def configure(cli: OutputManagerConfig): Unit = { + syncFromGlobalConfig() + syncFromCli(cli) + createOutDir() + } + // Flags can be passed from options too, e.g. --profile or --write-intermediate + // Strangly, we currently require data to flow both from the pass options + // to the output manager and from the manager to the pass options, this this "sync" + // is by directional. // TODO: remove this once all flag operations are moved into PassOptions - def syncFromOptions(opt: PassOptions): Unit = { + def syncWithOptions(opt: WriteablePassOptions): Unit = { opt.get[Boolean]("general", IntermediateFlag) foreach { flags += IntermediateFlag -> _ } opt.get[Boolean]("general", ProfilingFlag) foreach { flags += ProfilingFlag -> _ } + opt.set("io.outdir", outDir) } /** lends flags to execute `cmd` conditionally */ @@ -113,17 +154,13 @@ object OutputManager { } ) - /** Inside `outputDirPath`, create a directory for an individual run */ + /** Inside `outputDirOpt`, create a directory for an individual run */ def createRunDirectory(specName: String): Unit = if (runDirOpt.isEmpty) { val nicedate = LocalDateTime.now().format(DateTimeFormatter.ofPattern(s"yyyy-MM-dd")) val nicetime = LocalDateTime.now().format(DateTimeFormatter.ofPattern(s"HH-mm-ss")) - val outdir = new File(outputDirPath) - if (!outdir.exists()) { - outdir.mkdir() - } // prefix for disambiguation - val rundir = Files.createTempDirectory(Paths.get(outdir.getAbsolutePath), s"${specName}_${nicedate}T${nicetime}_") + val rundir = Files.createTempDirectory(outDir, s"${specName}_${nicedate}T${nicetime}_") runDirOpt = Some(rundir) } }