Skip to content
The rewrite of TLAPM, the TLAPS proof manager
OCaml TLA Other
Branch: master
Clone or download
quicquid Merge pull request #25 from gliptak/patch-1
Add current OCaml versions to Travis
Latest commit 8cc7103 Jul 23, 2019
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
bugreports added library and examples to tlaps v2 Jan 8, 2015
docs added semantics if parameterized instantiation to doc Nov 21, 2017
examples git reset Mar 22, 2016
jenkins added jenkins script for building the project in continuous integration Jun 10, 2015
lib adjusted sany parser and ds to accomodate the source link for instant… Nov 21, 2017
library added setting for pm path Jul 20, 2016
nunchaku adapted nunchaku backend to newer version of nunchaku (subset is now … Feb 28, 2017
spec spec started Aug 6, 2014
src Add current OCaml versions to Travis Jul 16, 2019
test pass over Martin's test cases Apr 20, 2018
.merlin in the middle of adapting to the new xml schema - does not compile Apr 7, 2017
.ocamlinit added alias module for expressions Oct 5, 2017
.travis.yml Add current OCaml versions to Travis Jul 16, 2019
LICENSE remove licenses of software which is only part of the the binary dist… Dec 12, 2017
Makefile Added the Makefile since only there it is possible to supress warnings Oct 15, 2014
README.md changed tla tools location in readme Dec 6, 2017
_oasis adding more source files to documentation list Sep 5, 2017
_tags adding more source files to documentation list Sep 5, 2017
configure added configuration files Oct 19, 2014
generate_test_cases.sh moving test directories, commenting simple expression conversion out … Jul 21, 2016
opam Add current OCaml versions to Travis Jul 16, 2019
run-test.sh fixed accumulator bug in expr_simple Apr 7, 2016
setup.ml adding more source files to documentation list Sep 5, 2017
tla2xml.sh simple expressions Mar 29, 2016
tlapm added tlapm shell script Jul 22, 2016

README.md

TLAPM

Build Status

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

Installation

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.

Compilation

The compilation requirements are:

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.

Running

For execution, a Java Runtime Environment (at least 7) is also necessary.

You can’t perform that action at this time.