Publish nightly builds

[alygin]

In order to give users early access to new features and bug fixes, it would be nice to have nightly builds and publish them as a separate "TLA+ Nightly" extension.

[lemmy]

From personal experience, it would be convenient to always include the most recent TLC build--even better if a TLC build would trigger a nightly build here (like the eclipse toolbox gets build along with TLC).

Also, there are approximately 400 installs of this extension on the openvsx marketplace. Not sure if this justifies nightly builds on that marketplace. However, openvsx is where gitpod gets extension from.

[alygin]

But that means we also have to commit new tla2tools.jar to the extension repository every night automatically. Which means we'll always publish extension with the most recent, the least tested version of the TLA+ tools. That doesn't feel right.

I much more like the idea to allow the user to choose the tools channel (stable or nightly) in settings. In this case the extension is always published with a stable tla2tools.jar (or at least with something that has been tested for some reasonable time, and not just compiled several hours before the release), but the user can switch to the nightly at their own risk.

[lemmy]

Independently of this discussion, I'd suggest removing tla2tools.jar from the repository strategically. The jar file is > 2MB now, and we've wanted to do more frequent TLC releases anyway. Also, the fast-changing CommunityModules should ideally be bundled with the extension (the Eclipse Toolbox already contains the latest release).

Letting users choose channels sounds like overhead, assuming that users who download a nightly VScode extension are also likely to want the most recent build of TLC. Secondly, it causes extra work on our end to support the last released TLC and its nightly build. For example, integrating the TLA+ debugger into the extension would have required branching on the TLC version. A tighter integration between the VSCode extension and TLC would also allow pushing features into TLC, which wasn't done with the Eclipse Toolbox and turned out to be a big mistake.

If we settle for stable and nightly channels, choosing the channel ideally is configurable through .devcontainer/devcontainer.json or .vscode/settings.json, which would be important in the context of Gitpod and Codespaces (think tutorials).