Upload nightly build and use examples for tests

Added install instructions for Arch Linux Fixed bug in generation of makefile Removed redundant tests in CI Signed-off-by: Andrew Helwer <[email protected]>
tlaplus · Jan 27, 2024 · fde994b · fde994b
1 parent a0ae986
commit fde994b
Show file tree

Hide file tree

Showing 6 changed files with 95 additions and 80 deletions.
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -1,33 +1,31 @@
 name: Build and Package TLA Proof Manager
 on:
-    push:
-    schedule:
-        - cron: '42 5 5 * *'
+  push:
+    branches:
+      - main
 jobs:
     test:
         name: Build TLAPS installer and test it
         runs-on: ${{ matrix.operating-system }}
         strategy:
-            matrix:
-                operating-system: [
-                    macos-latest,
-                    ubuntu-latest]
-                ocaml-compiler: [
-                    '0',
-                    '1',
-                    '2',
-                    ]
+          matrix:
+            operating-system:
+              - macos-latest,
+              - ubuntu-latest
+            ocaml-compiler:
+              - '0'
+              - '1'
         steps:
             - name: Install deps
               if: matrix.operating-system == 'ubuntu-latest'
               run: |
                 sudo apt-get update
                 sudo apt-get install --yes time
             - name: Set up Python
-              uses: actions/setup-python@v2
+              uses: actions/setup-python@v4
               with:
-                python-version: '3.10'
-            - uses: actions/checkout@v2
+                python-version: '3.12'
+            - uses: actions/checkout@v3
             - name: Get OCaml version
               run: |
                 INDEX=${{ matrix.ocaml-compiler }}
@@ -39,29 +37,28 @@ jobs:
             - 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 installer of TLAPS
+            - name: Build TLAPS installer
               run: |
                 eval $(opam env)
                 opam install ./ --deps-only --yes
                 make
                 make release
-            - name: Run a subset of `tlapm` tests
-              run: |
-                eval $(opam env)
-                make test-inline test-fast-basic
-            - name: Run all `tlapm` tests
+            - name: Run tests
               if: >-
                 matrix.operating-system == 'ubuntu-latest' &&
-                matrix.ocaml-compiler == '2'
+                matrix.ocaml-compiler == '1'
               run: |
                 eval $(opam env)
+                set +e
                 make test
-            - name: Print Test Results
-              if: matrix.operating-system == 'ubuntu-latest'
-              run: |
+                TEST_RESULT=$?
                 cat _build/default/test/tests.log
+                exit $TEST_RESULT
+            - name: Trigger run of tlaplus/examples CI
+              if: matrix.ocaml-compiler == '1'
+              uses: peter-evans/repository-dispatch@v2
+              with:
+                  token: ${{ secrets.GITHUB_TOKEN }}
+                  repository: tlaplus/examples
+                  event-type: tlapm-dispatch
+
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
@@ -1,37 +1,30 @@
 name: Build on PR
-on:
-    pull_request:
-    push:
-        paths:
-            - '.github/workflows/pr.yml'
-    schedule:
-        - cron: '42 5 20 * *'
+on: [pull_request]
 jobs:
     test:
         name: Build and Test
         runs-on: ${{ matrix.operating-system }}
         strategy:
-            fail-fast: false
-            matrix:
-                operating-system: [
-                    macos-latest,
-                    ubuntu-latest]
-                ocaml-compiler: [
-                    '0',
-                    '1',
-                    '2',
-                    ]
+          fail-fast: false
+          matrix:
+            operating-system:
+              - macos-latest,
+              - ubuntu-latest
+            ocaml-compiler:
+              - '0'
+              - '1'
         steps:
             - name: Install deps
               if: matrix.operating-system == 'ubuntu-latest'
               run: |
                 sudo apt-get update
                 sudo apt-get install --yes time
             - name: Set up Python
-              uses: actions/setup-python@v2
+              uses: actions/setup-python@v4
               with:
-                python-version: '3.10'
-            - uses: actions/checkout@v2
+                python-version: '3.12'
+            - name: Clone repo
+              uses: actions/checkout@v3
             - name: Get OCaml version
               run: |
                 INDEX=${{ matrix.ocaml-compiler }}
@@ -48,21 +41,45 @@ jobs:
             #   with:
             #     path: _build_cache
             #     key: ${{ runner.os }}_build_cache
-            - name: Build installer of TLAPS
+            - name: Build TLAPS installer
               run: |
                 eval $(opam env)
                 opam install ./ --deps-only --yes
                 make
                 make release
-            - name: Run a subset of `tlapm` tests
+            - name: Get TLA+ examples
+              uses: actions/checkout@v3
+              with:
+                repository: tlaplus/examples
+                path: tlaplus-examples
+            - name: Check proofs in TLA+ examples
               run: |
