OutputManager for files produced by Apalache #1036
Conversation
tla-io/src/main/scala/at/forsyte/apalache/io/OutputManager.scala
Outdated
Show resolved
Hide resolved
tla-io/src/main/scala/at/forsyte/apalache/io/OutputManager.scala
Outdated
Show resolved
Hide resolved
tla-io/src/main/scala/at/forsyte/apalache/io/OutputManager.scala
Outdated
Show resolved
Hide resolved
tla-io/src/main/scala/at/forsyte/apalache/io/OutputManager.scala
Outdated
Show resolved
Hide resolved
Co-authored-by: Shon Feder <shon@informal.systems>
Co-authored-by: Shon Feder <shon@informal.systems>
Co-authored-by: Shon Feder <shon@informal.systems>
There was a problem hiding this comment.
It's definitely a good improvement over the chaos that we currently have about files and directories. Since we are refactoring now, shall we make one more step to make code nice:
- introduce a trait that gives us the output manager and configuration options
- this would require minor refactoring of
PassOptions(renaming?).
docs/src/apalache/config.md
Outdated
| - `OUTDIR`: The value of `OUTDIR` defines a directory, in which all Apalache runs write their outputs. Each run will produce a unique subdirectory inside `OUTDIR` using the following convention: `<SPECNAME>_yyyy-MM-dd_HH-mm-ss_<UNIQUEID>`. | ||
| Example value: `~/apalache-out`. | ||
| If this value is not defined in `apalache.cfg`, Apalache will, for each individual run, define it to be equal to `DIR/x/`, where `DIR` is the directory containing the specification. | ||
| - `profiling`: This Boolean flag has to be one of `TRUE/true/FALSE/false` and governs the creation of `profile-rules.txt` used in [profiling](profiling.md). The file is only created if `profiling` is set to `TRUE/true`. Setting `profiling=false` is incompatible with the `--smtprof` flag. |
There was a problem hiding this comment.
Can we avoid these TRUE/true/FALSE/false and use a standard parser for configuration files? Either Java properties file or YAML. I am not fan of yaml, but hand-written configs are even less fun.
There was a problem hiding this comment.
Yes, like I said in a previous answer, this was just the fastest way to get the proof-of-concept prototype working, without committing too much.
| TLA IR. | ||
| - File `out-parser.json` is produced as a result of converting the Apalache TLA IR representation of the input into JSON | ||
| format. | ||
| - File `out-config.tla` is produced as a result of substituting CONSTANTS, as described |
There was a problem hiding this comment.
What happened tou out-parser.json? The MBT team has asked for it.
There was a problem hiding this comment.
- The text above says "each pass of the model checker produces an intermediate TLA+ file in the run-specific
directory" - ALL of the files listed here have
.jsoncounterparts.
There was a problem hiding this comment.
Also, 3) Rodrigo renamed all these files, so their names are out of sync, but that's a TODO for later
| def syncFromCFG(): Unit = { | ||
| val flagRegex = raw"^\s*([a-zA-Z\-]+)\s*=\s*(.+)\s*$$".r | ||
| val home = System.getProperty("user.home") | ||
| val configFile = new File(home, CFG_FILE) | ||
| if (configFile.exists()) { | ||
| val src = Source.fromFile(configFile.getAbsolutePath) | ||
| for (line <- src.getLines) { | ||
| flagRegex.findAllMatchIn(line).foreach { m => | ||
| // Flags have the shape FLAGNAME=FLAGVAL | ||
| val flagname = m.group(1) | ||
| val flagVal = m.group(2) | ||
| if (flagname == OUTDIR_NAME_IN_CFG) { |
There was a problem hiding this comment.
This is a prototype, so I just wanted a quick-and-dirty txt file to read
Let's not do that. There are tonnes of libraries around in the Java/Scala world. We do not want to do IO ourselves, unless we really badly need to do that.
| if (flagVal.startsWith("~")) flagVal.replaceFirst("~", home) | ||
| else flagVal |
There was a problem hiding this comment.
I don't know whether standard libraries like Apache Commons Configuration would be able to handle ~, perhaps, they would work with environment variables like $HOME. In any case, we should never implement this kind of things, unless we have a really good reason to do it. Check Apache Commons Configuration, or google for a YAML parser.
tla-io/src/main/scala/at/forsyte/apalache/io/OutputManager.scala
Outdated
Show resolved
Hide resolved
tla-io/src/main/scala/at/forsyte/apalache/io/OutputManager.scala
Outdated
Show resolved
Hide resolved
|
Manual changes are in #1025. This branch merges into the ADR one, not unstable directly. |
* Outputs ADR * tweaks * Apply suggestions from code review Co-authored-by: Igor Konnov <igor@informal.systems> * tweaks * tweaks * OutputManager for files produced by Apalache (#1036) * OutputManager * logs * comments * removed unnecessary file * tweaks for logless runs * string.strip nonsense * docs * Update docs/src/apalache/config.md Co-authored-by: Shon Feder <shon@informal.systems> * Update docs/src/apalache/config.md Co-authored-by: Shon Feder <shon@informal.systems> * Update docs/src/apalache/config.md Co-authored-by: Shon Feder <shon@informal.systems> * v2, with YAML * md * run.txt Co-authored-by: Shon Feder <shon@informal.systems> * unreleased * fmt Co-authored-by: Igor Konnov <igor@informal.systems> Co-authored-by: Shon Feder <shon@informal.systems>
Tests added for any new codemake fmt-fix(or had formatting run automatically on all files edited)Entry added to UNRELEASED.md for any new functionalityPrototype implementation, following #1025.
Closes #977