I'd like to run the TLA+ tools in CI. I thought it would be useful to have a Docker image with the tools already installed for that.
I've made an attempt here: https://github.com/talex5/tla
It works for my use (I'm experimenting with making a TLA+ spec for SwarmKit:
https://github.com/docker/swarmkit/pull/2613), but I'm not convinced it's installed quite correctly. In particular, if I use `tlapm -C` then I get:
Unknown logic "TLA+" -- no heap file found in:
/root/.isabelle/Isabelle2011-1/heaps/polyml-5.4.0_x86_64-linux
/opt/Isabelle/heaps/polyml-5.4.0_x86_64-linux
The -C option doesn't seem to be needed (my "proofs" are very trivial), but if someone knows how to fix that, please let me know. The install script I'm using is at
https://github.com/talex5/tla/blob/master/Dockerfile.