From decd45d8edf579a078862a8fa2d51100ab4cdee0 Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <github.com@lemmster.de>
Date: Mon, 19 Aug 2024 10:57:37 +0200
Subject: [PATCH] Build main/HEAD of Apalache until new official Apalache
 builds are available.

https://github.com/apalache-mc/apalache/issues/2951

[Build]

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
---
 .github/workflows/tla.yml | 27 ++++++++++++++++++++++-----
 1 file changed, 22 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/tla.yml b/.github/workflows/tla.yml
index 44d18f9..038ed40 100644
--- a/.github/workflows/tla.yml
+++ b/.github/workflows/tla.yml
@@ -16,13 +16,30 @@ jobs:
         with:
           distribution: 'microsoft'
           java-version: '17'
-      - name: Setup
+      - name: Install Apalache's scala-sbt build dependency
         run: |
-          wget https://github.com/informalsystems/apalache/releases/latest/download/apalache.tgz
-          tar zxvf apalache.tgz
-      - name: Typecheck
+          ## https://www.scala-sbt.org/1.x/docs/Installing-sbt-on-Linux.html#Ubuntu+and+other+Debian-based+distributions
+          echo "deb https://repo.scala-sbt.org/scalasbt/debian all main" | sudo tee /etc/apt/sources.list.d/sbt.list
+          echo "deb https://repo.scala-sbt.org/scalasbt/debian /" | sudo tee /etc/apt/sources.list.d/sbt_old.list
+          curl -sL "https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x2EE0EA64E40A89B84B2DF73499E82A75642AC823" | sudo -H gpg --no-default-keyring --keyring gnupg-ring:/etc/apt/trusted.gpg.d/scalasbt-release.gpg --import
+          sudo chmod 644 /etc/apt/trusted.gpg.d/scalasbt-release.gpg
+          sudo apt-get update
+          sudo apt-get install sbt --no-install-recommends -y
+      - name: Build Apalache
         run: |
-          ./apalache/bin/apalache-mc typecheck APApbft.tla
+          git clone https://github.com/apalache-mc/apalache.git
+          cd apalache
+          make package ## do not run Apalache's unit tests
+      - name: Type- and (ordinary) invariant checking with Apalache
+        run: |
+          ./apalache/bin/apalache-mc check --config=APApbft.cfg APApbft.tla
+      - name: Upload Apalache's counterexample (if any)
+        uses: actions/upload-artifact@v4
+        if: always()
+        with:
+            path: |
+              _apalache-out/APApbft.tla/
+
   tlc:
     runs-on: ubuntu-latest
     steps: