Closed Isaac-DeFrain closed 3 years ago
I suspect that there is a problem with permissions. Definitely, the tool should write what went wrong.
Oh, that's hilarious. It throws an exception when the directory $HOME/.tlaplus
does not exist :-)
What's also hilarious is that we independently discovered and fixed the same bug in TLC/Toolbox: https://github.com/tlaplus/tlaplus/commit/227f515065425752ec36f9f9b3285b95d1b19dbf
That's amazing! I wanted to open a PR in tlaplus but gave up on running the tests for the whole thing :-)
In our case, if you never ran Toolbox (which is not the case for most of us), then apalache would have crashed as in the bug report.
That's amazing! I wanted to open a PR in tlaplus but gave up on running the tests for the whole thing :-)
$ ant -f tlatools/org.lamport.tlatools/customBuild.xml
for TLC and $ mvn clean verify
for the Toolbox+TLC should "just work".
True. It is even written in DEVELOPING.md
. I just typed mvn test
in the root directory, and that was a wrong move.
Description
I have statistics reporting enabled in the toolbox and would like to enable statistics for Apalache, but I keep getting an exception in thread "main" java.io.IOException: No such file or directory.
Input specification
N/A
The command line parameters used to run the tool
apalache config --enable-stats=true
Expected behavior
Statistics are enabled.
Log files
System information
apalache-mc version
]: 0.15.4-SNAPSHOT build v0.15.3-15-g8c71e2c