Run TLA+ consensus/consistency from vscode

[heidihoward]

At the moment, users cannot run the TLA+ specs in codespaces out of the box due to the shared StatsFile.tla. It would be great if we could support this, we have at least three options:

• Remove StatsFile.tla as this was mostly used for cimetrics
• Duplicate StatsFile.tla between the consensus and consistency directories
• (If possible) Modify the devcontainer settings so the TLA+ vscode plugin knows to look in /tla for the modules

We would also need to add tlc2.tool.impl.Tool.cdot=true to the devcontainer

[lemmy]

At the moment, users cannot run the TLA+ specs in codespaces out of the box due to the shared StatsFile.tla. It would be great if we could support this, we have at least three options:

• Remove StatsFile.tla as this was mostly used for cimetrics
• Duplicate StatsFile.tla between the consensus and consistency directories
• (If possible) Modify the devcontainer settings so the TLA+ vscode plugin knows to look in /tla for the modules

The module StatsFile does not seem to be a dependency of the consistency spec anymore.

We would also need to add tlc2.tool.impl.Tool.cdot=true to the devcontainer

I recommend rewriting ccfraft without using cdot, as the incomplete implementation of cdot may lead to subtle issues under (non-trivial) refinement:

CCF/tla/consensus/ccfraft.tla

Lines 1101 to 1102 in 3cf06af

	\/ ConflictAppendEntriesRequest(i, index, m) \cdot AppendEntriesAlreadyDone(i, j, index, m)
	\/ ConflictAppendEntriesRequest(i, index, m) \cdot NoConflictAppendEntriesRequest(i, j, m)

[achamayou]

@heidihoward is this still an issue with StatsFile.tla gone?

In general, it's relatively straightforward to guarantee that things we run in the CI are reproducible by users (modulo unfortunately the stuff that requires Azure resources like the SNP tests): they can pull the image and run the same commands. Checking that something works in VS Code is not something we can practically check in CI, as far as I can tell.

[heidihoward]

There's now a new challenge as the environment variables introduced last week need to be set

[achamayou]

@heidihoward they don't need to, need to, because the current behaviour is to set defaults if they're missing. It'd be nice to be able to provide them through VS Code, I agree, which sounds like a feature request for the extension maybe?

[achamayou]

The invocation seems to set the environment, to provide cwd, but allows no other env var customisation: https://github.com/tlaplus/vscode-tlaplus/blob/35a53385b33c5374100e7c1bce10a9b8ead8ca59/src/tla2tools.ts#L157

[heidihoward]

Just testing and it does work now (for default env vars)