-                eval $(opam env)
-                make test-inline test-fast-basic
-            - name: Run all `tlapm` tests
+                EXAMPLES_DIR=tlaplus-examples
+                mkdir $EXAMPLES_DIR/deps
+                cp ./_build/tlaps*.tar.gz $EXAMPLES_DIR/deps/tlaps.tar.gz
+                tar -xzf $EXAMPLES_DIR/deps/tlaps.tar.gz -C $EXAMPLES_DIR/deps
+                rm $EXAMPLES_DIR/deps/tlaps.tar.gz
+                mv $EXAMPLES_DIR/deps/tlaps* $EXAMPLES_DIR/deps/tlapm-install
+                SKIP=(
+                  # Missing operator ENABLEDrules; will be fixed after
+                  # updated_enabled_cdot branch is merged.
+                  "specifications/ewd998/AsyncTerminationDetection.tla",
+                  # General proof failure
+                  "specifications/MisraReachability/ReachabilityProofs.tla",
+                  "specifications/Paxos/Consensus.tla",
+                  "specifications/PaxosHowToWinATuringAward/Consensus.tla",
+                  "specifications/lamport_mutex/LamportMutex_proofs.tla"
+                )
+                python $EXAMPLES_DIR/.github/scripts/check_proofs.py      \
+                  --tlapm_path $EXAMPLES_DIR/deps/tlapm-install           \
+                  --manifest_path $EXAMPLES_DIR/manifest.json             \
+                  --skip "${SKIP[@]}"
+            - name: Run tests
               run: |
                 eval $(opam env)
+                set +e
                 make test
-            - name: Print Test Results
-              if: matrix.operating-system == 'ubuntu-latest'
-              run: |
+                TEST_RESULT=$?
                 cat _build/default/test/tests.log
+                exit $TEST_RESULT
+
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -1,7 +1,8 @@
 name: Upload installer of TLA Proof Manager
 on:
     push:
-        branches: release_installer_on_github
+        branches:
+          - release_installer_on_github
 jobs:
     release:
             # This task creates a release on GitHub,
@@ -59,23 +60,22 @@ jobs:
         needs: [release]
         runs-on: ${{ matrix.operating-system }}
         strategy:
-            matrix:
-                operating-system: [
-                    macos-latest,
-                    ubuntu-latest]
-                ocaml-compiler: [
-                    '2',
-                    ]
+          matrix:
+            operating-system:
+              - macos-latest,
+              - ubuntu-latest
+            ocaml-compiler:
+              - '2'
         steps:
             - name: Install deps
               if: matrix.operating-system == 'ubuntu-latest'
               run: |
                 sudo apt-get update
                 sudo apt-get install --yes time
             - name: Set up Python
-              uses: actions/setup-python@v2
+              uses: actions/setup-python@v4
               with:
-                python-version: '3.10'
+                python-version: '3.12'
             # Read "Output Release URL and
             # ID File" of `release` job above.
             - name: Load Release URL File from release job
@@ -93,7 +93,7 @@ jobs:
               env:
                 TAG_REF_NAME: ${{ github.ref }}
                 REPOSITORY_NAME: ${{ github.repository }}
-            - uses: actions/checkout@v2
+            - uses: actions/checkout@v3
             - name: Get OCaml version
               run: |
                 INDEX=${{ matrix.ocaml-compiler }}
@@ -117,10 +117,6 @@ jobs:
                 make
                 make release
                 echo "TLAPM_RELEASE_FILE=$(make release-print-file)" >> "$GITHUB_ENV"
-            - name: Run a subset of `tlapm` tests
-              run: |
-                eval $(opam env)
-                make test-inline test-fast-basic
             - name: Upload Release Asset
               if: matrix.ocaml-compiler == '2'
               id: upload-release-asset
@@ -132,3 +128,4 @@ jobs:
                 asset_path: _build/${{ env.TLAPM_RELEASE_FILE }}
                 asset_name: ${{ env.TLAPM_RELEASE_FILE }}
                 asset_content_type: application/octet-stream
+
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.
 

diff --git a/deps/isabelle/Makefile b/deps/isabelle/Makefile
@@ -88,7 +88,7 @@ $(ISABELLE_DIR).no-links: $(ISABELLE_DIR) $(ISABELLE_DIR)/src/TLA+
 # 		flags (or sets on all the files). Here we generate a script to restore the flags.
 Isabelle.post-install: $(ISABELLE_DIR).no-links
 	echo "FILES=$(shell find $(ISABELLE_DIR) -type f $(FIND_EXEC))" > $@
-	echo "all:\n\t chmod +x \$$(FILES)" >> $@
+	echo -e "all:\n\t chmod +x \$$(FILES)" >> $@
 
 clean:
 	rm -rf $(ISABELLE_ARCHIVE) $(ISABELLE_DIR) $(ISABELLE_DIR).no-links Isabelle.post-install