Trigger CI for leanprover/lean4#2484

Author: leanprover-community-mathlib4-bot

.docker/gitpod/Dockerfile

@@ -6,7 +6,7 @@ FROM ubuntu:jammy
 
 USER root
 
-RUN apt-get update && apt-get install sudo git curl git bash-completion python3 -y && apt-get clean
+RUN apt-get update && apt-get install sudo git curl git bash-completion python3 python3-requests -y && apt-get clean
 
 RUN useradd -l -u 33333 -G sudo -md /home/gitpod -s /bin/bash -p gitpod gitpod \
     # passwordless sudo for users in the 'sudo' group

.github/CONTRIBUTING.md

@@ -0,0 +1 @@
+Please see [our contribution guide](https://leanprover-community.github.io/contribute/index.html) on our website.

.github/workflows/bors.yml

@@ -37,11 +37,12 @@ jobs:
 
       - uses: actions/checkout@v3
 
-      - name: Install bibtool
-        if: ${{ 'bors' == 'ubuntu-latest' }}
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y bibtool
+      # Run the case checker action
+      - name: Check Case Sensitivity
+        uses: credfeto/action-case-checker@v1.3.0
+
+      - name: Look for ignored files
+        uses: credfeto/action-no-ignored-files@v1.1.0
 
       - name: install Python
         if: ${{ 'bors' == 'ubuntu-latest' }}
@@ -53,6 +54,12 @@ jobs:
         run: |
           ./scripts/lint-style.sh
 
+      - name: Install bibtool
+        if: ${{ 'bors' == 'ubuntu-latest' }}
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y bibtool
+
       - name: lint references.bib
         run: |
           ./scripts/lint-bib.sh
@@ -91,6 +98,25 @@ jobs:
       - name: check that all files are imported
         run: git diff --exit-code
 
+  check_workflows:
+    if: github.repository == 'leanprover-community/mathlib4'
+    name: check workflows
+    runs-on: ubuntu-latest
+    steps:
+      - name: cleanup
+        run: |
+          find . -name . -o -prune -exec rm -rf -- {} +
+
+      - uses: actions/checkout@v3
+
+      - name: update workflows
+        run: |
+          cd .github/workflows/
+          ./mk_build_yml.sh
+
+      - name: check that workflows were consistent
+        run: git diff --exit-code
+
   build:
     if: github.repository == 'leanprover-community/mathlib4'
     name: Build
@@ -99,6 +125,10 @@ jobs:
       - name: cleanup
         run: |
           find . -name . -o -prune -exec rm -rf -- {} +
+          # Delete all but the 5 most recent toolchains.
+          # Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
+          # Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
+          cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +6 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"' || true
 
       # The Hoskinson runners may not have jq installed, so do that now.
       - name: 'Setup jq'
@@ -107,7 +137,7 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
@@ -126,10 +156,18 @@ jobs:
             elan toolchain uninstall `cat lean-toolchain`
           fi
 
+      - name: print lean and lake versions
+        run: |
+          lean --version
+          lake --version
+
       - name: get cache
         run: |
           lake exe cache clean
-          lake exe cache get
+          # We've been seeing many failures at this step recently because of network errors.
+          # As a band-aid, we try twice.
+          # The 'sleep 1' is small pause to let the network recover.
+          lake exe cache get || (sleep 1; lake exe cache get)
 
       - name: build mathlib
         id: build
@@ -141,50 +179,106 @@ jobs:
 
       - name: check for noisy stdout lines
         run: |
-          ! grep "stdout:" stdout.log
+          ! grep --after-context=1 "stdout:" stdout.log
 
       - name: build library_search cache
         run: lake build -KCI MathlibExtras
 
       - name: upload cache
         if: always()
         run: |
+          # run this in CI if it gets an incorrect lake hash for existing cache files somehow
+          # lake exe cache pack! || true
           lake exe cache commit || true
-          lake exe cache put || true
+          # try twice in case of network errors
+          lake exe cache put || (sleep 1; lake exe cache put) || true
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
 
+      - name: check the cache
+        run: |
+          # Because the `lean-pr-testing-NNNN` branches use toolchains that are "updated in place"
+          # the cache mechanism is unreliable, so we don't test it if we are on such a branch.
+          if [[ ! `cat lean-toolchain` =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
+            lake exe cache get || (sleep 1; lake exe cache get)
+            # We pipe the output of `lake build` to a file,
+            # and if we find " Building Mathlib" in that file we kill `lake build`, and error.
+            lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building Mathlib" && kill $! ))
+          fi
+
       - name: build archive
-        run: lake build Archive
+        run: |
+          # Note: we should not be including `Archive` and `Countexamples` in the cache.
+          # We do this for now for the sake of not rebuilding them in every CI run
+          # even when they are not touched.
+          # Since `Archive` and `Counterexamples` files have very simple dependencies,
+          # it should be possible to determine whether they need to be built without actually
+          # storing and transferring oleans over the network.
+          # Hopefully a future re-implementation of `cache` will obviate the present need for this hack.
+          # We retry twice in case of network errors.
+          lake exe cache get Archive.lean || (sleep 1; lake exe cache get Archive.lean)
+          lake build Archive
+          lake exe cache put Archive.lean || (sleep 1; lake exe cache put Archive.lean)
+        env:
+          MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
 
       - name: build counterexamples
-        run: lake build Counterexamples
+        run: |
+          lake exe cache get Counterexamples.lean || (sleep 1; lake exe cache get Counterexamples.lean)
+          lake build Counterexamples
+          lake exe cache put Counterexamples.lean || (sleep 1; lake exe cache put Counterexamples.lean)
+        env:
+          MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
 
       - name: check declarations in db files
         run: |
           python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
-          build/bin/checkYaml
+          lake exe checkYaml
+
+      - name: verify `lake exe graph` works
+        run: |
+          lake exe graph
+          rm import_graph.dot
 
       - name: test mathlib
         id: test
-        run: make -j 8 test
+        run: |
+          # Tests use parts of ProofWidgets not imported by Mathlib.
+          # Ensure everything has been built.
+          lake build ProofWidgets
+          make -j 8 test
 
       - name: lint mathlib
         id: lint
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
           linters: gcc
-          run: env LEAN_ABORT_ON_PANIC=1 make lint
+          run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib
+
+      - name: check environments using lean4checker
+        id: lean4checker
+        run: |
+          git clone https://github.com/leanprover/lean4checker
+          cd lean4checker
+          git checkout toolchain/v4.3.0
+          # Now that the git hash is embedded in each olean,
+          # we need to compile lean4checker on the same toolchain
+          cp ../lean-toolchain .
+          lake build
+          ./test.sh
+          cd ..
+          lake env lean4checker/.lake/build/bin/lean4checker
 
       - name: Post comments for lean-pr-testing branch
         if: always()
         env:
           TOKEN: ${{ secrets.LEAN_PR_TESTING }}
           GITHUB_CONTEXT: ${{ toJson(github) }}
-          WORKFLOW_URL: ${{ github.event.workflow_run.html_url }}
+          WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
           LINT_OUTCOME: ${{ steps.lint.outcome }}
           TEST_OUTCOME: ${{ steps.test.outcome }}
           BUILD_OUTCOME: ${{ steps.build.outcome }}
+          CHECK_OUTCOME: ${{ steps.lean4checker.outcome }}
         run: |
           scripts/lean-pr-testing-comments.sh