reference-manual/.github/workflows/pr-testing.yml at main · leanprover/reference-manual · 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
on:
    push:
        branches:
            - main
            - "lean-pr-testing-*"

name: "Report PR testing status to the lean4 repository"

jobs:
    build:
        name: Build site and generate HTML
        runs-on: nscloud-ubuntu-22.04-amd64-8x16

        steps:
            - name: Install elan
              run: |
                  set -o pipefail
                  curl -sSfL https://github.com/leanprover/elan/releases/download/v4.2.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
                  ./elan-init -y --default-toolchain none
                  echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

            - uses: actions/checkout@v4

            - name: Lean Version
              run: |
                  lean --version

            - name: Cache .lake
              uses: actions/cache/restore@v4
              with:
                  path: |
                      .lake/packages
                      .lake/build/bin
                      .lake/build/ir
                      .lake/build/lib
                  key:
                      ${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{
                      hashFiles('lake-manifest.json') }}-${{ hashFiles('lakefile.lean') }}-${{
                      github.sha }}
                  restore-keys: |
                      ${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('lakefile.lean') }}-${{ github.sha }}
                      ${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('lakefile.lean') }}
                      ${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-
                      ${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-

            - name: Build
              id: build
              run: |
                  lake build

            - name: Save cache for .lake
              uses: actions/cache/save@v4
              with:
                  path: |
                      .lake/packages
                      .lake/build/bin
                      .lake/build/ir
                      .lake/build/lib
                  key:
                      ${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{
                      hashFiles('lake-manifest.json') }}-${{ hashFiles('lakefile.lean') }}-${{
                      github.sha }}

            - name: Generate HTML (non-release)
              id: generate
              run: |
                  ./generate-html.sh --mode preview

            - name: Report status to Lean PR
              if: always() && github.repository == 'leanprover/reference-manual'
              shell: bash
              env:
                  TOKEN: ${{ secrets.LEAN_PR_TESTING }}
                  GITHUB_CONTEXT: ${{ toJson(github) }}
                  WORKFLOW_URL:
                      https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
                  BUILD_OUTCOME: ${{ steps.build.outcome }}
                  GENERATE_OUTCOME: ${{ steps.generate.outcome }}
                  NIGHTLY_TESTING_REPO: leanprover/reference-manual
              run: |
                  scripts/lean-pr-testing-comments.sh lean