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 · Oct 29, 2023 · 6918ead · 6918ead
1 parent 5a56e60
commit 6918ead
Show file tree

Hide file tree

Showing 5 changed files with 70 additions and 41 deletions.
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -1,8 +1,8 @@
 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
@@ -24,10 +24,10 @@ jobs:
                 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.11'
+            - uses: actions/checkout@v3
             - name: Get OCaml version
               run: |
                 INDEX=${{ matrix.ocaml-compiler }}
@@ -44,17 +44,13 @@ 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
-              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'
@@ -65,3 +61,27 @@ jobs:
               if: matrix.operating-system == 'ubuntu-latest'
               run: |
                 cat _build/default/test/tests.log
+            - name: Set up build server SSH key
+              if: matrix.ocaml-compiler == '2'
+              run: |
+                mkdir -p ~/.ssh
+                echo "$INRIA_SSH_PRIVKEY" > ~/.ssh/id_rsa
+                chmod 600 ~/.ssh/id_rsa
+              shell: bash
+              env:
+                INRIA_SSH_PRIVKEY: ${{ secrets.INRIA_SSH_PRIVKEY }}
+            - name: Upload to nightly build server
+              if: matrix.ocaml-compiler == '2'
+              run: |
+                # File paths examples, including git commit hash:
+                # ./_build/tlaps-f0b3919-x86_64-darwin.tar.gz
+                # ./_build/tlaps-f0b3919-x86_64-linux-gnu.tar.gz
+                mv _build/tlaps*.tar.gz "_build/tlaps-x86_64-${{ runner.os }}.tar.gz"
+                rsync -e "ssh -o StrictHostKeyChecking=no -i ~/.ssh/id_rsa" --delete -av "_build/tlaps-x86_64-{{ runner.os }}.tar.gz" [email protected]:dist/
+            - name: Trigger run of tlaplus/examples CI
+              if: matrix.ocaml-compiler == '2'
+              uses: peter-evans/repository-dispatch@v1
+              with:
+                  token: ${{ secrets.DISPATCH_ACCESS_TOKEN }}
+                  repository: tlaplus/examples
+                  event-type: tlapm-dispatch
diff --git a/.github/workflows/pr.yml b/.github/workflows/pr.yml
@@ -1,11 +1,5 @@
 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
@@ -28,10 +22,11 @@ jobs:
                 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.11'
+            - name: Clone repo
+              uses: actions/checkout@v3
             - name: Get OCaml version
               run: |
                 INDEX=${{ matrix.ocaml-compiler }}
@@ -48,21 +43,34 @@ 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
+                python $EXAMPLES_DIR/.github/scripts/check_proofs.py \
+                  --tlapm_path $EXAMPLES_DIR/deps/tlapm-install      \
+                  --manifest_path $EXAMPLES_DIR/manifest.json
+            - name: Run tests
               run: |
                 eval $(opam env)
+                set +e
                 make test
-            - name: Print Test Results
-              if: matrix.operating-system == 'ubuntu-latest'
-              run: |
+                result=$?
                 cat _build/default/test/tests.log
+                exit $result
+
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -73,9 +73,9 @@ jobs:
                 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.11'
             # 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

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