Skip to content
This repository was archived by the owner on Mar 16, 2026. It is now read-only.

Remove tlaplus-smith dependency for now #38

Remove tlaplus-smith dependency for now

Remove tlaplus-smith dependency for now #38

name: Semantic Preservation Test
on:
push:
branches: [ main ]
workflow_dispatch: # Allow manual trigger
jobs:
semantic-preservation:
runs-on: ubuntu-latest
permissions:
contents: read
steps:
- name: Checkout formatter repository
uses: actions/checkout@v6
- name: Checkout tlaplus/Examples repository
uses: actions/checkout@v6
with:
repository: tlaplus/Examples
path: tlaplus-examples
- name: Checkout TLAPS repository
uses: actions/checkout@v6
with:
repository: tlaplus/tlapm
path: tlapm
- name: Checkout Apalache repository
uses: actions/checkout@v6
with:
repository: apalache-mc/apalache
path: apalache
- name: Download Community Modules
run: |
curl -LO https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar
unzip -o CommunityModules-deps.jar -d CommunityModules
- name: Set up JDK 21
uses: actions/setup-java@v5
with:
java-version: '21'
distribution: 'temurin'
- name: Validate Gradle wrapper
uses: gradle/actions/wrapper-validation@v5
- name: Setup Gradle
uses: gradle/actions/setup-gradle@v5
- name: Run semantic preservation tests
run: ./gradlew semanticPreservationTest -Dtlaplus.examples.path=${{ github.workspace }}/tlaplus-examples -DTLA-Library="${{ github.workspace }}/tlapm/library:${{ github.workspace }}/CommunityModules:${{ github.workspace }}/apalache/src/tla"
- name: Upload test results
uses: actions/upload-artifact@v7
if: always()
with:
name: semantic-preservation-results
path: build/test-results/semanticPreservationTest/
retention-days: 30