Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update the installation instructions. #125

Merged
merged 4 commits into from
May 5, 2024
Merged

Update the installation instructions. #125

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
4e17391
Update the installation instructions.
kape1395 Apr 19, 2024
0cc875c
Cygwin is not supported currently.
kape1395 May 4, 2024
cba4808
Merge remote-tracking branch 'origin/main' into docs-install
kape1395 May 4, 2024
ed54ce0
Use macos version that supports x86 architecture.
kape1395 May 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions doc/web/content/Download/Binaries/Linux.html
View file
Open in desktop
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>
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In the (near) future when we switch to a rolling release model I suppose we will want to use the /latest/ tag along with a link to a binary that does not have the version in the name.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree. This will have to be changed in the future.
For now, I just wanted to keep links valid after a new release is made.

</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
Open in desktop
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
Open in desktop
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
Open in desktop
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 and Cygwin on Windows,
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we want to remove mention of Cygwin here and focus on WSL support?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, I removed the mention of Cygwin.

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
Loading