[BUG] cli parse command output is written to intermediate directory but not copied to output directory

[danwt]

Appears in APALACHE version 0.17.0 build f62f370

Description

The command apalache-mc parse --output=<filename> <tlafile> does not actually write the output to $filename in the output directory. In fact, it actually writes the output to the intermediate directory, which is only visible if passing --write-intermediate.

The command line parameters used to run the tool

apalache-mc parse --output=<filename> <tlafile>

Expected behavior

A file should be created in the output directory.

Log files

System information

• Apalache version [apalache-mc version]: APALACHE version 0.17.0 build f62f370
• OS [e.g. Ubuntu Linux or Mac OS, and the current version]: OSX 11.5
• JDK version [e.g. OpenJDK 0.8.0]: OpenJDK Runtime Environment Zulu16.32+15-CA (build 16.0.2+7)

Additional context

Reproduce with file main.tla

------------------------------------ MODULE main -----------------------------

\* @type: () => Bool;
Init ==
    /\ TRUE

Next == TRUE

===============================================================================

tree 3
.
├── apalache-pkg-0.17.0-full.jar
└── main.tla

java -jar apalache-pkg-0.17.0-full.jar parse --output=foobar.tla main.tla

tree 3
.
├── _apalache-out
│  └── main.tla_2021-11-03T19-20-28_10048578539153344840
│     ├── detailed.log
│     └── run.txt
├── apalache-pkg-0.17.0-full.jar
└── main.tla


java -jar apalache-pkg-0.17.0-full.jar --write-intermediate=true parse --output=foobar.tla main.tla

tree 4

.
├── _apalache-out
│  └── main.tla_2021-11-03T19-22-08_5579138356771785926
│     ├── detailed.log
│     ├── intermediate
│     │  ├── 00_OutParser.json
│     │  ├── 00_OutParser.tla
│     │  └── foobar.tla
│     └── run.txt
├── apalache-pkg-0.17.0-full.jar
└── main.tla

[shonfeder]

If I'm not mistaken, this is all by design, following #1025.

[shonfeder]

I did not mean to close this, especially not with such a curt message. Sorry!

To elaborate, iiuc:

• The parse output files are intermediate files.
• Those are only generated now when --write-intermediate is passed.
• All intermediate files are now written to the intermediate sub directory.

However, I think the documentation did not get updated to reflect the conditional generation of the output file, and I could see an argument that parse should imply that this intermediate output is meant to be created. However, I'm kind if inclined to the other side of argument. The parse subcommand is useful to check syntactic correctness (this is the main use it is documented as serving), and for specialist usage where one wants to consume the intermediate output, I think it's reasonable to provide a flag.

This is just my preliminary analysis tho, I don't have strong feelings here.

Would be good to get more feedback from @danwt and @Kukovec.

[danwt]

* The parse output files are intermediate files.

* Those are only generated now when `--write-intermediate` is passed.

* All intermediate files are now written to the `intermediate` sub directory.

Ah ok so it's true parse is mainly used internally but it is also exposed in the cli as a useful piece of functionality in of itself, so in that usage scenario it should probably be written to the output directory. Especially since the --output argument is given.

[shonfeder]

Ah! I'm sorry! I misread! I read output as the new out-dir flag. I don't think this is by design at all, and it does seem like a new bug. Clearly the output flag is meant to specify the output file. My bad!