chore(ci): remove unneeded Lean version restrictions

.github/workflows/build.yml

@@ -6,21 +6,16 @@ jobs:
   build:
     name: Build mathlib
     runs-on: ubuntu-latest
-    strategy:
-      matrix:
-        lean_version:
-          - leanprover-community/lean:3.5.1
-      fail-fast: false
     steps:
       - uses: actions/checkout@v2
 
       - 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/elan override set ${{ matrix.lean_version }}
           ~/.elan/bin/lean --version
           echo "::add-path::$HOME/.elan/bin"
+          echo "::set-env name=short_lean_version::$(~/.elan/bin/lean --run scripts/lean_version.lean)"
 
       - name: install azcopy
         run: |
@@ -43,7 +38,7 @@ jobs:
           git config --unset http.https://github.com/.extraheader
 
       - name: push release to azure
-        if: always() && github.repository == 'leanprover-community/mathlib' && github.event_name == 'push' && matrix.lean_version == 'leanprover-community/lean:3.5.1'
+        if: always() && github.repository == 'leanprover-community/mathlib' && github.event_name == 'push'
         run: |
           branch=${GITHUB_REF#refs/heads/}
           git fetch --depth=1 origin-bot $branch
@@ -57,7 +52,7 @@ jobs:
           fi
 
       - name: push release to mathlib-nightly
-        if: github.repository == 'leanprover-community/mathlib' && github.event_name == 'push' && github.ref == 'refs/heads/master' && matrix.lean_version == 'leanprover-community/lean:3.5.1'
+        if: github.repository == 'leanprover-community/mathlib' && github.event_name == 'push' && github.ref == 'refs/heads/master'
         run: ./scripts/deploy_nightly.sh
         env:
           DEPLOY_NIGHTLY_GITHUB_TOKEN: ${{ secrets.DEPLOY_NIGHTLY_GITHUB_TOKEN }}
@@ -66,7 +61,6 @@ jobs:
         id: setup_precompiled
         run: |
           git_hash="$(git log -1 --pretty=format:%h)"
-          short_lean_version="$(echo ${{ matrix.lean_version }} | sed 's/.*://')"
           echo "::set-output name=artifact_name::precompiled-mathlib-$short_lean_version-$git_hash"
       - name: upload precompiled mathlib zip file
         uses: actions/upload-artifact@v1
@@ -96,14 +90,14 @@ jobs:
           python-version: 3.8
 
       - name: generate docs
-        if: github.repository == 'leanprover-community/mathlib' && github.event_name == 'push' && github.ref == 'refs/heads/master' && matrix.lean_version == 'leanprover-community/lean:3.5.1'
+        if: github.repository == 'leanprover-community/mathlib' && github.event_name == 'push' && github.ref == 'refs/heads/master'
         run:
           ./scripts/deploy_docs.sh
         env:
           DEPLOY_NIGHTLY_GITHUB_TOKEN: ${{ secrets.DEPLOY_NIGHTLY_GITHUB_TOKEN }}
 
       - name: update nolints.txt
-        if: github.repository == 'leanprover-community/mathlib' && github.event_name == 'push' && github.ref == 'refs/heads/master' && matrix.lean_version == 'leanprover-community/lean:3.5.1'
+        if: github.repository == 'leanprover-community/mathlib' && github.event_name == 'push' && github.ref == 'refs/heads/master'
         run:
           ./scripts/update_nolints.sh
         env:

scripts/deploy_docs.sh

@@ -6,11 +6,20 @@ set -x
 git_hash="$(git log -1 --pretty=format:%h)"
 git clone https://github.com/leanprover-community/doc-gen.git
 cd doc-gen
+
+# the commit hash in leanpkg.toml is used by doc_gen.
 sed -i "s/rev = \"\S*\"/rev = \"$git_hash\"/" leanpkg.toml
+
 echo -e "builtin_path\npath ./src\npath ../src" > leanpkg.path
 git clone "https://$DEPLOY_NIGHTLY_GITHUB_USER:$DEPLOY_NIGHTLY_GITHUB_TOKEN@github.com/leanprover-community/mathlib_docs.git"
 rm -rf mathlib_docs/docs/
-elan override set leanprover-community/lean:3.5.1
+
+# Force doc_gen project to match the Lean version used in CI.
+# If they are incompatible, something in doc_gen will fail to compile,
+# but this is better than trying to recompile all of mathlib.
+# short_lean_version is of the form 3.5.1 and set earlier in CI.
+elan override set "leanprover-community/lean:$short_lean_version"
+
 python3 -m pip install --upgrade pip
 pip3 install markdown2 toml
 ./gen_docs -w -r "../" -t "mathlib_docs/docs/"

scripts/deploy_nightly.sh

@@ -31,7 +31,8 @@ fi
 
 # Try to update the lean-x.y.z branch on mathlib. This could fail if
 # a subsequent commit has already pushed an update.
-LEAN_VERSION="lean-3.5.1"
+# short_lean_version is of the form 3.5.1, set earlier in CI
+LEAN_VERSION="lean-$short_lean_version"
 
 git push mathlib HEAD:refs/heads/$LEAN_VERSION || \
     echo "mathlib rejected push to branch $LEAN_VERSION; maybe it already has a later version?" >&2