ValidationTestSuite/.github/workflows/main.yml at 868e03874b8ae1bdc2c501e771d806584ddf916d · tlaplus/ValidationTestSuite · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
name: Validation Test Suite Report Generation
on:
  repository_dispatch:
    types: [tlaplus-dispatch]
  workflow_dispatch:

jobs:
  validate:
    runs-on: #ubuntu-latest
      group: ubuntu-latest-beefy

    permissions:
      contents: write
      security-events: write

    steps:
      - name: Clone repo
        uses: actions/checkout@v4
        with:
          lfs: true
      - name: Install python
        uses: actions/setup-python@v5
        with:
          python-version: '3.9'
      - name: Install Java
        uses: actions/setup-java@v4
        with:
          distribution: adopt
          java-version: 17
      - name: Get (nightly) TLC
        run: |
            mkdir -p tools/1.8.0
            wget https://nightly.tlapl.us/dist/tla2tools.jar -O tools/1.8.0/tla2tools.jar
      - name: Install testgen dependencies
        run: pip install -r requirements.txt
      - name: Configure App armor profile to allow testgen to use bubblewrap ## https://github.com/DevToys-app/DevToys/issues/1198#issuecomment-2985517203
        run: |
            sudo apt-get update && sudo apt-get install -y bubblewrap uidmap apparmor-profiles apparmor-profiles-extra
            sudo ln -s /usr/share/apparmor/extra-profiles/bwrap-userns-restrict /etc/apparmor.d/bwrap
            sudo apparmor_parser /etc/apparmor.d/bwrap
            bwrap --ro-bind / / --unshare-user --unshare-ipc echo "bwrap successfully configured"
      - name: Run testgen
        run: |
            python -m testgen -o reports/ -s -e --html -x explanation.yaml -w $(nproc) --tlc-jar tools/1.8.0/tla2tools.jar
      - name: Upload report to https://dl.tlapl.us/validation-test-suite for easy access.
        if: always()
        uses: burnett01/rsync-deployments@7.1.0
        with:
          switches: -avzr --delete
          path: reports/
          remote_path: validation-test-suite/1.8.0/
          remote_host: upload.tlapl.us
          remote_user: github
          remote_key: ${{ secrets.INRIA_SSH_PRIVKEY }}
      - name: Compress reports before archiving.
        if: always()
        run: |
            zip -r reports.zip reports/
      - name: Archive generated reports as workflow artifact.
        if: always()
        uses: actions/upload-artifact@v4
        with:
          include-hidden-files: true
          name: TLAplus-Validation-Test-Suite-Report
          path: |
            reports.zip
      - name: Archive generated reports as GitHub Release.
        if: always()
        uses: softprops/action-gh-release@v2
        with:
          tag_name: 'sha-${{ github.sha }}'
          name: 'TLA+ Validation Test Suite Report (git sha: ${{ github.sha }})'
          files: reports.zip
        env:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
      - name: Convert execution report to SARIF
        if: always()
        run: |
            python tools/execution_report_to_sarif.py \
              --execution-report reports/execution/execution.json \
              --sarif-output reports/validation.sarif \
              --summary-output reports/execution-summary.json
      - name: Upload SARIF report
        if: always()
        uses: github/codeql-action/upload-sarif@v4
        with:
          sarif_file: reports/validation.sarif
          category: tlc-validation
      - name: Fail workflow on unexplained deviations
        if: always()
        run: |
            python - <<'PY'
            import json
            import pathlib
            import sys

            p = pathlib.Path("reports/execution-summary.json")
            if not p.exists():
                print("Missing reports/execution-summary.json; failing gate.")
                sys.exit(1)

            d = json.load(p.open())
            print(f"failed_unexplained={d.get('failed_unexplained')}")
            sys.exit(1 if d.get("failed_unexplained", 1) > 0 else 0)
            PY