From 5e71b24db228d2b7ef4d25e4cbaadb3e80206912 Mon Sep 17 00:00:00 2001 From: Andrew Helwer <2n8rn1w1f@mozmail.com> Date: Fri, 27 Oct 2023 11:17:55 -0400 Subject: [PATCH] Use tlaplus/examples for tests Unified main/pr workflows Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com> --- .github/workflows/ci.yml | 103 ++++++++++++++++++++++++++++ .github/workflows/main.yml | 67 ------------------ .github/workflows/ocaml_versions.py | 5 +- .github/workflows/pr.yml | 68 ------------------ 4 files changed, 105 insertions(+), 138 deletions(-) create mode 100644 .github/workflows/ci.yml delete mode 100644 .github/workflows/main.yml delete mode 100644 .github/workflows/pr.yml diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 00000000..6797264d --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,103 @@ +name: Build & Test +on: + pull_request: + branches: [main] + 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: Run tests + run: | + eval $(opam env) + set +e + make test + TEST_RESULT=$? + cat _build/default/test/tests.log + exit $TEST_RESULT + - 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/bcastByz/bcastByz.tla" + "specifications/byzpaxos/Consensus.tla" + "specifications/byzpaxos/VoteProof.tla" + "specifications/ewd998/AsyncTerminationDetection_proof.tla" + "specifications/ewd998/EWD998_proof.tla" + "specifications/LearnProofs/FindHighest.tla" + "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 + "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[@]}" + diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml deleted file mode 100644 index c01dc056..00000000 --- a/.github/workflows/main.yml +++ /dev/null @@ -1,67 +0,0 @@ -name: Build and Package TLA Proof Manager -on: - push: - schedule: - - cron: '42 5 5 * *' -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', - ] - 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 index d7229ea9..339e6e2c 100644 --- 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 deleted file mode 100644 index baafc9af..00000000 --- a/.github/workflows/pr.yml +++ /dev/null @@ -1,68 +0,0 @@ -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: [ - '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