From 4d76a388ff6676a8f8d9b6b41be53507ed5b060a Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 21 Jun 2021 17:24:18 +0200
Subject: [PATCH 01/17] perf(ci): use self-hosted runner for bors

---
 .github/workflows/bors.yml | 177 +++++++++++++++++++++++++++++++++++++
 1 file changed, 177 insertions(+)
 create mode 100644 .github/workflows/bors.yml

diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
new file mode 100644
index 0000000000000..d3a34f770aa6f
--- /dev/null
+++ b/.github/workflows/bors.yml
@@ -0,0 +1,177 @@
+name: continuous integration
+
+on:
+  push:
+    branches:
+      - nael
+
+jobs:
+
+  style_lint:
+    name: Lint style
+    runs-on: self-hosted
+    steps:
+      - uses: actions/checkout@v2
+
+      - name: install Python
+        uses: actions/setup-python@v2
+        with:
+          python-version: 3.8
+
+      - name: lint
+        run: |
+          ./scripts/lint-style.sh
+
+  build:
+    name: Build mathlib
+    runs-on: self-hosted
+    env:
+      # number of commits to check for olean cache
+      GIT_HISTORY_DEPTH: 20
+    outputs:
+      artifact_name: ${{ steps.setup_precompiled.outputs.artifact_name }}
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}
+
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          ~/.elan/bin/lean --version
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+          echo "short_lean_version=$(~/.elan/bin/lean --run scripts/lean_version.lean)" >> $GITHUB_ENV
+
+      # - name: install Python
+      #   uses: actions/setup-python@v1
+      #   with:
+      #     python-version: 3.8
+
+      - name: try to find olean cache
+        run: ./scripts/fetch_olean_cache.sh
+
+      - name: leanpkg build
+        id: build
+        run: |
+          leanpkg configure
+          echo "::set-output name=started::true"
+          lean --json -T100000 --make src | python scripts/detect_errors.py
+          lean --json -T100000 --make src | python scripts/detect_errors.py
+
+      - name: push release to azure
+        if: always() && github.repository == 'leanprover-community/mathlib' && steps.build.outputs.started == 'true'
+        run: |
+          archive_name="$(git rev-parse HEAD).tar.gz"
+          find src/ -name "*.olean" -o -name ".noisy_files" | tar czf "$archive_name" -T -
+          azcopy copy "$archive_name" "${{ secrets.AZURE_SAS_TOKEN }}" --block-size-mb 99 --overwrite false
+          archive_name="$(git rev-parse HEAD).tar.xz"
+          find src/ -name "*.olean" -o -name ".noisy_files" | tar cJf "$archive_name" -T -
+          azcopy copy "$archive_name" "${{ secrets.AZURE_SAS_TOKEN }}" --block-size-mb 99 --overwrite false
+
+      - name: setup precompiled zip file
+        if: always() && steps.build.outputs.started == 'true'
+        id: setup_precompiled
+        run: |
+          touch workspace.tar
+          tar -cf workspace.tar --exclude=*.tar* .
+          git_hash="$(git log -1 --pretty=format:%h)"
+          echo "::set-output name=artifact_name::precompiled-mathlib-$short_lean_version-$git_hash"
+      - name: upload precompiled mathlib zip file
+        if: always() && steps.build.outputs.started == 'true'
+        uses: actions/upload-artifact@v2
+        with:
+          name: ${{ steps.setup_precompiled.outputs.artifact_name }}
+          path: workspace.tar
+
+  lint:
+    name: Lint mathlib
+    runs-on: self-hosted
+    needs: build
+
+    # # skip on master branch
+    # if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
+
+    steps:
+      - name: retrieve build
+        uses: actions/download-artifact@v2
+        with:
+          name: ${{ needs.build.outputs.artifact_name }}
+
+      - name: untar build
+        run: tar -xf workspace.tar
+
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          ~/.elan/bin/lean --version
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: lint
+        run: |
+          ./scripts/mk_all.sh
+          lean --run scripts/lint_mathlib.lean
+
+  tests:
+    name: Run tests
+    runs-on: self-hosted
+    needs: build
+
+    # # skip on master branch
+    # if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
+
+    steps:
+      - name: retrieve build
+        uses: actions/download-artifact@v2
+        with:
+          name: ${{ needs.build.outputs.artifact_name }}
+
+      - name: untar build
+        run: tar -xf workspace.tar
+
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          ~/.elan/bin/lean --version
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      # - name: install Python
+      #   uses: actions/setup-python@v1
+      #   with:
+      #     python-version: 3.8
+
+      # - name: install Python dependencies
+      #   run: python -m pip install --upgrade pip pyyaml
+
+      - name: tests
+        run: |
+          set -o pipefail
+          lean --json -T100000 --make docs archive roadmap test counterexamples | python scripts/detect_errors.py
+
+      # - uses: actions/setup-java@v2
+      #   with:
+      #     distribution: 'adopt'
+      #     java-version: '16'
+
+      - name: install trepplein
+        run: |
+          pushd ..
+          trepplein_version=1.0
+          wget https://github.com/gebner/trepplein/releases/download/v$trepplein_version/trepplein-$trepplein_version.zip
+          unzip trepplein-$trepplein_version.zip
+          echo $PWD/trepplein-$trepplein_version/bin >>$GITHUB_PATH
+          popd
+
+      - name: export as low-level text file
+        run: lean --recursive --export=mathlib.txt src/
+
+      - name: trepplein
+        run: trepplein mathlib.txt
+
+      - name: check declarations in db files
+        run: |
+          python scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
+          bash scripts/mk_all.sh
+          lean --run scripts/yaml_check.lean

