[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Docker image with TLA+ tools



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.