Fix regression #1072 - parse output file not being created #1073
Conversation
shonfeder
force-pushed
the
shon/fix-1072
branch
from
1ad3af1 to
4f45551
Compare
Additionally: - Fix output CLI parser to parse an optional value rather than just a string - Fix TlaWriterFactory to support writing to given PrintWriters, and not just locations inside of the output dir
shonfeder
force-pushed
the
shon/fix-1072
branch
from
8d4fab0 to
75f2ef0
Compare
| $ apalache-mc check --out-dir=./test-out-dir --length=0 Counter.tla &> /dev/null && find ./test-out-dir -type f -exec basename {} \; | ./sort.sh | ||
| $ apalache-mc check --out-dir=./test-out-dir --length=0 Counter.tla | sed 's/[IEW]@.*//' && find ./test-out-dir -type f -exec basename {} \; | ./sort.sh | ||
| ... | ||
| EXITCODE: OK |
There was a problem hiding this comment.
These changes just let us get more helpful feedback when the outputs fail due to a crash or something.
shonfeder
changed the title
shonfeder
requested review from
Kukovec and
konnov
and removed request for
Kukovec
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: Igor Konnov <igor@informal.systems>
| val dirName = intermediateDirPathOpt.getOrElse("") | ||
| logger.error( | ||
| s"Unable to find or create intermediate output directory ${dirName}. Intermediate output will not be written.") | ||
| false | ||
| } |
There was a problem hiding this comment.
@konnov I've opted for logging an error rather than crashing in the event of failure. The rationale being that if you're in the middle of a long running checking session, you may not want to lose all your progress and results just because this file cannot be created for some reason.
Does that seem sensible, or should it rather raise an exception?
It just occurs to me, it would be better if we just ensure all the directories needed for the configured output exist at startup, then error out early if they don't. However, I think that reworking of the initialization of the OutputManager is probably out of scope for this PR, and should instead be included in #1069. How does that sound?
There was a problem hiding this comment.
I think it's a good compromise.
Followup to #1073 That fix introduced *another* regression test, which caused the of the parser to always go to TLA. :(
* Fix output format detection Followup to #1073 That fix introduced *another* regression test, which caused the of the parser to always go to TLA. :( * Add regression test This way if I break the output detection again, I'll know it before merging :)
Closes #1072
Follow up to #1025, which caused a regression in the handling of the
--outputflag. Instead of writing the specified file, as it used (and as it seems it should), it was only writing to theintermediatesubdirectory of the run directory, and then only when the--write-intermediateflag was also given.This restores the previous behavior. I think the guiding principle for this kind of UI decision re: output files might be something like:
This PR also introduces a few utilities to the OutputManager to support the fix.
make fmt-fix(or had formatting run automatically on all files edited)