Merge remote-tracking branch 'origin/main' into isabelle2020

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
tlaplus · Dec 21, 2023 · 6a63614 · 6a63614
2 parents 2c3d011 + fe954fc
commit 6a63614
Show file tree

Hide file tree

Showing 487 changed files with 45,951 additions and 49,937 deletions.
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -1,133 +1,67 @@
 name: Build and Package TLA Proof Manager
-on: [push]
-
-## The 'release' job creates an empty Github (draft) release before the 'publish' job
-## below builds and uploads installers into the release.  This complexity is required
-## because the standard Github release action cannot be executed as part of the matrix
-## job (the first runner to create the release wins but the others fail).  In other words,
-## we need a single runner to create the release to which all runners will upload their
-## assets (installers).  Things would be simpler if e.g. Linux could build the installers
-## for all platforms.
+on:
+    push:
+    schedule:
+        - cron: '42 5 5 * *'
 jobs:
-  release:
-    name: Create Github Release
-    runs-on: ubuntu-latest
-    steps:
-    - name: Get current date
-      id: date
-      run: echo "::set-output name=date::$(date +'%Y%m%d%H%M')"
-    - name: Create Github Release
-      id: create_release
-      uses: actions/create-release@v1.1.4
-      env:
-        GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-      with:
-        tag_name: ${{steps.date.outputs.date}}
-        release_name: ${{steps.date.outputs.date}}
-        draft: false
-        prerelease: true
-    ## Remember the release URL and ID so the runners executing 'publish' below
-    ## know where to upload assets.
-    - name: Output Release URL and ID File
-      run: |
-           echo "${{ steps.create_release.outputs.upload_url }}" > release_url.txt
-           echo "${{steps.date.outputs.date}}" > release_id.txt
-    - name: Save Release URL File for publish
-      uses: actions/upload-artifact@v1
-      with:
-        name: release_url
-        path: release_url.txt
-    - name: Save Release ID File for publish
-      uses: actions/upload-artifact@v1
-      with:
-        name: release_id
-        path: release_id.txt
-
-  publish:
-    name: Build and Test
-    needs: [release]
-    runs-on: ${{ matrix.operating-system }}
-    strategy:
-      fail-fast: false
-      matrix:
-        operating-system: [macos-latest, ubuntu-latest]
-        ocaml-compiler: [ '4.08.1', '4.11.0', '4.12.0', '4.13.0' ]
-        include:
-        - operating-system: macos-latest
-          INSTALLER: tlaps-1.5.0-i386-darwin-inst.bin
-          DOWNLOADS: tlaps-1.5.0-i386-darwin-inst
-
-        - operating-system: ubuntu-latest
-          INSTALLER: tlaps-1.5.0-x86_64-linux-gnu-inst.bin
-          DOWNLOADS: tlaps-1.5.0-x86_64-linux-gnu
-    steps:
-      ## See "Output Release URL and ID File" of 'release' job above.
-      - name: Load Release URL File from release job
-        uses: actions/download-artifact@v1
-        with:
-          name: release_url
-      - name: Get Release File Name & Upload URL
-        id: get_release_info
-        run: |
-          echo ::set-output name=file_name::${REPOSITORY_NAME##*/}-${TAG_REF_NAME##*/v} # RepositoryName-v1.0.0
-          value=`cat release_url/release_url.txt`
-          echo ::set-output name=upload_url::$value
-        env:
-          TAG_REF_NAME: ${{ github.ref }}
-          REPOSITORY_NAME: ${{ github.repository }}
-      ## Get TLAPS repository checked out.
-      - uses: actions/checkout@master
-      ## Setup OCaml environment.
-      - uses: ocaml/setup-ocaml@v2
-        with:
-          ocaml-compiler: ${{ matrix.ocaml-compiler }}
-      ## The TLAPM test suite requires the kaputt package.
-      - name: Install OCaml dependencies
-        run: opam install kaputt
-      - uses: actions/cache@v2
-        id: cache
-        with:
-          path: ${{ matrix.DOWNLOADS }}
-          key: ${{ matrix.DOWNLOADS }}
-      ## Create the installer and run the 'fast' test suite as smoke tests before
-      ## installers are uploaded to the Github release.
-      - name: Build and Test TLAPM installer
-        run: |
-            eval $(opam env)
-            ./configure
-            cd tools/installer
-            ./tlaps-release.sh
-            ./${{ matrix.INSTALLER }} -d ../..
-            cd ../..
-            PATH=$(pwd)/bin:$(pwd)/lib/tlaps/bin:$PATH make test
-      - name: Upload Release Asset
-        if: matrix.ocaml-compiler == '4.13.0'
-        id: upload-release-asset
-        uses: actions/upload-release-asset@v1.0.1
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-        with:
-          upload_url: ${{ steps.get_release_info.outputs.upload_url }}
-          asset_path: tools/installer/${{ matrix.INSTALLER }}
-          asset_name: ${{ matrix.INSTALLER }}
-          asset_content_type: application/octet-stream
-      ## Run the full test suite.
-      - name: Download and Test TLAPM installer
-        if: >-
-            matrix.operating-system == 'ubuntu-latest' &&
-            matrix.ocaml-compiler == '4.13.0'
-        ## The test suite has known failures, thus keep going until the
-        ## test suite has been fixed (TODO).
-        continue-on-error: true
-        run: |
-            ls -lah
-            eval $(opam env)
-            ocaml --version
-            make
-            PATH=$(pwd)/bin:$(pwd)/lib/tlaps/bin:$PATH which tlapm
-            PATH=$(pwd)/bin:$(pwd)/lib/tlaps/bin:$PATH which zenon
-            PATH=$(pwd)/bin:$(pwd)/lib/tlaps/bin:$PATH tlapm --version
-            PATH=$(pwd)/bin:$(pwd)/lib/tlaps/bin:$PATH make testall
-      - name: Print Test Results
-        if: matrix.operating-system == 'ubuntu-latest'
-        run: cat test/tests.log
+    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',
+                    ]
+        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
+              with:
+                python-version: '3.10'
+            - uses: actions/checkout@v2
+            - 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 installer of TLAPS
+              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
+              if: >-
+                matrix.operating-system == 'ubuntu-latest' &&
+                matrix.ocaml-compiler == '2'
+              run: |
+                eval $(opam env)
+                make test
+            - name: Print Test Results
+              if: matrix.operating-system == 'ubuntu-latest'
+              run: |
+                cat _build/default/test/tests.log
diff --git a/.github/workflows/ocaml_versions.py b/.github/workflows/ocaml_versions.py
@@ -0,0 +1,33 @@
+"""Array of OCaml versions tested in CI."""
+import argparse
+
+
+OCAML_VERSIONS = [
+    '4.08.1',
+    '4.13.0',
+    '4.14.0',
+    ]
+
+
+def _main():
+    """Entry point."""
+    index = _parse_args()
+    ocaml_version = OCAML_VERSIONS[index]
+    print(ocaml_version)
+
+
+def _parse_args():
+    """Return command-line arguments."""
+    parser = argparse.ArgumentParser()
+    parser.add_argument(
+        'index',
+        help='index in array of OCaml versions, '
+            'to return the corresponding '
+            'OCaml version',
+        type=int)
+    args = parser.parse_args()
+    return args.index
+
+
+if __name__ == '__main__':
+    _main()
diff --git a/.github/workflows/pr.yml b/.github/workflows/pr.yml
@@ -1,51 +1,68 @@
-name: Build and Package TLA Proof Manager
-on: [pull_request]
-
+name: Build on PR
+on:
+    pull_request:
+    push:
+        paths:
+            - '.github/workflows/pr.yml'
+    schedule:
+        - cron: '42 5 20 * *'
 jobs:
-  test:
-    name: Build and Test
-    runs-on: ${{ matrix.operating-system }}
-    strategy:
-      fail-fast: false
-      matrix:
-        operating-system: [macos-latest, ubuntu-latest]
-        ocaml-compiler: [ '4.08.1', '4.11.0', '4.12.0', '4.13.0' ]
-        include:
-        - operating-system: macos-latest
-          INSTALLER: tlaps-1.5.0-i386-darwin-inst.bin
-          DOWNLOADS: tlaps-1.5.0-i386-darwin-inst
-
-        - operating-system: ubuntu-latest
-          INSTALLER: tlaps-1.5.0-x86_64-linux-gnu-inst.bin
-          DOWNLOADS: tlaps-1.5.0-x86_64-linux-gnu
-    steps:
-      ## Get TLAPS repository checked out.
-      - uses: actions/checkout@master
-      ## Setup OCaml environment.
-      - uses: ocaml/setup-ocaml@v2
-        with:
-          ocaml-compiler: ${{ matrix.ocaml-compiler }}
-      ## The TLAPM test suite requires the kaputt package.
-      - name: Install OCaml dependencies
-        run: opam install kaputt
-      - uses: actions/cache@v2
-        id: cache
-        with:
-          path: ${{ matrix.DOWNLOADS }}
-          key: ${{ matrix.DOWNLOADS }}
-      ## Create the installer and run the 'fast' test suite as smoke tests before
-      ## installers are uploaded to the Github release.
-      - name: Build and Test TLAPM installer
-        run: |
-            eval $(opam env)
-            ./configure
-            cd tools/installer
-            ./tlaps-release.sh
-            ./${{ matrix.INSTALLER }} -d ../..
-            cd ../..
-            PATH=$(pwd)/bin:$(pwd)/lib/tlaps/bin:$PATH make test
-            make
-            PATH=$(pwd)/bin:$(pwd)/lib/tlaps/bin:$PATH make testall
-      - name: Print Test Results
-        if: matrix.operating-system == 'ubuntu-latest'
-        run: cat test/tests.log
+    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',
+                    ]
+        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
+              with:
+                python-version: '3.10'
+            - uses: actions/checkout@v2
+            - 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 installer of TLAPS
+              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
+              run: |
+                eval $(opam env)
+                make test
+            - name: Print Test Results
+              if: matrix.operating-system == 'ubuntu-latest'
+              run: |
+                cat _build/default/test/tests.log