[Merged by Bors] - perf(ci): use self-hosted runner for bors

.github/workflows/bors.yml

@@ -0,0 +1,196 @@
+# 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:
+      - staging
+
+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
+    steps:
+      - uses: actions/checkout@v2
+
+      - name: install Python
+        if: ${{ ! 1 }}
+        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
+        if: ${{ ! 1 }}
+        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
+        if: ${{ ! 1 }}
+        uses: actions/setup-python@v1
+        with:
+          python-version: 3.8
+
+      - 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
+        if: ${{ ! 1 }}
+        with:
+          distribution: 'adopt'
+          java-version: '16'
+
+      - name: install trepplein
+        run: |
+          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
+
+      - 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

.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:
@@ -10,8 +13,14 @@ 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
+      - 'staging'
+
+name: continuous integration
 
 jobs:
+
+  # Cancels previous runs of jobs in this file
   cancel:
     name: 'Cancel Previous Runs (CI)'
     runs-on: ubuntu-latest
@@ -22,34 +31,14 @@ jobs:
           all_but_latest: true
           access_token: ${{ github.token }}
 
-  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
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v2
 
       - name: install Python
+        if: ${{ ! 0 }}
         uses: actions/setup-python@v2
         with:
           python-version: 3.8
@@ -80,6 +69,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
@@ -174,11 +164,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
@@ -187,18 +179,17 @@ 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'
 
       - 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/