Stephan Merz

No, Isabelle/TLA+ doesn't rely on Java, but it may well be that the Isabelle binary checks if Java is present and doesn't start otherwise.

Before I get too much credit for the idea, the change was suggested by @kape1395 with the objective to ultimately reduce the number of global variables. As @glondu says, the...

My guess would be that the `translate' utility (related to the LS4 decision procedure for propositional temporal logic) might originally have been under LGPL, but the README says that the...

Thanks for reporting this. IMHO, it would indeed be better to remove this syntax from the language, as well as the similar "BY MODULE" construct. These constructs look like a...

I'm not sure what you mean by "steps" here. TLA+ proofs explicitly list all user-level steps, but each of those "steps" relies on a check by the back-end provers, and...

Back to the original question, note that TLAPM has the option ``--stretch`` that allows one to multiply all timeouts by some factor. That is a crude mechanism to account for...

Thanks for checking the proofs in the examples repository. I fixed most of the broken proofs, except for the ones in LamportMutex_proofs that I'm still working on: we had to...

For older versions of tlapm, fingerprints are stored at /path/to/module/module.tlaps/fingerprints More recent versions store them at /path/to/module/.tlacache/module.tlaps/fingerprints I don't think there is a command line option to change these paths...

I believe that all proofs now work again. Thanks for uncovering these issues!

Thanks for adding this! See above for two minor remarks on comments in the TLA module. Also, the module should be added to the manifest for the CI to succeed.