Add --profiling flag

UNRELEASED.md

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

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

@@ -140,7 +140,16 @@ object Tool extends LazyLogging {
   private def setCommonOptions(cli: General, options: WriteablePassOptions): Unit = {
     options.set("general.debug", cli.debug)
     options.set("smt.prof", cli.smtprof)
-    OutputManager.syncWithOptions(options)
+    // TODO Do we actual need this in the "pass options"? It seems like it is only
+    // derived from the OutputManager?
+    OutputManager.doIfFlag(OutputManager.Names.IntermediateFlag) {
+      options.set(s"general.${OutputManager.Names.IntermediateFlag}", true)
+    }
+    OutputManager.doIfFlag(OutputManager.Names.ProfilingFlag) {
+      options.set(s"general.${OutputManager.Names.ProfilingFlag}", true)
+    }
+    options.set("io.outdir", OutputManager.outDir)
+    // OutputManager.syncWithOptions(options)
   }
 
   private def runParse(injector: => Injector, parse: ParseCmd): Int = {

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

@@ -16,6 +16,10 @@ import at.forsyte.apalache.io.OutputManager
 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 profiling = opt[Option[Boolean]](name = OutputManager.Names.ProfilingFlag,
+      description =
+        s"write general profiling data to profile-rules.txt in the run directory, default: false (overrides envvar PROFILING)",
+      useEnv = true)
   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)

test/tla/cli-integration-tests.md

@@ -2064,3 +2064,10 @@ log0.smt
 run.txt
 $ rm -rf ./test-out-dir
 ```
+
+### use the --profiling flag to write profile-rules.txt
+
+```sh
+$ apalache-mc check --out-dir=./test-out-dir --profiling=true --length=0 Counter.tla &> /dev/null && test -s ./test-out-dir/*/profile-rules.txt
+$ rm -rf ./test-out-dir
+```

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

@@ -12,6 +12,7 @@ trait OutputManagerConfig {
   // TODO def debug : Boolean
   def outDir: Option[File]
   def writeIntermediate: Option[Boolean]
+  def profiling: Option[Boolean]
 }
 
 /**
@@ -116,6 +117,7 @@ object OutputManager {
   private def syncFromCli(cli: OutputManagerConfig): Unit = {
     cli.outDir.foreach(d => outDirOpt = Some(d.toPath()))
     cli.writeIntermediate.foreach(flags += IntermediateFlag -> _)
+    cli.profiling.foreach(flags += ProfilingFlag -> _)
   }
 
   /**
@@ -128,21 +130,6 @@ object OutputManager {
     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 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 */
   // TODO: remove this once all flag operations are moved into PassOptions
   def doIfFlag(flagName: String)(cmd: => Unit): Unit =