From 4e173912fc6dd2a7a0c964ccb97fbb0a06cc819e Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Fri, 19 Apr 2024 07:18:09 +0300 Subject: [PATCH 1/3] Update the installation instructions. Fixes #123. Signed-off-by: Karolis Petrauskas --- doc/web/content/Download/Binaries/Linux.html | 8 +- doc/web/content/Download/Binaries/MacOS.html | 6 +- .../content/Download/Binaries/Windows.html | 75 +------- doc/web/content/Download/Source.html | 167 +++--------------- 4 files changed, 33 insertions(+), 223 deletions(-) diff --git a/doc/web/content/Download/Binaries/Linux.html b/doc/web/content/Download/Binaries/Linux.html index 936b0bd5..f3ca9571 100644 --- a/doc/web/content/Download/Binaries/Linux.html +++ b/doc/web/content/Download/Binaries/Linux.html @@ -21,25 +21,25 @@

Linux

The package: tlaps-1.4.5-x86_64-linux-gnu-inst.bin + 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

1. Install the Proof System

You may have to change the installer's permissions with the following command-line:

-
$ chmod a+x tlaps-1.4.5-*-linux-gnu-inst.bin
+
$ chmod a+x tlaps-1.5.0-*-linux-gnu-inst.bin

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

-
$ sudo ./tlaps-1.4.5-*-linux-gnu-inst.bin
+
$ sudo ./tlaps-1.5.0-*-linux-gnu-inst.bin

(you must have an administrator account, and you will have to type your password)

If you want to install it in some other directory dir, run:

-
$ sudo ./tlaps-1.4.5-*-linux-gnu-inst.bin -d dir
+
$ sudo ./tlaps-1.5.0-*-linux-gnu-inst.bin -d dir

(you must have an administrator account, and you will have to type your password)

diff --git a/doc/web/content/Download/Binaries/MacOS.html b/doc/web/content/Download/Binaries/MacOS.html index 21a354ed..6ac7a810 100644 --- a/doc/web/content/Download/Binaries/MacOS.html +++ b/doc/web/content/Download/Binaries/MacOS.html @@ -21,7 +21,7 @@

Mac OS X (10.13 and later)

The package: tlaps-1.4.5-i386-darwin-inst.bin + 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

1. Install   make

@@ -40,12 +40,12 @@

2. Install the Proof System

You may have to change the installer's permissions with the following command-line:

-
$ chmod a+x tlaps-1.4.5-i386-darwin-inst.bin
+
$ chmod a+x tlaps-1.5.0-i386-darwin-inst.bin

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

-
$ sudo ./tlaps-1.4.5-i386-darwin-inst.bin
+
$ sudo ./tlaps-1.5.0-i386-darwin-inst.bin

(you must have an administrator account, and you will have to type your password)

diff --git a/doc/web/content/Download/Binaries/Windows.html b/doc/web/content/Download/Binaries/Windows.html index b226ce94..bbef5dfe 100644 --- a/doc/web/content/Download/Binaries/Windows.html +++ b/doc/web/content/Download/Binaries/Windows.html @@ -20,76 +20,11 @@

Windows

-

The package:

- - -

1. Install Cygwin

-

Cygwin 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 - not work on 64-bit Cygwin.

- -

2. Install the Cygwin packages   - make, perl, wget

-

Consult the - Cygwin - manual for instructions on how to install Cygwin - packages. Installing these packages will bring in a number of other - packages, which are also needed.

- -

3. Install the Proof System

-

Download the - TLAPS - installer - and run the following command in a Cygwin terminal, from the - directory in which the package has been downloaded - (usually /cygdrive/c/Users/$USER/Downloads):

- -
$ ./tlaps-1.4.5-*-cygwin-inst.exe
- -

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

- -

4. Set the Toolbox's library path

-

We strongly recommend that you install the - Toolbox - (version 1.6.0 or later). You will need to add the location of the - TLAPS.tla file to the list - of libraries used by the Toolbox. To do this, open the Toolbox and - go to "File > Preferences > TLA+ Preferences". Add the - directory where TLAPS.tla is located to the list of - library path locations. If you have the default installation, this - directory is C:\cygwin\usr\local\lib\tlaps\.

- -

5. Install CVC4 (optional)

-

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.

-

To install CVC4, you should download it from - the - CVC4 download page, then rename it and move it - to /usr/local/lib/tlaps/bin with this command:

- -
$ mv cvc4-1.7-win64-opt.exe /usr/local/lib/tlaps/bin/cvc4.exe
- - - - -
-

Uninstallation

-

To uninstall TLAPS, open a cygwin terminal and type:

- -
$ `tlapm --where`/un-inst
- -

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, never store any important files in the directory where - TLAPS is installed.

+

+ On Windows, TLAPS runs under WSL (Windows Subsystem for Linux). + After installing and launching the WSL follow the + TLAPS installation instructions for Linux. +

diff --git a/doc/web/content/Download/Source.html b/doc/web/content/Download/Source.html index a07d7ca3..2ad2d665 100644 --- a/doc/web/content/Download/Source.html +++ b/doc/web/content/Download/Source.html @@ -21,158 +21,33 @@

Generic Instructions

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, MacOSX, etc.

-