From ac304e8f2988bc4bfc93f7d314acc5c7a7b075d7 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 21 Jun 2021 17:28:36 +0200
Subject: [PATCH 02/17] bump

---
 .github/workflows/bors.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
index d3a34f770aa6f..dcc3223b8492f 100644
--- a/.github/workflows/bors.yml
+++ b/.github/workflows/bors.yml
@@ -175,3 +175,4 @@ jobs:
           python scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
           bash scripts/mk_all.sh
           lean --run scripts/yaml_check.lean
+

From 9cddcffe69a4ef9a3c8910782fc17d01a97240ac Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 21 Jun 2021 17:32:47 +0200
Subject: [PATCH 03/17] bump

---
 .github/workflows/build.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index be903c4beaf40..134a64a93eb53 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -10,6 +10,8 @@ on:
       - 'nolints'
       # do not build lean-x.y.z branch used by leanpkg
       - 'lean-3.*'
+      # ignore staging branch used by bors, this is handled by bors.yml
+      - 'nael'
 
 jobs:
   cancel:

From 7b6df354ad45835708197cc471856094e08c3031 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 21 Jun 2021 17:42:29 +0200
Subject: [PATCH 04/17] bump

---
 .github/workflows/bors.yml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
index dcc3223b8492f..1f2cfe8b6bba8 100644
--- a/.github/workflows/bors.yml
+++ b/.github/workflows/bors.yml
@@ -13,10 +13,10 @@ jobs:
     steps:
       - uses: actions/checkout@v2
 
-      - name: install Python
-        uses: actions/setup-python@v2
-        with:
-          python-version: 3.8
+      # - name: install Python
+      #   uses: actions/setup-python@v2
+      #   with:
+      #     python-version: 3.8
 
       - name: lint
         run: |

From b3ee386aca208a383610d039d67478814ba5df59 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 21 Jun 2021 18:30:08 +0200
Subject: [PATCH 05/17] buimp

---
 .github/workflows/bors.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
index 1f2cfe8b6bba8..2cc4b77d909eb 100644
--- a/.github/workflows/bors.yml
+++ b/.github/workflows/bors.yml
@@ -92,6 +92,8 @@ jobs:
     # # skip on master branch
     # if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
 
+    if: false
+
     steps:
       - name: retrieve build
         uses: actions/download-artifact@v2

From 8a0d4e33836c8619d1681b1321323068caac53b8 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 21 Jun 2021 19:42:26 +0200
Subject: [PATCH 06/17] extract cancel job into separate file

---
 .github/workflows/build.yml  | 10 ----------
 .github/workflows/cancel.yml | 12 ++++++++++++
 2 files changed, 12 insertions(+), 10 deletions(-)
 create mode 100644 .github/workflows/cancel.yml

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 134a64a93eb53..d4e4f33cb53f6 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -14,16 +14,6 @@ on:
       - 'nael'
 
 jobs:
-  cancel:
-    name: 'Cancel Previous Runs (CI)'
-    runs-on: ubuntu-latest
-    # timeout-minutes: 3
-    steps:
-      - uses: styfle/cancel-workflow-action@0.9.0
-        with:
-          all_but_latest: true
-          access_token: ${{ github.token }}
-
   lint_self_test:
     name: Ensure the linter works
     runs-on: ${{ matrix.os }}
diff --git a/.github/workflows/cancel.yml b/.github/workflows/cancel.yml
new file mode 100644
index 0000000000000..faba0771a25a2
--- /dev/null
+++ b/.github/workflows/cancel.yml
@@ -0,0 +1,12 @@
+name: cancel previous runs
+
+jobs:
+  cancel:
+    name: 'Cancel Previous Runs (CI)'
+    runs-on: ubuntu-latest
+    # timeout-minutes: 3
+    steps:
+      - uses: styfle/cancel-workflow-action@0.9.0
+        with:
+          all_but_latest: true
+          access_token: ${{ github.token }}

From 5f645123a246fa9726924ee1fbf889c78c0ad947 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 21 Jun 2021 19:45:34 +0200
Subject: [PATCH 07/17] Extract linter self test

---
 .github/workflows/build.yml          | 20 ---------------
 .github/workflows/lint_self_test.yml | 37 ++++++++++++++++++++++++++++
 2 files changed, 37 insertions(+), 20 deletions(-)
 create mode 100644 .github/workflows/lint_self_test.yml

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index d4e4f33cb53f6..034c500a8cd99 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -14,26 +14,6 @@ on:
       - 'nael'
 
 jobs:
-  lint_self_test:
-    name: Ensure the linter works
-    runs-on: ${{ matrix.os }}
-    strategy:
-      fail-fast: false
-      matrix:
-        os: [macos-latest, ubuntu-latest, windows-latest]
-        python-version:
-          - name: 3.8
-          - name: 3.9
-    steps:
-      - uses: actions/checkout@v2
-      - name: Set up Python ${{ matrix.python-version.name }}
-        uses: actions/setup-python@v2
-        with:
-          python-version: ${{ matrix.python-version.name }}
-
-      - name: sanity check the linter
-        run: |
-          ./scripts/lint_style_sanity_test.py
 
   style_lint:
     name: Lint style
