Use tlaplus/examples for tests

Unified main/pr workflows Added install instructions for Arch Linux Signed-off-by: Andrew Helwer <[email protected]>
tlaplus · Apr 20, 2024 · e206ef1 · e206ef1
1 parent d53d147
commit e206ef1
Show file tree

Hide file tree

Showing 5 changed files with 107 additions and 141 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -0,0 +1,97 @@
+name: Build & Test
+on: [pull_request]
+on:
+  push:
+    branches: [main]
+jobs:
+    test:
+        name: Build & Test
+        runs-on: ${{ matrix.os }}
+        strategy:
+          fail-fast: false
+          matrix:
+            os: [ubuntu-latest, macos-latest]
+            ocaml-compiler: ['0', '1']
+        env:
+          EXAMPLES_DIR: "tlaplus-examples"
+          SCRIPT_DIR: "tlaplus-examples/.github/scripts"
+          DEPS_DIR: "tlaplus-examples/deps"
+          DIST_DIR: "tlatools/org.lamport.tlatools/dist"
+        steps:
+            - name: Clone repo
+              uses: actions/checkout@v4
+            - name: Install deps
+              if: matrix.os == 'ubuntu-latest'
+              run: |
+                sudo apt-get update
+                sudo apt-get install --yes time
+            - name: Set up Python
+              uses: actions/setup-python@v5
+              with:
+                python-version: '3.12'
+            - name: Get OCaml version
+              run: |
+                INDEX=${{ matrix.ocaml-compiler }}
+                OCAML_VERSION=\
+                `python .github/workflows/ocaml_versions.py $INDEX`
+                echo "OCAML_VERSION=$OCAML_VERSION" \
+                >> $GITHUB_ENV
+                echo "OCAML_VERSION = $OCAML_VERSION"
+            - uses: ocaml/setup-ocaml@v2
+              with:
+                ocaml-compiler: ${{ env.OCAML_VERSION }}
+            # - uses: actions/cache@v3
+            #   id: cache
+            #   with:
+            #     path: _build_cache
+            #     key: ${{ runner.os }}_build_cache
+            - name: Build TLAPM
+              run: |
+                eval $(opam env)
+                opam install ./ --deps-only --yes
+                make
+                make release
+            - name: Clone tlaplus/examples
+              uses: actions/checkout@v4
+              with:
+                repository: tlaplus/examples
+                path: ${{ env.EXAMPLES_DIR }}
+            - name: Check proofs in TLA+ examples
+              run: |
+                mkdir -p "$DEPS_DIR"
+                cp ./_build/tlaps*.tar.gz "$DEPS_DIR/tlaps.tar.gz"
+                tar -xzf "$DEPS_DIR/tlaps.tar.gz" -C "$DEPS_DIR"
+                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"
+                  "specifications/LearnProofs/FindHighest.tla"
+                  "specifications/LoopInvariance/BinarySearch.tla"
+                  "specifications/LoopInvariance/Quicksort.tla"
+                  "specifications/LoopInvariance/SumSequence.tla"
+                  "specifications/TeachingConcurrency/SimpleRegular.tla"
+                  "specifications/MisraReachability/ReachabilityProofs.tla"
+                  "specifications/Paxos/Consensus.tla"
+                  "specifications/PaxosHowToWinATuringAward/Consensus.tla"
+                  "specifications/lamport_mutex/LamportMutex_proofs.tla"
+                  # Long-running
+                  "specifications/byzpaxos/BPConProof.tla" # Takes about 30 minutes
+                )
+                python "$SCRIPT_DIR/check_proofs.py"            \
+                  --tlapm_path "$DEPS_DIR/tlapm-install"        \
+                  --manifest_path "$EXAMPLES_DIR/manifest.json" \
+                  --skip "${SKIP[@]}"
+            - name: Run tests
+              run: |
+                eval $(opam env)
+                set +e
+                make test
+                TEST_RESULT=$?
+                cat _build/default/test/tests.log
+                exit $TEST_RESULT
+
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
diff --git a/.github/workflows/ocaml_versions.py b/.github/workflows/ocaml_versions.py
@@ -3,9 +3,8 @@
 
 
 OCAML_VERSIONS = [
-    '4.08.1',
-    '4.13.0',
-    '4.14.0',
+    '4.13.1',
+    '5.1.0',
     ]
 
 

diff --git a/.github/workflows/pr.yml b/.github/workflows/pr.yml
diff --git a/INSTALL.md b/INSTALL.md
@@ -15,6 +15,8 @@ Copyright (C) 2008-2010  INRIA and Microsoft Corporation
 
     Typically installed using `opam` (<https://opam.ocaml.org/>).
 
+  - The Dune build system.
+
   - Zenon.
 
     Built during the TLAPM build procedure.
@@ -25,15 +27,18 @@ Copyright (C) 2008-2010  INRIA and Microsoft Corporation
 
 ## 1. Installation
 
-### 1.1. Debian / Ubuntu
+### 1.1. Linux
 
 #### 1.1.1. Setup the environment
 
-Setup required OS packages:
-
+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
+```
 
 Initialize the OPAM. Add `--disable-sandboxing` option if running this on the docker or sandboxing is not supported for other reasons.