diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
index 0f5c743ff995f..28529365ea3ab 100644
--- a/.github/workflows/bors.yml
+++ b/.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:
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index e15333736f0f6..ea21ea76ead30 100644
--- a/.github/workflows/build.yml
+++ b/.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'
diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
index 324577424645f..1e3e110364271 100644
--- a/.github/workflows/build.yml.in
+++ b/.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,7 +95,7 @@ jobs:
           path: workspace.tar
 
   lint:
-    name: Lint mathlib
+    name: Lint mathlibJOB_NAME
     runs-on: RUNS_ON
     needs: build
 
@@ -102,6 +103,10 @@ jobs:
     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,7 +128,7 @@ jobs:
           lean --run scripts/lint_mathlib.lean
 
   tests:
-    name: Run tests
+    name: Run testsJOB_NAME
     runs-on: RUNS_ON
     needs: build
 
@@ -131,6 +136,10 @@ jobs:
     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:
diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
new file mode 100644
index 0000000000000..836959192d405
--- /dev/null
+++ b/.github/workflows/build_fork.yml
@@ -0,0 +1,216 @@
+# 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.
+
+# Forks of mathlib and other projects should be able to use build_fork.yml directly
+# The jobs in this file run on GitHub-hosted workers and will only be run from external forks
+
+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.*'
+
+name: continuous integration (mathlib forks)
+
+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
+    steps:
+      - uses: styfle/cancel-workflow-action@0.9.0
+        with:
+          all_but_latest: true
+          access_token: ${{ github.token }}
+
+  style_lint:
+    if: github.repository != 'leanprover-community/mathlib'
+    name: Lint style (fork)
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+
+      - name: install Python
+        if: ${{ ! 0 }}
+        uses: actions/setup-python@v2
+        with:
+          python-version: 3.8
+
+      - name: lint
+        run: |
+          ./scripts/lint-style.sh
+
+  build:
+    if: github.repository != 'leanprover-community/mathlib'
+    name: Build mathlib (fork)
+    runs-on: ubuntu-latest
+    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: ${{ ! 0 }}
+        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 (fork)
+    runs-on: ubuntu-latest
+    needs: build
+
+    # skip on master branch
+    if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
+
+    steps:
+      - name: clean build directory
+        if: ${{ 0 }}
+        run: rm -rf ./* ./.??*
+
+      - 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 (fork)
+    runs-on: ubuntu-latest
+    needs: build
+
+    # skip on master branch
+    if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
+
+    steps:
+      - name: clean build directory
+        if: ${{ 0 }}
+        run: rm -rf ./* ./.??*
+
+      - 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: ${{ ! 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
+        run: |
+          set -o pipefail
+          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: |
+          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
diff --git a/.github/workflows/mk_build_yml.sh b/.github/workflows/mk_build_yml.sh
index be357799c7869..e2080b83e9733 100755
--- a/.github/workflows/mk_build_yml.sh
+++ b/.github/workflows/mk_build_yml.sh
@@ -9,12 +9,15 @@ header() {
 # 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
 EOF
 }
 
 build_yml() {
   header
   cat <<EOF
+# The jobs in this file run on self-hosted workers and will not be run from external forks
+
 on:
   push:
     branches-ignore:
@@ -27,27 +30,57 @@ on:
       - 'lean-3.*'
       # ignore staging branch used by bors, this is handled by bors.yml
       - 'staging'
+
+name: continuous integration
 EOF
-  include 0 ubuntu-latest
+  include 1 pr == ""
 }
 
 bors_yml() {
   header
   cat <<EOF
+# 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 (staging)
+EOF
+  include 1 self-hosted == ""
+}
+
+build_fork_yml() {
+  header
+  cat <<EOF
+# The jobs in this file run on GitHub-hosted workers and will only be run from external forks
+
+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.*'
+
+name: continuous integration (mathlib forks)
 EOF
-  include 1 self-hosted
+  include 0 ubuntu-latest != " (fork)"
 }
 
 include() {
   sed "
     s/IS_SELF_HOSTED/$1/g;
     s/RUNS_ON/$2/g;
+    s/MAIN_OR_FORK/$3/g;
+    s/JOB_NAME/$4/g;
   " build.yml.in
 }
 
 build_yml > build.yml
 bors_yml > bors.yml
+build_fork_yml > build_fork.yml
diff --git a/bors.toml b/bors.toml
index 2c38555e25459..84a49233c52b9 100644
--- a/bors.toml
+++ b/bors.toml
@@ -1,4 +1,7 @@
 status = ["Build mathlib", "Lint mathlib", "Run tests", "Lint style"]
+# if you want to use bors in an external fork of mathlib,
+# comment out the first line and uncomment the line below
+# status = ["Build mathlib (fork)", "Lint mathlib (fork)", "Run tests (fork)", "Lint style (fork)"]
 use_squash_merge = true
 timeout_sec = 28800
 block_labels = ["not-ready-to-merge", "WIP", "blocked-by-other-PR"]