diff --git a/.github/workflows/lint_self_test.yml b/.github/workflows/lint_self_test.yml
new file mode 100644
index 0000000000000..fdbe6c5be4988
--- /dev/null
+++ b/.github/workflows/lint_self_test.yml
@@ -0,0 +1,37 @@
+name: linter self test
+
+on:
+  push:
+    branches-ignore:
+      # ignore tmp branches used by bors
+      - 'staging.tmp*'
+      - 'trying.tmp*'
+      - 'staging*.tmp'
+      # ignore nolints
+      - 'nolints'
+      # do not build lean-x.y.z branch used by leanpkg
+      - 'lean-3.*'
+      # ignore staging branch used by bors, this is handled by bors.yml
+      - 'staging'
+
+jobs:
+  lint_self_test:
+    name: Ensure the linter works
+    runs-on: ${{ matrix.os }}
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [macos-latest, ubuntu-latest, windows-latest]
+        python-version:
+          - name: 3.8
+          - name: 3.9
+    steps:
+      - uses: actions/checkout@v2
+      - name: Set up Python ${{ matrix.python-version.name }}
+        uses: actions/setup-python@v2
+        with:
+          python-version: ${{ matrix.python-version.name }}
+
+      - name: sanity check the linter
+        run: |
+          ./scripts/lint_style_sanity_test.py

From f44ffccae1328cfe9ae65fd764ad69248e9f7a54 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 21 Jun 2021 20:02:48 +0200
Subject: [PATCH 08/17] Add script to generate build.yml and bors.yml

---
 .github/workflows/bors.yml        |  64 ++++++-----
 .github/workflows/build.yml       |  15 ++-
 .github/workflows/build.yml.in    | 181 ++++++++++++++++++++++++++++++
 .github/workflows/mk_build_yml.sh |  53 +++++++++
 4 files changed, 285 insertions(+), 28 deletions(-)
 create mode 100644 .github/workflows/build.yml.in
 create mode 100755 .github/workflows/mk_build_yml.sh

diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
index 2cc4b77d909eb..164b2b1d06586 100644
--- a/.github/workflows/bors.yml
+++ b/.github/workflows/bors.yml
@@ -1,9 +1,14 @@
-name: continuous integration
+# DO NOT EDIT THIS FILE!!!
+
+# This file is automatically generated by mk_build_yml.sh
+# Edit build.yml.in instead and run mk_build_yml.sh to update.
 
 on:
   push:
     branches:
-      - nael
+      - staging
+
+name: continuous integration
 
 jobs:
 
@@ -13,10 +18,11 @@ jobs:
     steps:
       - uses: actions/checkout@v2
 
-      # - name: install Python
-      #   uses: actions/setup-python@v2
-      #   with:
-      #     python-version: 3.8
+      - name: install Python
+        if: ! 1
+        uses: actions/setup-python@v2
+        with:
+          python-version: 3.8
 
       - name: lint
         run: |
@@ -36,6 +42,7 @@ jobs:
           fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}
 
       - name: install elan
+        if: ! 1
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -43,10 +50,11 @@ jobs:
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
           echo "short_lean_version=$(~/.elan/bin/lean --run scripts/lean_version.lean)" >> $GITHUB_ENV
 
-      # - name: install Python
-      #   uses: actions/setup-python@v1
-      #   with:
-      #     python-version: 3.8
+      - name: install Python
+        if: ! 1
+        uses: actions/setup-python@v1
+        with:
+          python-version: 3.8
 
       - name: try to find olean cache
         run: ./scripts/fetch_olean_cache.sh
@@ -89,10 +97,8 @@ jobs:
     runs-on: self-hosted
     needs: build
 
-    # # skip on master branch
-    # if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
-
-    if: false
+    # skip on master branch
+    if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
 
     steps:
       - name: retrieve build
@@ -104,6 +110,7 @@ jobs:
         run: tar -xf workspace.tar
 
       - name: install elan
+        if: ! 1
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -120,8 +127,8 @@ jobs:
     runs-on: self-hosted
     needs: build
 
-    # # skip on master branch
-    # if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
+    # skip on master branch
+    if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
 
     steps:
       - name: retrieve build
@@ -133,29 +140,33 @@ jobs:
         run: tar -xf workspace.tar
 
       - name: install elan
+        if: ! 1
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
           ~/.elan/bin/lean --version
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
-      # - name: install Python
-      #   uses: actions/setup-python@v1
-      #   with:
-      #     python-version: 3.8
+      - name: install Python
+        if: ! 1
+        uses: actions/setup-python@v1
+        with:
+          python-version: 3.8
 
-      # - name: install Python dependencies
-      #   run: python -m pip install --upgrade pip pyyaml
+      - name: install Python dependencies
+        if: ! 1
+        run: python -m pip install --upgrade pip pyyaml
 
       - name: tests
         run: |
           set -o pipefail
           lean --json -T100000 --make docs archive roadmap test counterexamples | python scripts/detect_errors.py
 
-      # - uses: actions/setup-java@v2
-      #   with:
-      #     distribution: 'adopt'
-      #     java-version: '16'
+      - uses: actions/setup-java@v2
+        if: ! 1
+        with:
+          distribution: 'adopt'
+          java-version: '16'
 
       - name: install trepplein
         run: |
@@ -177,4 +188,3 @@ jobs:
           python scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
           bash scripts/mk_all.sh
           lean --run scripts/yaml_check.lean
-
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 034c500a8cd99..e217b4a17439f 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -1,4 +1,7 @@
-name: continuous integration
+# DO NOT EDIT THIS FILE!!!
+
+# This file is automatically generated by mk_build_yml.sh
+# Edit build.yml.in instead and run mk_build_yml.sh to update.
 
 on:
   push:
@@ -13,6 +16,8 @@ on:
       # ignore staging branch used by bors, this is handled by bors.yml
       - 'nael'
 
+name: continuous integration
+
 jobs:
 
   style_lint:
@@ -22,6 +27,7 @@ jobs:
       - uses: actions/checkout@v2
 
       - name: install Python
+        if: ! 0
         uses: actions/setup-python@v2
         with:
           python-version: 3.8
@@ -44,6 +50,7 @@ jobs:
           fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}
 
       - name: install elan
+        if: ! 0
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -52,6 +59,7 @@ jobs:
           echo "short_lean_version=$(~/.elan/bin/lean --run scripts/lean_version.lean)" >> $GITHUB_ENV
 
       - name: install Python
+        if: ! 0
         uses: actions/setup-python@v1
         with:
           python-version: 3.8
@@ -110,6 +118,7 @@ jobs:
         run: tar -xf workspace.tar
 
       - name: install elan
+        if: ! 0
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -139,6 +148,7 @@ jobs:
         run: tar -xf workspace.tar
 
       - name: install elan
+        if: ! 0
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -146,11 +156,13 @@ jobs:
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
       - name: install Python
+        if: ! 0
         uses: actions/setup-python@v1
         with:
           python-version: 3.8
 
       - name: install Python dependencies
+        if: ! 0
         run: python -m pip install --upgrade pip pyyaml
 
       - name: tests
@@ -159,6 +171,7 @@ jobs:
           lean --json -T100000 --make docs archive roadmap test counterexamples | python scripts/detect_errors.py
 
       - uses: actions/setup-java@v2
+        if: ! 0
         with:
           distribution: 'adopt'
           java-version: '16'
diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
new file mode 100644
index 0000000000000..6fa1c42815c82
--- /dev/null
+++ b/.github/workflows/build.yml.in
@@ -0,0 +1,181 @@
+
+name: continuous integration
+
+jobs:
+
+  style_lint:
+    name: Lint style
+    runs-on: RUNS_ON
+    steps:
+      - uses: actions/checkout@v2
+
+      - name: install Python
+        if: ! IS_SELF_HOSTED
+        uses: actions/setup-python@v2
+        with:
+          python-version: 3.8
+
+      - name: lint
+        run: |
+          ./scripts/lint-style.sh
+
+  build:
+    name: Build mathlib
+    runs-on: RUNS_ON
+    env:
+      # number of commits to check for olean cache
+      GIT_HISTORY_DEPTH: 20
+    outputs:
+      artifact_name: ${{ steps.setup_precompiled.outputs.artifact_name }}
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}
+
+      - name: install elan
+        if: ! IS_SELF_HOSTED
+        run: |
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          ~/.elan/bin/lean --version
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+          echo "short_lean_version=$(~/.elan/bin/lean --run scripts/lean_version.lean)" >> $GITHUB_ENV
+
+      - name: install Python
+        if: ! IS_SELF_HOSTED
+        uses: actions/setup-python@v1
+        with:
+          python-version: 3.8
+
+      - name: try to find olean cache
+        run: ./scripts/fetch_olean_cache.sh
+
+      - name: leanpkg build
+        id: build
+        run: |
+          leanpkg configure
+          echo "::set-output name=started::true"
+          lean --json -T100000 --make src | python scripts/detect_errors.py
+          lean --json -T100000 --make src | python scripts/detect_errors.py
+
+      - name: push release to azure
+        if: always() && github.repository == 'leanprover-community/mathlib' && steps.build.outputs.started == 'true'
+        run: |
+          archive_name="$(git rev-parse HEAD).tar.gz"
+          find src/ -name "*.olean" -o -name ".noisy_files" | tar czf "$archive_name" -T -
+          azcopy copy "$archive_name" "${{ secrets.AZURE_SAS_TOKEN }}" --block-size-mb 99 --overwrite false
+          archive_name="$(git rev-parse HEAD).tar.xz"
+          find src/ -name "*.olean" -o -name ".noisy_files" | tar cJf "$archive_name" -T -
+          azcopy copy "$archive_name" "${{ secrets.AZURE_SAS_TOKEN }}" --block-size-mb 99 --overwrite false
+
+      - name: setup precompiled zip file
+        if: always() && steps.build.outputs.started == 'true'
+        id: setup_precompiled
+        run: |
+          touch workspace.tar
+          tar -cf workspace.tar --exclude=*.tar* .
+          git_hash="$(git log -1 --pretty=format:%h)"
+          echo "::set-output name=artifact_name::precompiled-mathlib-$short_lean_version-$git_hash"
+      - name: upload precompiled mathlib zip file
+        if: always() && steps.build.outputs.started == 'true'
+        uses: actions/upload-artifact@v2
+        with:
+          name: ${{ steps.setup_precompiled.outputs.artifact_name }}
+          path: workspace.tar
+
+  lint:
+    name: Lint mathlib
+    runs-on: RUNS_ON
+    needs: build
+
+    # skip on master branch
+    if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
+
+    steps:
+      - name: retrieve build
+        uses: actions/download-artifact@v2
+        with:
+          name: ${{ needs.build.outputs.artifact_name }}
+
+      - name: untar build
+        run: tar -xf workspace.tar
+
+      - name: install elan
+        if: ! IS_SELF_HOSTED
+        run: |
+          set -o pipefail
+          curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          ~/.elan/bin/lean --version
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: lint
+        run: |
+          ./scripts/mk_all.sh
+          lean --run scripts/lint_mathlib.lean
+
+  tests:
+    name: Run tests
+    runs-on: RUNS_ON
+    needs: build
+
+    # skip on master branch
+    if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
+
+    steps:
+      - name: retrieve build
+        uses: actions/download-artifact@v2
+        with:
+          name: ${{ needs.build.outputs.artifact_name }}
+
+      - name: untar build
+        run: tar -xf workspace.tar
+
+      - name: install elan
+        if: ! IS_SELF_HOSTED
+        run: |
+          set -o pipefail
+          curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          ~/.elan/bin/lean --version
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: install Python
+        if: ! IS_SELF_HOSTED
+        uses: actions/setup-python@v1
+        with:
+          python-version: 3.8
+
+      - name: install Python dependencies
+        if: ! IS_SELF_HOSTED
+        run: python -m pip install --upgrade pip pyyaml
+
+      - name: tests
+        run: |
+          set -o pipefail
+          lean --json -T100000 --make docs archive roadmap test counterexamples | python scripts/detect_errors.py
+
+      - uses: actions/setup-java@v2
+        if: ! IS_SELF_HOSTED
+        with:
+          distribution: 'adopt'
+          java-version: '16'
+
+      - name: install trepplein
+        run: |
+          pushd ..
+          trepplein_version=1.0
+          wget https://github.com/gebner/trepplein/releases/download/v$trepplein_version/trepplein-$trepplein_version.zip
+          unzip trepplein-$trepplein_version.zip
+          echo $PWD/trepplein-$trepplein_version/bin >>$GITHUB_PATH
+          popd
+
+      - name: export as low-level text file
+        run: lean --recursive --export=mathlib.txt src/
+
+      - name: trepplein
+        run: trepplein mathlib.txt
+
+      - name: check declarations in db files
+        run: |
+          python scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
+          bash scripts/mk_all.sh
+          lean --run scripts/yaml_check.lean
diff --git a/.github/workflows/mk_build_yml.sh b/.github/workflows/mk_build_yml.sh
new file mode 100755
index 0000000000000..1cad94d1d4fb7
--- /dev/null
+++ b/.github/workflows/mk_build_yml.sh
@@ -0,0 +1,53 @@
+#!/usr/bin/env bash
+set -ex
+cd $(dirname "$(realpath "$0")")
+
+header() {
+  cat <<EOF
+# DO NOT EDIT THIS FILE!!!
+
+# This file is automatically generated by mk_build_yml.sh
+# Edit build.yml.in instead and run mk_build_yml.sh to update.
+
+EOF
+}
+
+build_yml() {
+  header
+  cat <<EOF
+on:
+  push:
+    branches-ignore:
+      # ignore tmp branches used by bors
+      - 'staging.tmp*'
+      - 'trying.tmp*'
+      - 'staging*.tmp'
+      - 'nolints'
+      # do not build lean-x.y.z branch used by leanpkg
+      - 'lean-3.*'
+      # ignore staging branch used by bors, this is handled by bors.yml
+      - 'nael'
+EOF
+  include 0 ubuntu-latest
+}
+
+bors_yml() {
+  header
+  cat <<EOF
+on:
+  push:
+    branches:
+      - nael
+EOF
+  include 1 self-hosted
+}
+
+include() {
+  sed "
+    s/IS_SELF_HOSTED/$1/g;
+    s/RUNS_ON/$2/g;
+  " build.yml.in
+}
+
+build_yml > build.yml
+bors_yml > bors.yml

