-
Notifications
You must be signed in to change notification settings - Fork 21
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
snapshot of the TLAPM sources just before release 1.4.4
- Loading branch information
0 parents
commit c9f82ae
Showing
1,001 changed files
with
203,768 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,21 @@ | ||
*.o | ||
*.cmi | ||
*.cmx | ||
*.annot | ||
*.exe | ||
*.err | ||
*.out | ||
*.toolbox | ||
*.tlaps | ||
*.log | ||
|
||
/Makefile | ||
/config.log | ||
/config.status | ||
/src/alexer.ml | ||
/src/config.ml | ||
/src/load.ml | ||
/src/tlapm.native | ||
/tools/installer/tlaps-release.sh | ||
/tools/installer/tlaps-source-release.sh | ||
tlapm |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,20 @@ | ||
S src | ||
S src/frontend | ||
S src/util | ||
S src/expr | ||
S src/smt | ||
S src/typesystem | ||
S src/pars | ||
S src/module | ||
S src/backend | ||
S src/proof | ||
|
||
B src | ||
B src/frontend | ||
B src/util | ||
B src/expr | ||
B src/smt | ||
B src/typesystem | ||
B src/pars | ||
B src/module | ||
B src/backend |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,82 @@ | ||
Installing the TLA+ Proof Manager (tlapm) | ||
========================================= | ||
|
||
Copyright (C) 2008-2010 INRIA and Microsoft Corporation | ||
|
||
0. Dependencies | ||
--------------- | ||
|
||
- A UNIX-like system. The following are known to work: | ||
|
||
* Any modern UNIX | ||
* Cygwin under Windows | ||
* OS X | ||
|
||
- Objective Caml (OCaml) version 3.10.2 or later. | ||
|
||
Try one of the following: | ||
|
||
a. Use a precompiled binary package for your operating system. | ||
|
||
b. Build it from the official source. | ||
|
||
c. Use GODI: http://godi.camlcity.org/godi/index.html | ||
|
||
d. On most modern Linux distributions, OCaml is already packaged. | ||
Here are the commands for some of the more popular Linux | ||
distributions: | ||
|
||
Debian and Ubuntu: | ||
apt-get install ocaml | ||
Redhat, Mandriva, and SuSE: | ||
yum install ocaml | ||
Gentoo: | ||
emerge ocaml | ||
Arch Linux: | ||
pacman install ocaml | ||
|
||
- Zenon. See instructions in zenon/INSTALL | ||
|
||
- Isabelle/TLA+. See instructions in TLA+/INSTALL | ||
|
||
|
||
1. Installation | ||
--------------- | ||
|
||
A standard 'configure' script is provided to generate a Makefile. Run | ||
it as: | ||
|
||
% ./configure | ||
|
||
This will install tlapm in the default local install directory on your | ||
operating system, usually /usr/local. This directory is represented | ||
by ${prefix}. | ||
|
||
If you want to install it to a different location, such as ${HOME}, | ||
run 'configure' as follows: | ||
|
||
% ./configure --prefix=${HOME} | ||
|
||
If you want to install it in-place, run: | ||
|
||
% ./configure --prefix=`pwd` | ||
|
||
(Remember to add `pwd`/bin to your $PATH.) | ||
|
||
If 'configure' completes successfully, then run: | ||
|
||
% make all install | ||
|
||
This will build the PM, copy the binary 'tlapm' (or 'tlapm.exe') to | ||
${prefix}/bin, and copy some program data to ${prefix}/share/tlaps. | ||
|
||
|
||
2. Uninstallation | ||
----------------- | ||
|
||
To uninstall 'tlapm', run: | ||
|
||
% make uninstall | ||
|
||
This will remove the 'tlapm' binary from ${prefix}/bin and any data | ||
belonging to tlapm from ${prefix}/share/tlaps. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,26 @@ | ||
Copyright (c) 2008-2013 INRIA and Microsoft Corporation | ||
All rights reserved. | ||
|
||
Redistribution and use in source and binary forms, with or without | ||
modification, are permitted provided that the following conditions are | ||
met: | ||
|
||
* Redistributions of source code must retain the above copyright | ||
notice, this list of conditions and the following disclaimer. | ||
|
||
* Redistributions in binary form must reproduce the above copyright | ||
notice, this list of conditions and the following disclaimer in | ||
the documentation and/or other materials provided with the | ||
distribution. | ||
|
||
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS | ||
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT | ||
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR | ||
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT | ||
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, | ||
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT | ||
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, | ||
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY | ||
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT | ||
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE | ||
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,28 @@ | ||
The TLA+ Proof Manager (tlapm) | ||
============================== | ||
|
||
Copyright (C) 2008-2013 INRIA and Microsoft Corporation | ||
|
||
Authors: Kaustuv Chaudhuri | ||
Denis Cousineau | ||
Damien Doligez | ||
Leslie Lamport | ||
Tomer Libal | ||
Stephan Merz | ||
Jean-Baptiste Tristan | ||
Hernan Vanzetto | ||
|
||
License: 2-clause BSD, portions under LGPL2.1+LE | ||
(see LICENSE for details) | ||
|
||
1. Installation | ||
--------------- | ||
|
||
For installation instructions, see the file INSTALL in this directory. | ||
|
||
|
||
2. Use | ||
------ | ||
|
||
Some user documentation is in the form of HTML files in the directory | ||
doc/web. Start with doc/web/index.html. |
Oops, something went wrong.