ci(.github/workflows/*): switch to self-hosted runners (#8177)

With this PR, mathlib builds on all branches will use the self-hosted runners that have the "pr" tag. One self-hosted runner is reserved for bors staging branch builds and does not have that tag.

The `build_fork` workflow has been added for use by external forks (and other Lean projects which might want to copy mathlib's CI).



Co-authored-by: Gabriel Ebner <gebner@gebner.org>

.github/workflows/bors.yml

@@ -3,17 +3,21 @@
 # This file is automatically generated by mk_build_yml.sh
 # Edit build.yml.in instead and run mk_build_yml.sh to update.
 
+# Forks of mathlib and other projects should be able to use build_fork.yml directly
+# The jobs in this file run on self-hosted workers and will not be run from external forks
+
 on:
   push:
     branches:
       - staging
 
-name: continuous integration
+name: continuous integration (staging)
 
 jobs:
 
   # Cancels previous runs of jobs in this file
   cancel:
+    if: github.repository == 'leanprover-community/mathlib'
     name: 'Cancel Previous Runs (CI)'
     runs-on: ubuntu-latest
     # timeout-minutes: 3
@@ -24,6 +28,7 @@ jobs:
           access_token: ${{ github.token }}
 
   style_lint:
+    if: github.repository == 'leanprover-community/mathlib'
     name: Lint style
     runs-on: self-hosted
     steps:
@@ -40,6 +45,7 @@ jobs:
           ./scripts/lint-style.sh
 
   build:
+    if: github.repository == 'leanprover-community/mathlib'
     name: Build mathlib
     runs-on: self-hosted
     env:
@@ -111,6 +117,10 @@ jobs:
     if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
 
     steps:
+      - name: clean build directory
+        if: ${{ 1 }}
+        run: rm -rf ./* ./.??*
+
       - name: retrieve build
         uses: actions/download-artifact@v2
         with:
@@ -140,6 +150,10 @@ jobs:
     if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
 
     steps:
+      - name: clean build directory
+        if: ${{ 1 }}
+        run: rm -rf ./* ./.??*
+
       - name: retrieve build
         uses: actions/download-artifact@v2
         with:

.github/workflows/build.yml

@@ -3,6 +3,9 @@
 # This file is automatically generated by mk_build_yml.sh
 # Edit build.yml.in instead and run mk_build_yml.sh to update.
 
+# Forks of mathlib and other projects should be able to use build_fork.yml directly
+# The jobs in this file run on self-hosted workers and will not be run from external forks
+
 on:
   push:
     branches-ignore:
@@ -22,6 +25,7 @@ jobs:
 
   # Cancels previous runs of jobs in this file
   cancel:
+    if: github.repository == 'leanprover-community/mathlib'
     name: 'Cancel Previous Runs (CI)'
     runs-on: ubuntu-latest
     # timeout-minutes: 3
@@ -32,13 +36,14 @@ jobs:
           access_token: ${{ github.token }}
 
   style_lint:
+    if: github.repository == 'leanprover-community/mathlib'
     name: Lint style
-    runs-on: ubuntu-latest
+    runs-on: pr
     steps:
       - uses: actions/checkout@v2
 
       - name: install Python
-        if: ${{ ! 0 }}
+        if: ${{ ! 1 }}
         uses: actions/setup-python@v2
         with:
           python-version: 3.8
@@ -48,8 +53,9 @@ jobs:
           ./scripts/lint-style.sh
 
   build:
+    if: github.repository == 'leanprover-community/mathlib'
     name: Build mathlib
-    runs-on: ubuntu-latest
+    runs-on: pr
     env:
       # number of commits to check for olean cache
       GIT_HISTORY_DEPTH: 20
@@ -69,7 +75,7 @@ jobs:
           echo "short_lean_version=$(~/.elan/bin/lean --run scripts/lean_version.lean)" >> $GITHUB_ENV
 
       - name: install Python
-        if: ${{ ! 0 }}
+        if: ${{ ! 1 }}
         uses: actions/setup-python@v1
         with:
           python-version: 3.8
@@ -112,13 +118,17 @@ jobs:
 
   lint:
     name: Lint mathlib
-    runs-on: ubuntu-latest
+    runs-on: pr
     needs: build
 
     # skip on master branch
     if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
 
     steps:
+      - name: clean build directory
+        if: ${{ 1 }}
+        run: rm -rf ./* ./.??*
+
       - name: retrieve build
         uses: actions/download-artifact@v2
         with:
@@ -141,13 +151,17 @@ jobs:
 
   tests:
     name: Run tests
-    runs-on: ubuntu-latest
+    runs-on: pr
     needs: build
 
     # skip on master branch
     if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
 
     steps:
+      - name: clean build directory
+        if: ${{ 1 }}
+        run: rm -rf ./* ./.??*
+
       - name: retrieve build
         uses: actions/download-artifact@v2
         with:
@@ -164,13 +178,13 @@ jobs:
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
       - name: install Python
-        if: ${{ ! 0 }}
+        if: ${{ ! 1 }}
         uses: actions/setup-python@v1
         with:
           python-version: 3.8
 
       - name: install Python dependencies
-        if: ${{ ! 0 }}
+        if: ${{ ! 1 }}
         run: python -m pip install --upgrade pip pyyaml
 
       - name: tests
@@ -179,7 +193,7 @@ jobs:
           lean --json -T100000 --make docs archive roadmap test counterexamples | python scripts/detect_errors.py
 
       - uses: actions/setup-java@v2
-        if: ${{ ! 0 }}
+        if: ${{ ! 1 }}
         with:
           distribution: 'adopt'
           java-version: '16'

.github/workflows/build.yml.in

@@ -1,10 +1,9 @@
 
-name: continuous integration
-
 jobs:
 
   # Cancels previous runs of jobs in this file
   cancel:
+    if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib'
     name: 'Cancel Previous Runs (CI)'
     runs-on: ubuntu-latest
     # timeout-minutes: 3
@@ -15,7 +14,8 @@ jobs:
           access_token: ${{ github.token }}
 
   style_lint:
-    name: Lint style
+    if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib'
+    name: Lint styleJOB_NAME
     runs-on: RUNS_ON
     steps:
       - uses: actions/checkout@v2
@@ -31,7 +31,8 @@ jobs:
           ./scripts/lint-style.sh
 
   build:
-    name: Build mathlib
+    if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib'
+    name: Build mathlibJOB_NAME
     runs-on: RUNS_ON
     env:
       # number of commits to check for olean cache
@@ -94,14 +95,18 @@ jobs:
           path: workspace.tar
 
   lint:
-    name: Lint mathlib
+    name: Lint mathlibJOB_NAME
     runs-on: RUNS_ON
     needs: build
 
     # skip on master branch
     if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
 
     steps:
+      - name: clean build directory
+        if: ${{ IS_SELF_HOSTED }}
+        run: rm -rf ./* ./.??*
+
       - name: retrieve build
         uses: actions/download-artifact@v2
         with:
@@ -123,14 +128,18 @@ jobs:
           lean --run scripts/lint_mathlib.lean
 
   tests:
-    name: Run tests
+    name: Run testsJOB_NAME
     runs-on: RUNS_ON
     needs: build
 
     # skip on master branch
     if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
 
     steps:
+      - name: clean build directory
+        if: ${{ IS_SELF_HOSTED }}
+        run: rm -rf ./* ./.??*
+
       - name: retrieve build
         uses: actions/download-artifact@v2
         with: