Add TLA+ example and CI

.github/workflows/aya.yml

@@ -3,6 +3,8 @@ name: Aya CI
 on:
   push:
     branches: [ main ]
+    paths:
+      - 'aya/**'
   # Allows you to run this workflow manually from the Actions tab
   workflow_dispatch:
 

.github/workflows/lean4.yml

@@ -6,10 +6,14 @@ on:
     branches:
       - main
       - 'v4*'
+    paths:
+      - 'lean4/**'
   pull_request:
     branches:
       - main
       - 'v4*'
+    paths:
+      - 'lean4/**'
 
   # Allows you to run this workflow manually from the Actions tab
   workflow_dispatch:

.github/workflows/tla.yml

@@ -0,0 +1,29 @@
+name: TLA+ CI
+
+on:
+  push:
+    branches: [ main ]
+    paths:
+      - 'tla/**'
+  # Allows you to run this workflow manually from the Actions tab
+  workflow_dispatch:
+
+jobs:
+  tla:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+      - uses: extractions/setup-just@v1
+        with:
+          just-version: 1.35.0
+      - uses: actions/setup-java@v4
+        with:
+          distribution: 'temurin'
+          java-version: '23'
+      - name: check
+        run: |
+            cd tla
+            just install-tla
+            just check pluscal.tla
+

tla/justfile

@@ -0,0 +1,26 @@
+# To use just, run the following command to install:
+# curl --proto '=https' --tlsv1.2 -sSf https://just.systems/install.sh | bash -s -- --to /usr/local/bin/
+# or
+# brew install just
+
+default:
+    just --list
+
+prep-tla:
+    @echo brew install java
+    @echo install https://github.com/tlaplus/vscode-tlaplus
+
+trans SOURCE:
+    java -cp ~/.tla/tla2tools.jar pcal.trans {{SOURCE}}
+
+check SOURCE: (trans SOURCE)
+    java -cp ~/.tla/tla2tools.jar tlc2.TLC {{SOURCE}}
+
+install-tla:
+    #!/usr/bin/env bash
+    mkdir -p ~/.tla
+    cd ~/.tla
+    wget https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar
+    # wget https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/TLAToolbox-1.8.0-macosx.cocoa.x86_64.zip
+    # unzip TLAToolbox-1.8.0-macosx.cocoa.x86_64.zip
+    # mv TLAToolbox.app /Applications

tla/pluscal.tla

@@ -0,0 +1,17 @@
+\* from https://www.learntla.com/core/pluscal.html *\
+---- MODULE pluscal ----
+EXTENDS Integers, TLC
+
+(* --algorithm pluscal
+variables
+ x = 2;
+ y = TRUE;
+
+begin
+  A:
+    x := x + 1;
+  B:
+    x := x + 1;
+    y := FALSE;
+end algorithm; *)
+====