Skip to content

Commit

Permalink
Merge pull request #125 from tlaplus/docs-install
Browse files Browse the repository at this point in the history 
Update the installation instructions.
  • Loading branch information
@kape1395
kape1395 authored May 5, 2024
2 parents 5ef530f + ed54ce0 commit 8facb9a
Show file tree
Hide file tree
Showing 6 changed files with 35 additions and 225 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ jobs:
strategy:
fail-fast: false
matrix:
os: [ubuntu-latest, macos-latest]
os: [ubuntu-latest, macos-13]
ocaml-compiler: ['0', '1']
env:
EXAMPLES_DIR: "tlaplus-examples"
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/release.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ jobs:
strategy:
matrix:
operating-system: [
macos-latest,
macos-13,
ubuntu-latest]
ocaml-compiler: [
'2',
Expand Down
8 changes: 4 additions & 4 deletions doc/web/content/Download/Binaries/Linux.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,25 +21,25 @@ <h2><img class="blogo" src="images/logo_linux35.png"
alt="[Tux]"/>Linux</h2>
<p class="first"> The package:
<code><a type="application/x-executable"
href="https://github.com/tlaplus/tlapm/releases/latest/download/tlaps-1.4.5-x86_64-linux-gnu-inst.bin">tlaps-1.4.5-x86_64-linux-gnu-inst.bin</a></code>
href="https://github.com/tlaplus/tlapm/releases/download/202210041448/tlaps-1.5.0-x86_64-linux-gnu-inst.bin">tlaps-1.5.0-x86_64-linux-gnu-inst.bin</a></code>
</p>

<h3>1. Install the Proof System </h3>
<p>You may have to change the installer's permissions with the
following command-line:</p>

<div class="terminal">$ chmod a+x tlaps-1.4.5-*-linux-gnu-inst.bin</div>
<div class="terminal">$ chmod a+x tlaps-1.5.0-*-linux-gnu-inst.bin</div>

<p>In order to install the proof system
into <code>/usr/local</code>, run the installer as:</p>

<div class="terminal">$ sudo ./tlaps-1.4.5-*-linux-gnu-inst.bin</div>
<div class="terminal">$ sudo ./tlaps-1.5.0-*-linux-gnu-inst.bin</div>
<p style="position:relative; left:70px; top:-10px">(you must have an
administrator account, and you will have to type your password)</p>

<p>If you want to install it in some other directory <em>dir</em>, run:</p>

<div class="terminal">$ sudo ./tlaps-1.4.5-*-linux-gnu-inst.bin -d <em>dir</em></div>
<div class="terminal">$ sudo ./tlaps-1.5.0-*-linux-gnu-inst.bin -d <em>dir</em></div>
<p style="position:relative; left:70px; top:-10px">(you must have an
administrator account, and you will have to type your password)</p>

Expand Down
6 changes: 3 additions & 3 deletions doc/web/content/Download/Binaries/MacOS.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ <h2><img class="blogo" src="images/logo_macosx30s.png"
alt="[Apple logo]"/>Mac OS X (10.13 and later)</h2>
<p class="first"> The package:
<code><a type="application/octet-stream"
href="https://github.com/tlaplus/tlapm/releases/latest/download/tlaps-1.4.5-i386-darwin-inst.bin">tlaps-1.4.5-i386-darwin-inst.bin</a></code>
href="https://github.com/tlaplus/tlapm/releases/download/202210041448/tlaps-1.5.0-i386-darwin-inst.bin">tlaps-1.5.0-i386-darwin-inst.bin</a></code>
</p>

<h3>1. Install &nbsp; <code>make</code> </h3>
Expand All @@ -40,12 +40,12 @@ <h3>2. Install the Proof System </h3>
<p>You may have to change the installer's permissions with the
following command-line:</p>

<div class="terminal">$ chmod a+x tlaps-1.4.5-i386-darwin-inst.bin</div>
<div class="terminal">$ chmod a+x tlaps-1.5.0-i386-darwin-inst.bin</div>

<p>In order to install the proof system
into <code>/usr/local</code>, run the installer as:</p>

<div class="terminal">$ sudo ./tlaps-1.4.5-i386-darwin-inst.bin</div>
<div class="terminal">$ sudo ./tlaps-1.5.0-i386-darwin-inst.bin</div>

<p style="position:relative; left:70px; top:-10px">(you must have an
administrator account, and you will have to type your password)</p>
Expand Down
75 changes: 5 additions & 70 deletions doc/web/content/Download/Binaries/Windows.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,76 +20,11 @@
<a name="0"></a>
<h2><img class="blogo" src="images/windows_logo_only.png"
alt="[Windows logo]"/>Windows</h2>
<p class="first"> The package:</p>
<ul>
<li>for 32-bit Cygwin: <code><a href="https://github.com/tlaplus/tlapm/releases/latest/download/tlaps-1.4.5-i686-cygwin-inst.exe">tlaps-1.4.5-i686-cygwin-inst.exe</a></code>
</ul>

<h3>1. Install Cygwin</h3>
<p><a href="http://www.cygwin.com">Cygwin</a> version 3.0.7
or later is required. You need to install the 32-bit version of
Cygwin, even if your OS is 64-bit. This version of TLAPS does
<b>not</b> work on 64-bit Cygwin.</p>

<h3>2. Install the Cygwin packages &nbsp;
<code>make</code>, <code>perl</code>, <code>wget</code></h3>
<p>Consult the
<a href="http://www.cygwin.com/cygwin-ug-net/setup-net.html">Cygwin
manual</a> for instructions on how to install Cygwin
packages. Installing these packages will bring in a number of other
packages, which are also needed.</p>

<h3>3. Install the Proof System</h3>
<p>Download the
<a href="https://github.com/tlaplus/tlapm/releases/latest/download/tlaps-1.4.5-i686-cygwin-inst.exe">TLAPS
installer</a>
and run the following command in a Cygwin terminal, from the
directory in which the package has been downloaded
(usually <code>/cygdrive/c/Users/$USER/Downloads</code>):</p>

<div class="terminal">$ ./tlaps-1.4.5-*-cygwin-inst.exe</div>

<p>This will install the TLAPM binary in <code>/usr/local/bin</code>
and some other data in <code>/usr/local/lib/tlaps</code>, including
the <code>zenon</code>, <code>isabelle</code>, <code>z3</code>,
<code>ls4</code>, and <code>translate</code> binaries.</p>

<h3>4. Set the Toolbox's library path</h3>
<p>We strongly recommend that you install the
<a href="http://lamport.azurewebsites.net/tla/toolbox.html">Toolbox</a>
(version 1.6.0 or later). You will need to add the location of the
<code>TLAPS.tla</code> file to the list
of libraries used by the Toolbox. To do this, open the Toolbox and
go to "File &gt; Preferences &gt; TLA+ Preferences". Add the
directory where <code>TLAPS.tla</code> is located to the list of
library path locations. If you have the default installation, this
directory is <code>C:\cygwin\usr\local\lib\tlaps\</code>.</p>

<h3>5. Install CVC4 (optional)</h3>
<p>You may want to install CVC4 to use as an additional SMT back-end
for TLAPS (the default, Z3, is included in the installer). Note
that some of our example files use CVC4 for a few proof obligations.</p>
<p>To install CVC4, you should download it from
<a href="http://cvc4.cs.stanford.edu/downloads/builds/win64-opt/">the
CVC4 download page</a>, then rename it and move it
to <code>/usr/local/lib/tlaps/bin</code> with this command:</p>

<div class="terminal">$ mv cvc4-1.7-win64-opt.exe /usr/local/lib/tlaps/bin/cvc4.exe</div>

</div>


<div class="section" style="position:relative; top:40px">
<h3>Uninstallation</h3>
<p>To uninstall TLAPS, open a cygwin terminal and type:</p>

<div class="terminal">$ `tlapm --where`/un-inst</div>

<p>The uninstaller for an existing version of TLAPS is automatically
run when the TLAPS installer (for any version of TLAPS, including
the same version) tries to install into the same location. Because
of this, <b>never store any important files in the directory where
TLAPS is installed</b>.</p>
<p class="first">
On Windows, TLAPS runs under WSL (Windows Subsystem for Linux).
After installing and launching the WSL follow the
<a href="Linux.html">TLAPS installation instructions for Linux</a>.
</p>
</div>


Expand Down
167 changes: 21 additions & 146 deletions doc/web/content/Download/Source.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,158 +21,33 @@
<h2>Generic Instructions</h2>

<p>These instructions apply to any UNIX-like system, including
GNU/Linux, most BSD variants, Solaris, Cygwin on Windows,
GNU/Linux, most BSD variants, Solaris, WSL on Windows,
MacOSX, etc.</p>
<p>Notes for Windows users:</p>
<ul>
<li>TLAPS requires Cygwin 3.0.7 or later. At this time it works only
with the 32-bit version of cygwin.</li>
<li>The following Cygwin packages are required for the
instructions below: <code>gcc4</code>, <code>make</code>,
<code>wget</code>, <code>perl</code>. Install them using
Cygwin's <code>setup.exe</code>.</li>
</ul>
<p>Notes for Windows users: TLAPS requires WSL (Windows Subsystem for Linux).</p>

<p> TLAPS tarball:
<a href="https://github.com/tlaplus/tlapm/archive/v1.4.5.tar.gz">tlaps-1.4.5.tar.gz</a></p>


<h3>1. Unpack TLAPS tarball</h3>
<div class="hr"></div>

<p>You can unpack TLAPS by running the following command:</p>

<div class="terminal">$ tar -xzf tlaps-1.4.5.tar.gz</div>

<p>This creates a directory named <code>tlaps-1.4.5</code> that
contains four subdirectories: <code>tlapm</code>, <code>zenon</code>,
<code>isabelle</code> and <code>emacs</code>.</p>

<h3>2. Install OCaml</h3>
<div class="hr"></div>

<p>TLAPS is implemented in OCaml and requires version 4.04.2 or
higher. You can follow any of the suggestions
on <a href="https://ocaml.org/docs/install.html">the offical
OCaml release page</a> to install OCaml. On Windows/Cygwin, OCaml
can be installed directly from Cygwin's <code>setup.exe</code>.
On most modern
GNU/Linux distributions, OCaml is already packaged. Here are the
commands for the common Linux distributions:</p>

<table style="margin-left: 2em;">
<tbody>
<tr>
<td style="padding-right: 3em;">Debian, Ubuntu, etc.</td>
<td><code>apt-get install ocaml</code></td>
</tr>
<tr>
<td valign="top">Redhat, Fedora, SuSe,<br /> Mandriva, CentOS, etc.</td>
<td valign="top"><code>yum install ocaml</code></td>
</tr>
<tr>
<td valign="top">Gentoo</td>
<td valign="top"><code>emerge ocaml</code></td>
</tr>
<tr>
<td valign="top">Arch Linux</td>
<td valign="top"><code>pacman install ocaml</code></td>
</tr>
</tbody>
</table>

<p> On MacOSX, you can use the package
managers <a href="http://brew.sh/">Homebrew</a>
(<code>brew install objective-caml</code>)
or <a href="http://www.macports.org">MacPorts</a>
(<code>port install ocaml</code>).</p>

<p>If you want to install OCaml from source, consider
using <a href="http://opam.ocaml.org">OPAM</a>.</p>

<h3>3. Compile and Install Zenon</h3>
<div class="hr"></div>

<p>Run the following commands.</p>

<div class="terminal">$ pushd tlaps-1.4.5/zenon<br/>
$ ./configure &amp;&amp; make &amp;&amp; make install<br/>
$ popd</div>

<p>By default, the above will try to install
in <code>/usr/local</code>. If you don't have write access to that
directory, or would rather install Zenon elsewhere, such as
in <code>$HOME/bin</code>, run the following:</p>

<div class="terminal">$ pushd tlaps-1.4.5/zenon<br/>
$ ./configure --prefix $HOME &amp;&amp; make &amp;&amp; make install<br/>
$ popd</div>

<h3>4. Install Isabelle2011-1</h3>
<h3>1. Obtain source code</h3>
<div class="hr"></div>

<p>Follow the
<a href="http://isabelle.in.tum.de/website-Isabelle2011-1/download.html">instructions</a>
on the Isabelle Web site. TLAPS actually does not need the full
Isabelle2011-1 distribution. If you want only the necessary
components, run the following commands:</p>

<div class="terminal" style="width:95%">$ wget http://isabelle.in.tum.de/website-Isabelle2011-1/dist/Isabelle2011-1.tar.gz<br/>
$ wget http://isabelle.in.tum.de/website-Isabelle2011-1/dist/polyml-5.4.0.tar.gz<br/>
$ tar -xzf -C /usr/local Isabelle2011-1.tar.gz<br/>
$ tar -xzf -C /usr/local polyml-5.4.0.tar.gz</div>

<p style="position:relative; top:10px">You may
replace <code>/usr/local</code> above by any other directory. For
example, to install Isabelle2011-1 in your <code>$HOME</code>,
use <code> -C $HOME </code> instead of <code> -C /usr/local </code>.</p>

<p>Note that the <code>isabelle</code>
and <code>isabelle-process</code> executables (found
in <code>/usr/local/Isabelle/bin</code>
or <code>$HOME/Isabelle/bin</code>), or symbolic links to them, must
be in your <code>$PATH</code> for TLAPS to work.</p>

<p>You may delete the <code>Isabelle2011-1.tar.gz</code> and
<code>polyml-5.4.0.tar.gz</code> files after the above steps.</p>

<h3>5. Compile Isabelle/TLA+</h3>
<div class="hr"></div>

<p>Run the following commands.</p>

<div class="terminal">$ pushd /usr/local/Isabelle/src/Pure<br/>
$ isabelle make<br/>
$ popd<br/>
$ pushd tlaps-1.4.5/isabelle<br/>
$ make<br/>
$ popd</div>

<p>(Replace <code>/usr/local</code> above with wherever you
installed Isabelle in the previous step.)</p>

<h3>6. Compile the <strong>TLA</strong><sup>+</sup>
<p>TLAPS source code can be obtained as a release tarball or cloned from the <code>git</code> repository.
<ol type="A">
<li>
<p>Download the tarball: <a href="https://github.com/tlaplus/tlapm/archive/refs/tags/202210041448.tar.gz">202210041448.tar.gz</a></p>
<p>You can unpack TLAPS by running the following command:</p>
<div class="terminal">$ tar -xzf 202210041448.tar.gz</div>
</li>
<li>
<p>Clone the repository</p>
<div class="terminal">$ git clone https://github.com/tlaplus/tlapm/</div>
</li>
</ol>
</p>

<h3>2. Compile the <strong>TLA</strong><sup>+</sup>
<strong>P</strong>roof <strong>M</strong>anager (TLAPM)</h3>
<div class="hr"></div>

<p>Run the following commands.</p>

<div class="terminal">$ pushd tlaps-1.4.5/tlapm<br/>
$ ./configure &amp;&amp; make all<br/>
$ sudo make install<br/>
$ popd</div>

<p>By default, the above will try to install TLAPM
in <code>/usr/local</code>. If you don't have write access to that
directory, or would rather install the <code>TLAPM</code> elsewhere,
such as in <code>$HOME/bin</code>, run the following:</p>

<div class="terminal">$ pushd tlaps-1.4.5/tlapm<br/>
$ ./configure --prefix $HOME &amp;&amp; make all<br/>
$ make install<br/>
$ popd</div>
<p>See instructions at <a href="https://github.com/tlaplus/tlapm/blob/main/INSTALL.md">INSTALL.md</a>.</p>

<h3>7. Verify the installation</h3>
<h3>3. Verify the installation</h3>
<div class="hr"></div>

<p>Run the following command:</p>
Expand All @@ -183,7 +58,7 @@ <h3>7. Verify the installation</h3>
and <code>isabelle</code> you installed in earlier steps.</p>

<p>You can also test the <code>TLAPS</code> on any of the examples
in the <code>/usr/local/lib/tlaps/examples</code> directory (which
in the <code>examples</code> directory (which
you can easily refer to using the option <code>-I +examples</code>
to <code>tlapm</code>). For instance:</p>

Expand Down

0 comments on commit 8facb9a

Please sign in to comment.