From f87c6965695f73dccb5394eb0de32bb49915551a Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 21 Jun 2021 20:05:25 +0200
Subject: [PATCH 09/17] run mk_build_yml again

---
 .github/workflows/bors.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
index 164b2b1d06586..a0c90f7b54608 100644
--- a/.github/workflows/bors.yml
+++ b/.github/workflows/bors.yml
@@ -6,7 +6,7 @@
 on:
   push:
     branches:
-      - staging
+      - nael
 
 name: continuous integration
 

From 553800d5da0108b7e7c48f2112950cabe0a133a2 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 21 Jun 2021 20:07:10 +0200
Subject: [PATCH 10/17] fix syntax error??

---
 .github/workflows/bors.yml     | 16 ++++++++--------
 .github/workflows/build.yml    | 16 ++++++++--------
 .github/workflows/build.yml.in | 16 ++++++++--------
 3 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
index a0c90f7b54608..26ee9a8297c7f 100644
--- a/.github/workflows/bors.yml
+++ b/.github/workflows/bors.yml
@@ -19,7 +19,7 @@ jobs:
       - uses: actions/checkout@v2
 
       - name: install Python
-        if: ! 1
+        if: ${{ ! 1 }}
         uses: actions/setup-python@v2
         with:
           python-version: 3.8
@@ -42,7 +42,7 @@ jobs:
           fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}
 
       - name: install elan
-        if: ! 1
+        if: ${{ ! 1 }}
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -51,7 +51,7 @@ jobs:
           echo "short_lean_version=$(~/.elan/bin/lean --run scripts/lean_version.lean)" >> $GITHUB_ENV
 
       - name: install Python
-        if: ! 1
+        if: ${{ ! 1 }}
         uses: actions/setup-python@v1
         with:
           python-version: 3.8
@@ -110,7 +110,7 @@ jobs:
         run: tar -xf workspace.tar
 
       - name: install elan
-        if: ! 1
+        if: ${{ ! 1 }}
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -140,7 +140,7 @@ jobs:
         run: tar -xf workspace.tar
 
       - name: install elan
-        if: ! 1
+        if: ${{ ! 1 }}
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -148,13 +148,13 @@ jobs:
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
       - name: install Python
-        if: ! 1
+        if: ${{ ! 1 }}
         uses: actions/setup-python@v1
         with:
           python-version: 3.8
 
       - name: install Python dependencies
-        if: ! 1
+        if: ${{ ! 1 }}
         run: python -m pip install --upgrade pip pyyaml
 
       - name: tests
@@ -163,7 +163,7 @@ jobs:
           lean --json -T100000 --make docs archive roadmap test counterexamples | python scripts/detect_errors.py
 
       - uses: actions/setup-java@v2
