Use Isabelle202x

.github/workflows/ci.yml

@@ -11,8 +11,13 @@ jobs:
         strategy:
           fail-fast: false
           matrix:
-            os: [ubuntu-latest, macos-13]
-            ocaml-compiler: ['4.13.1', '5.1.0']
+            os:
+              - ubuntu-latest
+              - macos-13
+              - macos-14
+            ocaml-compiler:
+              - '4.13.1'
+              - '5.1.0'
         env:
           EXAMPLES_DIR: "tlaplus-examples"
           SCRIPT_DIR: "tlaplus-examples/.github/scripts"
@@ -21,19 +26,19 @@ jobs:
         steps:
             - name: Clone repo
               uses: actions/checkout@v4
-            - name: Install deps
+            - name: Install deps (ubuntu)
               if: matrix.os == 'ubuntu-latest'
               run: |
                 sudo apt-get update
                 sudo apt-get install --yes time
             - uses: ocaml/setup-ocaml@v2
               with:
                 ocaml-compiler: ${{ matrix.ocaml-compiler }}
-            # - uses: actions/cache@v3
-            #   id: cache
-            #   with:
-            #     path: _build_cache
-            #     key: ${{ runner.os }}_build_cache
+            - uses: actions/cache@v4
+              id: cache
+              with:
+                path: _build_cache
+                key: ${{ runner.os }}_build_cache
             - name: Build TLAPM
               run: |
                 eval $(opam env)
@@ -65,9 +70,6 @@ jobs:
                 rm "$DEPS_DIR/tlaps.tar.gz"
                 mv $DEPS_DIR/tlaps* "$DEPS_DIR/tlapm-install"
                 SKIP=(
-                  # Missing operator ENABLEDrules; will be fixed after
-                  # updated_enabled_cdot branch is merged.
-                  "specifications/ewd998/AsyncTerminationDetection.tla"
                   # General proof failure
                   "specifications/Bakery-Boulangerie/Bakery.tla"
                   "specifications/Bakery-Boulangerie/Boulanger.tla"
@@ -80,12 +82,9 @@ jobs:
                   "specifications/LoopInvariance/BinarySearch.tla"
                   "specifications/LoopInvariance/Quicksort.tla"
                   "specifications/LoopInvariance/SumSequence.tla"
-                  "specifications/MisraReachability/ReachabilityProofs.tla"
-                  "specifications/Paxos/Consensus.tla"
-                  "specifications/PaxosHowToWinATuringAward/Consensus.tla"
                   "specifications/lamport_mutex/LamportMutex_proofs.tla"
                   "specifications/TeachingConcurrency/SimpleRegular.tla"
-                  # Long-running
+                  # Failing and long-running
                   "specifications/byzpaxos/BPConProof.tla" # Takes about 30 minutes
                 )
                 python "$SCRIPT_DIR/check_proofs.py"            \

.github/workflows/release.yml

@@ -57,18 +57,17 @@ jobs:
         name: Create TLAPS installer, and upload it to GitHub release
             # fast testing *does* commence below
         needs: [release]
-        runs-on: ${{ matrix.operating-system }}
+        runs-on: ${{ matrix.os }}
         strategy:
             matrix:
-                operating-system: [
-                    macos-13,
-                    ubuntu-latest]
-                ocaml-compiler: [
-                    '4.13.1',
-                    ]
+                os:
+                  - macos-13
+                  - ubuntu-latest
+                ocaml-compiler:
+                  - '5.1.0'
         steps:
-            - name: Install deps
-              if: matrix.operating-system == 'ubuntu-latest'
+            - name: Install deps (ubuntu)
+              if: matrix.os == 'ubuntu-latest'
               run: |
                 sudo apt-get update
                 sudo apt-get install --yes time
@@ -93,11 +92,11 @@ jobs:
             - uses: ocaml/setup-ocaml@v2
               with:
                 ocaml-compiler: ${{ matrix.ocaml-compiler }}
-            # - uses: actions/cache@v3
-            #   id: cache
-            #   with:
-            #     path: _build_cache
-            #     key: ${{ runner.os }}_build_cache
+            - uses: actions/cache@v4
+              id: cache
+              with:
+                path: _build_cache
+                key: ${{ runner.os }}_build_cache
             - name: Build installer of TLAPS
               run: |
                 eval $(opam env)

.gitignore

@@ -1,7 +1,3 @@
-*.o
-*.cmi
-*.cmx
-*.annot
 *.exe
 *.err
 *.out

INSTALL.md

@@ -27,17 +27,20 @@ Copyright (C) 2008-2010  INRIA and Microsoft Corporation
 
 ## 1. Installation
 