Notes for Windows users:

- +

Notes for Windows users: TLAPS requires WSL (Windows Subsystem for Linux).

-

TLAPS tarball: - tlaps-1.4.5.tar.gz

- - -

1. Unpack TLAPS tarball

-
- -

You can unpack TLAPS by running the following command:

- -
$ tar -xzf tlaps-1.4.5.tar.gz
- -

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

- -

2. Install OCaml

-
- -

TLAPS is implemented in OCaml and requires version 4.04.2 or - higher. You can follow any of the suggestions - on the offical - OCaml release page to install OCaml. On Windows/Cygwin, OCaml - can be installed directly from Cygwin's setup.exe. - On most modern - GNU/Linux distributions, OCaml is already packaged. Here are the - commands for the common Linux distributions:

- - - - - - - - - - - - - - - - - - - - -
Debian, Ubuntu, etc.apt-get install ocaml
Redhat, Fedora, SuSe,
Mandriva, CentOS, etc.		yum install ocaml
Gentooemerge ocaml
Arch Linuxpacman install ocaml
- -

On MacOSX, you can use the package - managers Homebrew - (brew install objective-caml) - or MacPorts - (port install ocaml).

- -

If you want to install OCaml from source, consider - using OPAM.

- -

3. Compile and Install Zenon

-
- -

Run the following commands.

- -
$ pushd tlaps-1.4.5/zenon
-$ ./configure && make && make install
-$ popd
- -

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

- -
$ pushd tlaps-1.4.5/zenon
-$ ./configure --prefix $HOME && make && make install
-$ popd
- -

4. Install Isabelle2011-1

+

1. Obtain source code

- -

Follow the - instructions - 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:

- -
$ wget http://isabelle.in.tum.de/website-Isabelle2011-1/dist/Isabelle2011-1.tar.gz
-$ wget http://isabelle.in.tum.de/website-Isabelle2011-1/dist/polyml-5.4.0.tar.gz
-$ tar -xzf -C /usr/local Isabelle2011-1.tar.gz
-$ tar -xzf -C /usr/local polyml-5.4.0.tar.gz
- -

You may - replace /usr/local above by any other directory. For - example, to install Isabelle2011-1 in your $HOME, - use -C $HOME instead of -C /usr/local .

- -

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

- -

You may delete the Isabelle2011-1.tar.gz and - polyml-5.4.0.tar.gz files after the above steps.

- -

5. Compile Isabelle/TLA+

-
- -

Run the following commands.

- -
$ pushd /usr/local/Isabelle/src/Pure
-$ isabelle make
-$ popd
-$ pushd tlaps-1.4.5/isabelle
-$ make
-$ popd
- -

(Replace /usr/local above with wherever you - installed Isabelle in the previous step.)

- -

6. Compile the TLA+ +

TLAPS source code can be obtained as a release tarball or cloned from the git repository. +

    +
  1. +

    Download the tarball: 202210041448.tar.gz

    +

    You can unpack TLAPS by running the following command:

    +
    $ tar -xzf 202210041448.tar.gz
    +
    2. +
  2. +

    Clone the repository

    +
    $ git clone https://github.com/tlaplus/tlapm/
    +
    3. +
+

+ +

2. Compile the TLA+ Proof Manager (TLAPM)

-

Run the following commands.

- -
$ pushd tlaps-1.4.5/tlapm
-$ ./configure && make all
-$ sudo make install
-$ popd
- -

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

- -
$ pushd tlaps-1.4.5/tlapm
-$ ./configure --prefix $HOME && make all
-$ make install
-$ popd
+

See instructions at INSTALL.md.

-

7. Verify the installation

+

3. Verify the installation

Run the following command:

@@ -183,7 +58,7 @@

7. Verify the installation

and isabelle you installed in earlier steps.

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

From 0cc875c05ee625e1f0710453d24edd42e3ab9fc0 Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Sat, 4 May 2024 08:32:29 +0300 Subject: [PATCH 2/3] Cygwin is not supported currently. Signed-off-by: Karolis Petrauskas --- doc/web/content/Download/Source.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/web/content/Download/Source.html b/doc/web/content/Download/Source.html index 2ad2d665..52b9003f 100644 --- a/doc/web/content/Download/Source.html +++ b/doc/web/content/Download/Source.html @@ -21,7 +21,7 @@

Generic Instructions

These instructions apply to any UNIX-like system, including - GNU/Linux, most BSD variants, Solaris, WSL and Cygwin on Windows, + GNU/Linux, most BSD variants, Solaris, WSL on Windows, MacOSX, etc.

Notes for Windows users: TLAPS requires WSL (Windows Subsystem for Linux).

From ed54ce0aa35e907e9c5d7343264af1a221d3707c Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Sun, 5 May 2024 12:30:05 +0300 Subject: [PATCH 3/3] Use macos version that supports x86 architecture. Signed-off-by: Karolis Petrauskas --- .github/workflows/ci.yml | 2 +- .github/workflows/release.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6797264d..e2339313 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -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" diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 5de22a38..3611dea6 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -61,7 +61,7 @@ jobs: strategy: matrix: operating-system: [ - macos-latest, + macos-13, ubuntu-latest] ocaml-compiler: [ '2',