-        if: ! 1
+        if: ${{ ! 1 }}
         with:
           distribution: 'adopt'
           java-version: '16'
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index e217b4a17439f..94ad38a70d623 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -27,7 +27,7 @@ jobs:
       - uses: actions/checkout@v2
 
       - name: install Python
-        if: ! 0
+        if: ${{ ! 0 }}
         uses: actions/setup-python@v2
         with:
           python-version: 3.8
@@ -50,7 +50,7 @@ jobs:
           fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}
 
       - name: install elan
-        if: ! 0
+        if: ${{ ! 0 }}
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -59,7 +59,7 @@ jobs:
           echo "short_lean_version=$(~/.elan/bin/lean --run scripts/lean_version.lean)" >> $GITHUB_ENV
 
       - name: install Python
-        if: ! 0
+        if: ${{ ! 0 }}
         uses: actions/setup-python@v1
         with:
           python-version: 3.8
@@ -118,7 +118,7 @@ jobs:
         run: tar -xf workspace.tar
 
       - name: install elan
-        if: ! 0
+        if: ${{ ! 0 }}
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -148,7 +148,7 @@ jobs:
         run: tar -xf workspace.tar
 
       - name: install elan
-        if: ! 0
+        if: ${{ ! 0 }}
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -156,13 +156,13 @@ jobs:
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
       - name: install Python
-        if: ! 0
+        if: ${{ ! 0 }}
         uses: actions/setup-python@v1
         with:
           python-version: 3.8
 
       - name: install Python dependencies
-        if: ! 0
+        if: ${{ ! 0 }}
         run: python -m pip install --upgrade pip pyyaml
 
       - name: tests
@@ -171,7 +171,7 @@ jobs:
           lean --json -T100000 --make docs archive roadmap test counterexamples | python scripts/detect_errors.py
 
       - uses: actions/setup-java@v2
-        if: ! 0
+        if: ${{ ! 0 }}
         with:
           distribution: 'adopt'
           java-version: '16'
diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
index 6fa1c42815c82..d49df79e847d5 100644
--- a/.github/workflows/build.yml.in
+++ b/.github/workflows/build.yml.in
@@ -10,7 +10,7 @@ jobs:
       - uses: actions/checkout@v2
 
       - name: install Python
-        if: ! IS_SELF_HOSTED
+        if: ${{ ! IS_SELF_HOSTED }}
         uses: actions/setup-python@v2
         with:
           python-version: 3.8
@@ -33,7 +33,7 @@ jobs:
           fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}
 
       - name: install elan
-        if: ! IS_SELF_HOSTED
+        if: ${{ ! IS_SELF_HOSTED }}
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -42,7 +42,7 @@ jobs:
           echo "short_lean_version=$(~/.elan/bin/lean --run scripts/lean_version.lean)" >> $GITHUB_ENV
 
       - name: install Python
-        if: ! IS_SELF_HOSTED
+        if: ${{ ! IS_SELF_HOSTED }}
         uses: actions/setup-python@v1
         with:
           python-version: 3.8
@@ -101,7 +101,7 @@ jobs:
         run: tar -xf workspace.tar
 
       - name: install elan
-        if: ! IS_SELF_HOSTED
+        if: ${{ ! IS_SELF_HOSTED }}
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -131,7 +131,7 @@ jobs:
         run: tar -xf workspace.tar
 
       - name: install elan
-        if: ! IS_SELF_HOSTED
+        if: ${{ ! IS_SELF_HOSTED }}
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -139,13 +139,13 @@ jobs:
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
       - name: install Python
-        if: ! IS_SELF_HOSTED
+        if: ${{ ! IS_SELF_HOSTED }}
         uses: actions/setup-python@v1
         with:
           python-version: 3.8
 
       - name: install Python dependencies
-        if: ! IS_SELF_HOSTED
+        if: ${{ ! IS_SELF_HOSTED }}
         run: python -m pip install --upgrade pip pyyaml
 
       - name: tests
@@ -154,7 +154,7 @@ jobs:
           lean --json -T100000 --make docs archive roadmap test counterexamples | python scripts/detect_errors.py
 
       - uses: actions/setup-java@v2
-        if: ! IS_SELF_HOSTED
+        if: ${{ ! IS_SELF_HOSTED }}
         with:
           distribution: 'adopt'
           java-version: '16'

From bcc7abf68168c99f38223cfbd75a404bb2394870 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 21 Jun 2021 20:07:44 +0200
Subject: [PATCH 11/17] cancel: def trigger

---
 .github/workflows/cancel.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.github/workflows/cancel.yml b/.github/workflows/cancel.yml
index faba0771a25a2..1c3a06ba0a09a 100644
--- a/.github/workflows/cancel.yml
+++ b/.github/workflows/cancel.yml
@@ -1,5 +1,8 @@
 name: cancel previous runs
 
+on:
+  push:
+
 jobs:
   cancel:
     name: 'Cancel Previous Runs (CI)'

From 173661e65d0341ef37022afc5b379763ef71eeee Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 21 Jun 2021 20:09:00 +0200
Subject: [PATCH 12/17] Also install elan on nael

---
 .github/workflows/build.yml.in | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
index d49df79e847d5..229590b435e9f 100644
--- a/.github/workflows/build.yml.in
+++ b/.github/workflows/build.yml.in
@@ -33,7 +33,6 @@ jobs:
           fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}
 
       - name: install elan
-        if: ${{ ! IS_SELF_HOSTED }}
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -101,7 +100,6 @@ jobs:
         run: tar -xf workspace.tar
 
       - name: install elan
