Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Move simulation to ADO too, and shorten the length of its run to not delay PRs #5827

Merged
merged 9 commits into from
Nov 10, 2023
Merged

Move simulation to ADO too, and shorten the length of its run to not delay PRs #5827

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
21ad8b5
Move simulation to ADO too, and shorten the length of its run to not …
achamayou Nov 10, 2023
c388035
Merge branch 'main' into move_sim_to_ado_and_shorten_run
achamayou Nov 10, 2023
e8cd48f
Can't have jobs with the same names
achamayou Nov 10, 2023
c2ff3b2
Merge branch 'main' into move_sim_to_ado_and_shorten_run
achamayou Nov 10, 2023
0aa1f94
Actually shorten simulations, and report stats
achamayou Nov 10, 2023
f36e1cd
Merge branch 'move_sim_to_ado_and_shorten_run' of https://github.com/…
achamayou Nov 10, 2023
74b169d
Some stats aren't there in all files
achamayou Nov 10, 2023
47aca82
Why copilot, why
achamayou Nov 10, 2023
c382cdd
Might as well add the env var then
achamayou Nov 10, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions .azure-pipelines-templates/matrix.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -157,6 +157,15 @@ jobs:
depends_on:
- configure

- ${{ if eq(parameters.perf_tests, 'run') }}:
- template: simulation.yml
parameters:
target: Virtual
env: ${{ parameters.env.Virtual }}
installExtendedTestingTools: false
depends_on:
- configure

- ${{ if eq(parameters.perf_tests, 'run') }}:
- template: cimetrics.yml
parameters:
Expand Down
30 changes: 30 additions & 0 deletions .azure-pipelines-templates/simulation.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
jobs:
- job: Simulation
displayName: Simulation
variables:
Codeql.SkipTaskAutoInjection: true
skipComponentGovernanceDetection: true

${{ insert }}: ${{ parameters.env }}

steps:
- checkout: self
clean: true
fetchDepth: 1

- script: |
set -ex
sudo apt update
sudo apt install -y default-jre
python3 ./tla/install_deps.py
displayName: Setup

- script: ./tlc.sh -workers auto -simulate -depth 100 consensus/SIMccfraft.tla -dumpTrace tla SIMccfraft.trace.tla -dumpTrace json SIMccfraft.json
achamayou marked this conversation as resolved.
Show resolved Hide resolved
workingDirectory: tla
displayName: Simulation

- task: PublishPipelineArtifact@1
inputs:
artifactName: "Simulation Traces"
targetPath: tla
condition: or(failed(), canceled())
24 changes: 0 additions & 24 deletions .github/workflows/tlaplus.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,30 +10,6 @@ on:
workflow_dispatch:

jobs:
simulation-consensus:
name: Simulation - Consensus
runs-on: ubuntu-latest

steps:
- uses: actions/checkout@v3
- run: python3 ./tla/install_deps.py

- name: SIMccfraft.tla
run: |
cd tla/
./tlc.sh -workers auto -simulate -depth 500 consensus/SIMccfraft.tla -dumpTrace tla SIMccfraft.trace.tla -dumpTrace json SIMccfraft.json
- name: Upload traces in TLA and JSON format
uses: actions/upload-artifact@v3
if: ${{ failure() }}
with:
name: tlc
path: |
tla/consensus/*_TTrace_*.tla
tla/consensus/*_TTrace_*.bin
tla/*.trace.tla
tla/*.json
model-checking-consistency:
name: Model Checking - Consistency
runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub]
Expand Down
Loading