iris-lean/.github/workflows/build.yml at master · leanprover-community/iris-lean · 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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
name: Build Iris Lean

on:
  push:
    branches: ["master"]
  pull_request:
    branches: ["master"]
  workflow_dispatch:

# Allow deployment to GitHub Pages
permissions:
  contents: read
  pages: write
  id-token: write

jobs:
  build:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
      - uses: leanprover/lean-action@v1
        with:
          lake-package-directory: Iris
          build-args: "--wfail"
      - name: Dump porting data
        working-directory: Iris
        run: lake exe dumpPortingData
      - name: Upload porting_data.json
        uses: actions/upload-artifact@v7
        with:
          name: porting-data
          path: Iris/.lake/porting_data.json
          retention-days: 1

  build-math:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
      - uses: leanprover/lean-action@v1
        with:
          lake-package-directory: IrisMath
          use-mathlib-cache: true
          build-args: "--wfail"

  report:
    needs: build
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
      - name: Download porting_data.json
        uses: actions/download-artifact@v8
        with:
          name: porting-data
          path: Iris/.lake
      - name: Read Rocq commit from revision file
        id: rocq-commit
        run: |
          sha=$(cat scripts/ROCQ_REVISION)
          echo "sha=$sha" >> "$GITHUB_OUTPUT"
      - name: Cache Rocq definitions
        uses: actions/cache@v6
        with:
          path: Iris/.lake/iris-rocq-cache
          key: rocq-defs-${{ steps.rocq-commit.outputs.sha }}
      - name: Generate porting report
        run: |
          mkdir -p _site
          python3 scripts/check_porting.py --no-build --format html --lean-rev "${{ github.sha }}" -o _site/index.html
      - name: Upload Pages artifact
        uses: actions/upload-pages-artifact@v5

  check-stale:
    if: github.event_name == 'pull_request' && github.event.pull_request.draft == false
    needs: build
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
      - name: Download porting_data.json
        uses: actions/download-artifact@v8
        with:
          name: porting-data
          path: Iris/.lake
      - name: Read pinned Rocq commit
        id: rocq-commit
        run: |
          sha=$(cat scripts/ROCQ_REVISION)
          echo "sha=$sha" >> "$GITHUB_OUTPUT"
      - name: Cache Rocq definitions
        uses: actions/cache@v6
        with:
          path: Iris/.lake/iris-rocq-cache
          key: rocq-defs-${{ steps.rocq-commit.outputs.sha }}
      - name: Generate stale report
        run: |
          python3 scripts/check_porting.py \
            --no-build \
            --format stale \
            --rocq-commit "${{ steps.rocq-commit.outputs.sha }}" \
            --lean-rev "${{ github.event.pull_request.head.sha }}" \
            -o stale-report.txt
      - name: Write job summary and fail if stale
        run: |
          set -euo pipefail
          {
            echo "## Stale porting entries"
            echo ""
            echo '```'
            cat stale-report.txt
            echo '```'
          } >> "$GITHUB_STEP_SUMMARY"
          if grep -q '^No stale entries\.$' stale-report.txt; then
            echo "No stale entries."
            exit 0
          fi
          echo "::error::Stale porting entries detected; see the job summary for the report."
          exit 1

  deploy:
     # we disable deploy for forks to prevent spurious CI failures
    if: github.ref == 'refs/heads/master' && github.repository == 'leanprover-community/iris-lean'
    needs: report
    runs-on: ubuntu-latest
    permissions:
      pages: write
      id-token: write
    environment:
      name: github-pages
      url: ${{ steps.deployment.outputs.page_url }}
    steps:
      - name: Deploy to GitHub Pages
        id: deployment
        uses: actions/deploy-pages@v5