-        if: ${{ ! IS_SELF_HOSTED }}
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -131,7 +129,6 @@ jobs:
         run: tar -xf workspace.tar
 
       - name: install elan
-        if: ${{ ! IS_SELF_HOSTED }}
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y

From eaaec57b4a09154c3d993ae882b2534025095552 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 21 Jun 2021 20:09:34 +0200
Subject: [PATCH 13/17] run mk_build_yml

---
 .github/workflows/bors.yml  | 3 ---
 .github/workflows/build.yml | 3 ---
 2 files changed, 6 deletions(-)

diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
index 26ee9a8297c7f..700583e94ac4f 100644
--- a/.github/workflows/bors.yml
+++ b/.github/workflows/bors.yml
@@ -42,7 +42,6 @@ jobs:
           fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}
 
       - name: install elan
-        if: ${{ ! 1 }}
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -110,7 +109,6 @@ jobs:
         run: tar -xf workspace.tar
 
       - name: install elan
-        if: ${{ ! 1 }}
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -140,7 +138,6 @@ jobs:
         run: tar -xf workspace.tar
 
       - name: install elan
-        if: ${{ ! 1 }}
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 94ad38a70d623..f8554ef25c5b9 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -50,7 +50,6 @@ jobs:
           fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}
 
       - name: install elan
-        if: ${{ ! 0 }}
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -118,7 +117,6 @@ jobs:
         run: tar -xf workspace.tar
 
       - name: install elan
-        if: ${{ ! 0 }}
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
@@ -148,7 +146,6 @@ jobs:
         run: tar -xf workspace.tar
 
       - name: install elan
-        if: ${{ ! 0 }}
         run: |
           set -o pipefail
           curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y

From 6c25d26ed0cc25ffe80c14afe2f045950973cf48 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 21 Jun 2021 20:19:14 +0200
Subject: [PATCH 14/17] self-hosted runner does not clean up after itself

---
 .github/workflows/bors.yml     | 4 ++--
 .github/workflows/build.yml    | 4 ++--
 .github/workflows/build.yml.in | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
index 700583e94ac4f..7bb912428ce29 100644
--- a/.github/workflows/bors.yml
+++ b/.github/workflows/bors.yml
@@ -96,6 +96,8 @@ jobs:
     runs-on: self-hosted
     needs: build
 
+    if: false
+
     # skip on master branch
     if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
 
@@ -167,12 +169,10 @@ jobs:
 
       - name: install trepplein
         run: |
-          pushd ..
           trepplein_version=1.0
           wget https://github.com/gebner/trepplein/releases/download/v$trepplein_version/trepplein-$trepplein_version.zip
           unzip trepplein-$trepplein_version.zip
           echo $PWD/trepplein-$trepplein_version/bin >>$GITHUB_PATH
-          popd
 
       - name: export as low-level text file
         run: lean --recursive --export=mathlib.txt src/
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index f8554ef25c5b9..366facb1ed72a 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -104,6 +104,8 @@ jobs:
     runs-on: ubuntu-latest
     needs: build
 
+    if: false
+
     # skip on master branch
     if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
 
@@ -175,12 +177,10 @@ jobs:
 
       - name: install trepplein
         run: |
-          pushd ..
           trepplein_version=1.0
           wget https://github.com/gebner/trepplein/releases/download/v$trepplein_version/trepplein-$trepplein_version.zip
           unzip trepplein-$trepplein_version.zip
           echo $PWD/trepplein-$trepplein_version/bin >>$GITHUB_PATH
-          popd
 
       - name: export as low-level text file
         run: lean --recursive --export=mathlib.txt src/
diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
index 229590b435e9f..19edec6d7600c 100644
--- a/.github/workflows/build.yml.in
+++ b/.github/workflows/build.yml.in
@@ -87,6 +87,8 @@ jobs:
     runs-on: RUNS_ON
     needs: build
 
+    if: false
+
     # skip on master branch
     if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
 
@@ -158,12 +160,10 @@ jobs:
 
       - name: install trepplein
         run: |
-          pushd ..
           trepplein_version=1.0
           wget https://github.com/gebner/trepplein/releases/download/v$trepplein_version/trepplein-$trepplein_version.zip
           unzip trepplein-$trepplein_version.zip
           echo $PWD/trepplein-$trepplein_version/bin >>$GITHUB_PATH
-          popd
 
       - name: export as low-level text file
         run: lean --recursive --export=mathlib.txt src/

From cbaf564f685ed3444353674ea08b517e8d2fb337 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 21 Jun 2021 20:20:49 +0200
Subject: [PATCH 15/17] sigh

---
 .github/workflows/bors.yml     | 2 +-
 .github/workflows/build.yml    | 2 +-
 .github/workflows/build.yml.in | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
index 7bb912428ce29..5b3ce0d4ca39e 100644
--- a/.github/workflows/bors.yml
+++ b/.github/workflows/bors.yml
@@ -99,7 +99,7 @@ jobs:
     if: false
 
     # skip on master branch
-    if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
+    # if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
 
     steps:
       - name: retrieve build
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 366facb1ed72a..a407d802d4693 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -107,7 +107,7 @@ jobs:
     if: false
 
     # skip on master branch
-    if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
+    # if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
 
     steps:
       - name: retrieve build
diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
index 19edec6d7600c..342a38d131b4b 100644
--- a/.github/workflows/build.yml.in
+++ b/.github/workflows/build.yml.in
@@ -90,7 +90,7 @@ jobs:
     if: false
 
     # skip on master branch
-    if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
+    # if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
 
     steps:
       - name: retrieve build

From 0d971c871abefd470209e1bc0f7e819cc73b6c39 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 21 Jun 2021 20:23:06 +0200
Subject: [PATCH 16/17] cancel must not be in separate file

