This is the next version of the TLA proof manager, which is part of the TLA+ Tools [1]. Since is still under development, please also refer to the current version[2].
[1] https://github.com/tlaplus/tlaplus
[2] https://tlaps.codeplex.com
The easiest way to install is via opam:
opam pin add tlapm2 https://github.com/tlaplus/v2-tlapm.git
If it is already pinned but not installed a simple
opam install tlapm2
will suffice.
The compilation requirements are:
- a recent version of ocaml (at least 4.02)
- xmlm (http://erratique.ch/software/xmlm)
- kaputt (http://kaputt.x9c.fr)
- oasis (http://oasis.forge.ocamlcore.org)
- result (if you are running ocaml < 4.03 )
- sexplib
The easiest way to install them is via opam (https://opam.ocaml.org):
opam install oasis xmlm kaputt result sexplib
To initialize the configuration, call
oasis setup ;
./configure --enable-tests --enable-debug
in the v2-tlapm base directory. For the actual compilation, the usual
make
will compile the project, wheras
make test
will run the test suite.
For execution, a Java Runtime Environment (at least 7) is also necessary.