Skip to content

Performance Tests TLC #120

Performance Tests TLC

Performance Tests TLC #120

Workflow file for this run

name: Performance Tests TLC
on:
workflow_dispatch:
inputs:
git-sha:
description: 'git commit sha'
required: false
default: ''
schedule:
- cron: '53 5 * * 4'
jobs:
build:
runs-on:
- runs-on # required so that RunsOn knows it needs to process the workflow
- cpu=16
- ram=32
- family=c6gd
- image=ubuntu24-full-x64
timeout-minutes: 720
steps:
- uses: actions/checkout@v4
with:
# Number of commits to fetch. 0 indicates all history.
# jgit task nested in customBuild.xml fails without history.
fetch-depth: '0'
ref: ${{ github.event.inputs.git-sha }}
- name: Set up JDK 11
uses: actions/setup-java@v2
with:
distribution: 'zulu'
java-version: '11'
java-package: jdk # optional (jdk or jre) - defaults to jdk
##
## Build TLC tla2tools.
##
- name: Build TLC
run: |
ant -f tlatools/org.lamport.tlatools/customBuild.xml info compile compile-test dist
- name: Download artifact from previous performance test
uses: dawidd6/action-download-artifact@v7
continue-on-error: true
with:
workflow: perf.yml
name: perf-results
path: previous
##
## Fetch CommunityModules.
##
- name: Fetch CommunityModules
run: |
wget https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar --output-document=tlatools/org.lamport.tlatools/dist/CommunityModules-deps.jar
##
## Run performance regression tests.
## Appends to a older out_run-stats.csv if it exists (cp ... is a no-op otherwise)
##
- name: Run performance tests
run: |
cp previous/out_run-stats.csv general/performance/ || :
cd general/performance
java -jar ../../tlatools/org.lamport.tlatools/dist/tla2tools.jar -config measure.tla measure.tla
##
## Upload results.
##
- name: Upload artifact
uses: actions/upload-artifact@v4
with:
name: perf-results
path: general/performance/out_run*