---
 .github/workflows/bors.yml     | 11 +++++++++++
 .github/workflows/build.yml    | 11 +++++++++++
 .github/workflows/build.yml.in | 11 +++++++++++
 .github/workflows/cancel.yml   | 15 ---------------
 4 files changed, 33 insertions(+), 15 deletions(-)
 delete mode 100644 .github/workflows/cancel.yml

diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
index 5b3ce0d4ca39e..a197479374537 100644
--- a/.github/workflows/bors.yml
+++ b/.github/workflows/bors.yml
@@ -12,6 +12,17 @@ name: continuous integration
 
 jobs:
 
+  # Cancels previous runs of jobs in this file
+  cancel:
+    name: 'Cancel Previous Runs (CI)'
+    runs-on: ubuntu-latest
+    # timeout-minutes: 3
+    steps:
+      - uses: styfle/cancel-workflow-action@0.9.0
+        with:
+          all_but_latest: true
+          access_token: ${{ github.token }}
+
   style_lint:
     name: Lint style
     runs-on: self-hosted
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index a407d802d4693..ffc5520a6aeda 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -20,6 +20,17 @@ name: continuous integration
 
 jobs:
 
+  # Cancels previous runs of jobs in this file
+  cancel:
+    name: 'Cancel Previous Runs (CI)'
+    runs-on: ubuntu-latest
+    # timeout-minutes: 3
+    steps:
+      - uses: styfle/cancel-workflow-action@0.9.0
+        with:
+          all_but_latest: true
+          access_token: ${{ github.token }}
+
   style_lint:
     name: Lint style
     runs-on: ubuntu-latest
diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
index 342a38d131b4b..a932b05139534 100644
--- a/.github/workflows/build.yml.in
+++ b/.github/workflows/build.yml.in
@@ -3,6 +3,17 @@ name: continuous integration
 
 jobs:
 
+  # Cancels previous runs of jobs in this file
+  cancel:
+    name: 'Cancel Previous Runs (CI)'
+    runs-on: ubuntu-latest
+    # timeout-minutes: 3
+    steps:
+      - uses: styfle/cancel-workflow-action@0.9.0
+        with:
+          all_but_latest: true
+          access_token: ${{ github.token }}
+
   style_lint:
     name: Lint style
     runs-on: RUNS_ON
diff --git a/.github/workflows/cancel.yml b/.github/workflows/cancel.yml
deleted file mode 100644
index 1c3a06ba0a09a..0000000000000
--- a/.github/workflows/cancel.yml
+++ /dev/null
@@ -1,15 +0,0 @@
-name: cancel previous runs
-
-on:
-  push:
-
-jobs:
-  cancel:
-    name: 'Cancel Previous Runs (CI)'
-    runs-on: ubuntu-latest
-    # timeout-minutes: 3
-    steps:
-      - uses: styfle/cancel-workflow-action@0.9.0
-        with:
-          all_but_latest: true
-          access_token: ${{ github.token }}

From fbdedf10c28d3dae559048e20eb194e91e21a9cd Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 21 Jun 2021 20:39:11 +0200
Subject: [PATCH 17/17] move to staging branch;

---
 .github/workflows/bors.yml        | 6 ++----
 .github/workflows/build.yml       | 6 ++----
 .github/workflows/build.yml.in    | 4 +---
 .github/workflows/mk_build_yml.sh | 4 ++--
 4 files changed, 7 insertions(+), 13 deletions(-)

diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
index a197479374537..0f5c743ff995f 100644
--- a/.github/workflows/bors.yml
+++ b/.github/workflows/bors.yml
@@ -6,7 +6,7 @@
 on:
   push:
     branches:
-      - nael
+      - staging
 
 name: continuous integration
 
@@ -107,10 +107,8 @@ jobs:
     runs-on: self-hosted
     needs: build
 
-    if: false
-
     # skip on master branch
-    # if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
+    if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
 
     steps:
       - name: retrieve build
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index ffc5520a6aeda..e15333736f0f6 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -14,7 +14,7 @@ on:
       # do not build lean-x.y.z branch used by leanpkg
       - 'lean-3.*'
       # ignore staging branch used by bors, this is handled by bors.yml
-      - 'nael'
+      - 'staging'
 
 name: continuous integration
 
@@ -115,10 +115,8 @@ jobs:
     runs-on: ubuntu-latest
     needs: build
 
-    if: false
-
     # skip on master branch
-    # if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
+    if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
 
     steps:
       - name: retrieve build
diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
index a932b05139534..324577424645f 100644
--- a/.github/workflows/build.yml.in
+++ b/.github/workflows/build.yml.in
@@ -98,10 +98,8 @@ jobs:
     runs-on: RUNS_ON
     needs: build
 
-    if: false
-
     # skip on master branch
-    # if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
+    if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
 
     steps:
       - name: retrieve build
diff --git a/.github/workflows/mk_build_yml.sh b/.github/workflows/mk_build_yml.sh
index 1cad94d1d4fb7..be357799c7869 100755
--- a/.github/workflows/mk_build_yml.sh
+++ b/.github/workflows/mk_build_yml.sh
@@ -26,7 +26,7 @@ on:
       # do not build lean-x.y.z branch used by leanpkg
       - 'lean-3.*'
       # ignore staging branch used by bors, this is handled by bors.yml
-      - 'nael'
+      - 'staging'
 EOF
   include 0 ubuntu-latest
 }
@@ -37,7 +37,7 @@ bors_yml() {
 on:
   push:
     branches:
-      - nael
+      - staging
 EOF
   include 1 self-hosted
 }