-### 1.1. Linux
-
-#### 1.1.1. Setup the environment
+### 1.1. Setup the environment
 
 Setup required OS packages; Debian/Ubuntu:
 ```{bash}
 sudo apt install opam zlib1g-dev gawk time
 ```
 Arch Linux:
 ```{bash}
-sudo pacman -S ocaml opam dune zlib time
+sudo pacman -Sy time git make gcc patch diffutils ocaml opam dune zlib wget fontconfig gnu-free-fonts
+```
+
+macOS:
+```{bash}
+# No additional packages needed.
 ```
 
 Initialize the OPAM. Add `--disable-sandboxing` option if running this on the docker or sandboxing is not supported for other reasons.
@@ -53,7 +56,7 @@ opam switch create 5.1.0
 eval $(opam env --switch=5.1.0)
 ```
 
-#### 1.1.2. Build and install TLAPM
+### 1.2. Build and install TLAPM
 
 Clone the TLAPM source code
 
@@ -65,6 +68,7 @@ cd tlapm
 Install the dependencies via OPAM. A helper `make` target is present for that:
 
 ```{bash}
+make opam-update
 make opam-deps
 ```
 
@@ -86,13 +90,13 @@ Now you can invoke `tlapm` in either way:
   - `~/.opam/5.1.0/bin/tlapm --help`.
 
 
-#### 1.1.3. Running the tests
+### 1.3. Running the tests
 To run the test suite, invoke:
 ```{bash}
 make test
 ```
 
-#### 1.1.4. Development environment
+### 1.4. Development environment
 
 To setup the development environment, run the following in addition to the above steps:
 
@@ -103,9 +107,9 @@ make opam-deps-dev
 Then view/edit the code e.g. using VSCode with the `OCaml Platform` extension installed.
 
 
-#### 1.1.5. Testing the build/install procedures
+## Appendix: Testing the build/install procedures
 
-The above instructions were tested with
+The above instructions were tested for Debian as follows:
 
 ```{bash}
 docker run -it --rm debian bash

Makefile

@@ -17,6 +17,10 @@ PREFIX=$(OPAM_SWITCH_PREFIX)
 
 all: build
 
+opam-update: # Update the package lists and install updates.
+	opam update
+	opam upgrade
+
 opam-deps:
 	opam install ./ --deps-only --yes --working-dir
 

deps/Makefile.post-install

@@ -1,3 +1,3 @@
 all:
 	chmod +x backends/bin/*
-	make -C backends -f Isabelle.post-install
+	cd backends && cat Isabelle.exec-files | xargs chmod +x

deps/isabelle/.gitignore

@@ -0,0 +1,3 @@
+/Isabelle.exec-files
+/Isabelle/
+/Isabelle-test/

deps/isabelle/README.md

@@ -0,0 +1,13 @@
+## Debugging Isabelle prover
+
+Run the `tlapm` with the `--debug=tempfiles` option, e.g.:
+
+    (cd ../tlaplus-examples/specifications/MisraReachability/ \
+        && rm -rf .tlacache/ && tlapm --toolbox 228 228 --debug=tempfiles ReachabilityProofs.tla)
+
+Then look for the corresponding `*.thy` files and open them with Isabelle, e.g.
+
+    ./_build/default/deps/isabelle/Isabelle/bin/isabelle jedit \
+        -d ./_build/default/deps/isabelle/Isabelle/src/TLA+/ \
+        ../tlaplus-examples/specifications/MisraReachability/.tlacache/ReachabilityProofs.tlaps/tlapm_624cb2.thy
+

deps/isabelle/dune

@@ -2,14 +2,21 @@
 ; The source code for the TLA+ theory is in the $PROJECT_ROOT/isabelle directory.
 ; The generated heaps (Pure and TLA+) are in Isabelle/heaps/polyml-*/.
 (rule
- (deps "Makefile" (source_tree theories))
- (targets (dir Isabelle) "Isabelle.no-links" "Isabelle.post-install")
- (action (run "make" "-C" "." "PROJECT_ROOT=%{project_root}" "Isabelle.no-links" "Isabelle.post-install")))
+ (alias default)
+ (deps
+  "dune.mk"
+  (source_tree ../../isabelle)
+  (sandbox none))
+ (targets
+  (dir "Isabelle")
+  (dir "Isabelle-test")
+  "Isabelle.exec-files")
+ (action (run "make" "-f" "dune.mk")))
 
 (install
  (section (site (tlapm backends)))
  (dirs Isabelle))
 
 (install
  (section (site (tlapm backends)))
- (files ("Isabelle.post-install" as "Isabelle.post-install")))
+ (files ("Isabelle.exec-files" as "Isabelle.exec-files")))