tlaplus
Consider bundling CommunityModules.jar as part of a TLC release
https://github.com/dgpv/bip32_template_parse_tplaplus_spec/issues/1 shows that users are reluctant to adopt CM because it adds an additional dependency. Thus, we should consider bundling/shipping a snapshot of CM with new TLC releases.
Requirements:
- Don't blur the lines between CM and the TLA+ standard modules (Specifying Systems)
- Override bundled CM with a newer release
Although copy&paste usually works for TLA+ definitions and thus doesn't create an additional dependency, this is not true for Java module overrides. Since one of the main value propositions of CM is module overrides, the general idea of bundling CM with the TLA+ tools received a blessing during today's conf call. However, it implies that we are more careful/conservative with adding new modules to CM and should always consider if https://github.com/tlaplus/examples is a more appropriate home.
Another idea: Instead of bundling CM with tla2tools.jar, tla2tools.jar could have a command to automatically fetch (a particular) version of CM from the web.
Simply dropping CommunityModules.jar (timestamp suffix stripped) into the toolbox directory makes sure that TLC loads the modules and overrides.
Questions:
- What is the lookup order if multiple copies of CommunityModules.jar appear on the Java classpath?
- Does this work from inside the Toolbox?
https://github.com/tlaplus/tlaplus/issues/490 (https://github.com/tlaplus/tlaplus/pull/493) would make it easy for users to load CommunityModules.jar system-wide (although TLA_PATH would have to be added to the classpath too for module overrides to work).
@lemmy We already have a Json module with no license problem, what did you plan as next steps? Are we bundling Community Modules to TLC release using CommunityModule-deps.jar or something else?
We will just move TLCExt and Json to TLC. The other modules will remain in the CommunityModules.