reference-manual/.github/workflows/merge-main-nightly.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
# This job merges every commit to `main` into `nightly-testing`, resolving merge conflicts in favor of `nightly-testing`.

name: Merge main to nightly

on:
    schedule:
        - cron: "30 9/6 * * *"
        # Run every six hours, starting at 10:30AM CET/1:30AM PT.
        # This is 30 minutes prior to attempting to update the toolchain.
    workflow_dispatch:

env:
    TARGET_BRANCH: nightly-testing

jobs:
    merge-to-nightly:
        runs-on: nscloud-ubuntu-22.04-amd64-8x16
        if: github.repository == 'leanprover/reference-manual'
        steps:
            - name: Checkout repository
              uses: actions/checkout@v4
              with:
                  ref: ${{ env.TARGET_BRANCH }}
                  fetch-depth: 0
                  token: ${{ secrets.GITHUB_TOKEN }}

            - name: Configure Git
              run: |
                  git config user.name "github-actions[bot]"
                  git config user.email "github-actions[bot]@users.noreply.github.com"

            - name: Merge main, favoring nightly changes
              run: |
                  git checkout ${{ env.TARGET_BRANCH }}
                  # If the merge goes badly, we proceed anyway via '|| true'.
                  git merge origin/main --strategy-option ours --no-commit --allow-unrelated-histories || true

            - 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"

            - name: Update dependencies
              run: |
                  lake --keep-toolchain update

            - name: Build
              run: |
                  lake build

            - name: Generate HTML
              run: |
                  ./generate-html.sh --mode preview

            - name: Commit and push
              run: |
                  git add .
                  # If there's nothing to do (because there are no new commits from main),
                  # that's okay, hence the '|| true'.
                  git commit -m "chore: merge main into ${{ env.TARGET_BRANCH }}" || true
                  git push origin ${{ env.TARGET_BRANCH }}