Merge branch 'master' into transcendental

.docker/gitpod-blueprint/Dockerfile

@@ -0,0 +1,47 @@
+# This is the Dockerfile for `leanprovercommunity/gitpod4-blueprint`.
+# As well as elan, we also install leanblueprint and all of its dependencies.
+
+# This container does not come with a pre-installed version of mathlib.
+# When a gitpod container is spawned, elan will be updated and mathlib will be downloaded:
+# see the .gitpod.yml file for more information.
+
+FROM ubuntu:jammy
+
+USER root
+
+ENV DEBIAN_FRONTEND=noninteractive
+RUN apt-get update && apt-get install sudo git curl git bash-completion texlive texlive-xetex latexmk graphviz graphviz-dev python3 python3-pip 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
+    && sed -i.bkp -e 's/%sudo\s\+ALL=(ALL\(:ALL\)\?)\s\+ALL/%sudo ALL=NOPASSWD:ALL/g' /etc/sudoers
+USER gitpod
+WORKDIR /home/gitpod
+
+SHELL ["/bin/bash", "-c"]
+
+# gitpod bash prompt
+RUN { echo && echo "PS1='\[\033[01;32m\]\u\[\033[00m\] \[\033[01;34m\]\w\[\033[00m\]\$(__git_ps1 \" (%s)\") $ '" ; } >> .bashrc
+
+# install elan
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+
+# install whichever toolchain mathlib is currently using
+RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain)
+
+# install neovim (for any lean.nvim user), via tarball since the appimage doesn't work for some reason, and jammy's version is ancient
+RUN curl -s -L https://github.com/neovim/neovim/releases/download/stable/nvim-linux64.tar.gz | tar xzf - && sudo mv nvim-linux64 /opt/nvim
+
+ENV PATH="/home/gitpod/.local/bin:/home/gitpod/.elan/bin:/opt/nvim/bin:${PATH}"
+
+# install leanblueprint
+RUN python3 -m pip install leanblueprint invoke
+
+# fix the infoview when the container is used on gitpod:
+ENV VSCODE_API_VERSION="1.50.0"
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true
+
+# run sudo once to suppress usage info
+RUN sudo echo finished

.docker/gitpod/Dockerfile

@@ -1,12 +1,15 @@
-# This is the Dockerfile for `leanprovercommunity/mathlib:gitpod`.
+# This is the Dockerfile for `leanprovercommunity/gitpod4`.
+
+# This container does not come with a pre-installed version of mathlib.
+# When a gitpod container is spawned, elan will be updated and mathlib will be downloaded:
+# see the .gitpod.yml file for more information.
 
-# gitpod doesn't support multiple FROM statements, (or rather, you can't copy from one to another)
-# so we just install everything in one go
 FROM ubuntu:jammy
 
 USER root
 
-RUN apt-get update && apt-get install sudo git curl git bash-completion python3 python3-requests -y && apt-get clean
+ENV DEBIAN_FRONTEND=noninteractive
+RUN apt-get update && apt-get install sudo git curl git bash-completion python3 python3-pip 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

.docker/lean/Dockerfile

@@ -0,0 +1,36 @@
+# This is the Dockerfile for `leanprovercommunity/lean4`.
+# It is based on the generic `debian` image, and installs `elan` and the current stable version of `lean`.
+
+# This container does not come with a pre-installed version of mathlib;
+# you should call `lake exe cache get` which will download the most recent version.
+# The only difference between this Dockerfile and leanprovercommunity/lean4 is that this image
+# bypasses a warning that could occur when trying to connect to github for the first time.
+
+# NOTE: to run this docker image on macos or windows,
+# you will need to increase the allowed memory (in the docker GUI) beyond 2GB
+
+FROM debian
+USER root
+# install prerequisites
+RUN apt-get update && apt-get install curl git -y && apt-get clean
+# create a non-root user
+RUN useradd -m lean
+
+USER lean
+WORKDIR /home/lean
+
+SHELL ["/bin/bash", "-c"]
+# set the entrypoint to be a login shell, so everything is on the PATH
+ENTRYPOINT ["/bin/bash", "-l"]
+
+# make sure binaries are available even in non-login shells
+ENV PATH="/home/lean/.elan/bin:/home/lean/.local/bin:$PATH"
+
+# install elan
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none && \
+    . ~/.profile && \
+    elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/leanpkg.toml | grep lean_version | awk -F'"' '{print $2}') && \
+    elan default stable
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true

.github/build.in.yml

@@ -133,8 +133,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get #Mathlib.Init
-          #lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          lake exe cache get Mathlib.Init
+          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
@@ -240,10 +240,20 @@ jobs:
           python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
           lake exe check-yaml
 
-      - name: verify `lake exe graph` works
-        run: |
-          lake exe graph
-          rm import_graph.dot
+      - name: generate our import graph
+        run: lake exe graph
+
+      - name: upload the import graph
+        uses: actions/upload-artifact@v4
+        with:
+          name: import-graph
+          path: import_graph.dot
+          ## the default is 90, but we build often, so unless there's a reason
+          ## to care about old copies in the future, just say 7 days for now
+          retention-days: 7
+
+      - name: clean up the import graph file
+        run: rm import_graph.dot
 
       - name: build everything
         # make sure everything is available for test/import_all.lean
@@ -294,6 +304,23 @@ jobs:
           scripts/lean-pr-testing-comments.sh lean
           scripts/lean-pr-testing-comments.sh batteries
 
+      - name: build lean4checker, but don't run it
+        if: ${{ (always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure') && contains(github.event.pull_request.changed_files, 'lean-toolchain') }}
+        run: |
+          git clone https://github.com/leanprover/lean4checker
+          cd lean4checker
+          # Read lean-toolchain file and checkout appropriate branch
+          TOOLCHAIN=$(cat ../lean-toolchain)
+          if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v ]]; then
+            VERSION=${TOOLCHAIN#leanprover/lean4:}
+            git checkout "$VERSION"
+          else
+            git checkout master
+          fi
+          # Build lean4checker using the same toolchain
+          cp ../lean-toolchain .
+          lake build
+
   final:
     name: Post-CI jobJOB_NAME
     if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'

.github/workflows/PR_summary.yml

@@ -95,6 +95,9 @@ jobs:
         currentHash="$(git rev-parse HEAD)"
         hashURL="https://github.com/${{ github.repository }}/pull/${{ github.event.pull_request.number }}/commits/${currentHash}"
 
-        message="$(printf '%s [%s](%s)%s\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${high_percentages}" "${importCount}" "${declDiff}")"
+        ## Technical debt changes
+        techDebtVar="$(./scripts/technical-debt-metrics.sh pr_summary)"
+
+        message="$(printf '%s [%s](%s)%s\n\n%s\n\n---\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${high_percentages}" "${importCount}" "${declDiff}" "${techDebtVar}")"
 
         ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}"

.github/workflows/bors.yml

@@ -143,8 +143,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get #Mathlib.Init
-          #lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          lake exe cache get Mathlib.Init
+          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
@@ -250,10 +250,20 @@ jobs:
           python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
           lake exe check-yaml
 
-      - name: verify `lake exe graph` works
-        run: |
-          lake exe graph
-          rm import_graph.dot
+      - name: generate our import graph
+        run: lake exe graph
+
+      - name: upload the import graph
+        uses: actions/upload-artifact@v4
+        with:
+          name: import-graph
+          path: import_graph.dot
+          ## the default is 90, but we build often, so unless there's a reason
+          ## to care about old copies in the future, just say 7 days for now
+          retention-days: 7
+
+      - name: clean up the import graph file
+        run: rm import_graph.dot
 
       - name: build everything
         # make sure everything is available for test/import_all.lean
@@ -304,6 +314,23 @@ jobs:
           scripts/lean-pr-testing-comments.sh lean
           scripts/lean-pr-testing-comments.sh batteries
 
+      - name: build lean4checker, but don't run it
+        if: ${{ (always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure') && contains(github.event.pull_request.changed_files, 'lean-toolchain') }}
+        run: |
+          git clone https://github.com/leanprover/lean4checker
+          cd lean4checker
+          # Read lean-toolchain file and checkout appropriate branch
+          TOOLCHAIN=$(cat ../lean-toolchain)
+          if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v ]]; then
+            VERSION=${TOOLCHAIN#leanprover/lean4:}
+            git checkout "$VERSION"
+          else
+            git checkout master
+          fi
+          # Build lean4checker using the same toolchain
+          cp ../lean-toolchain .
+          lake build
+
   final:
     name: Post-CI job
     if: github.repository == 'leanprover-community/mathlib4'

.github/workflows/build.yml

@@ -150,8 +150,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get #Mathlib.Init
-          #lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          lake exe cache get Mathlib.Init
+          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
@@ -257,10 +257,20 @@ jobs:
           python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
           lake exe check-yaml
 
-      - name: verify `lake exe graph` works
-        run: |
-          lake exe graph
-          rm import_graph.dot
+      - name: generate our import graph
+        run: lake exe graph
+
+      - name: upload the import graph
+        uses: actions/upload-artifact@v4
+        with:
+          name: import-graph
+          path: import_graph.dot
+          ## the default is 90, but we build often, so unless there's a reason
+          ## to care about old copies in the future, just say 7 days for now
+          retention-days: 7
+
+      - name: clean up the import graph file
+        run: rm import_graph.dot
 
       - name: build everything
         # make sure everything is available for test/import_all.lean
@@ -311,6 +321,23 @@ jobs:
           scripts/lean-pr-testing-comments.sh lean
           scripts/lean-pr-testing-comments.sh batteries
 
+      - name: build lean4checker, but don't run it
+        if: ${{ (always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure') && contains(github.event.pull_request.changed_files, 'lean-toolchain') }}
+        run: |
+          git clone https://github.com/leanprover/lean4checker
+          cd lean4checker
+          # Read lean-toolchain file and checkout appropriate branch
+          TOOLCHAIN=$(cat ../lean-toolchain)
+          if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v ]]; then
+            VERSION=${TOOLCHAIN#leanprover/lean4:}
+            git checkout "$VERSION"
+          else
+            git checkout master
+          fi
+          # Build lean4checker using the same toolchain
+          cp ../lean-toolchain .
+          lake build
+
   final:
     name: Post-CI job
     if: github.repository == 'leanprover-community/mathlib4'

.github/workflows/build_fork.yml

@@ -147,8 +147,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get #Mathlib.Init
-          #lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          lake exe cache get Mathlib.Init
+          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
@@ -254,10 +254,20 @@ jobs:
           python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
           lake exe check-yaml
 
-      - name: verify `lake exe graph` works
-        run: |
-          lake exe graph
-          rm import_graph.dot
+      - name: generate our import graph
+        run: lake exe graph
+
+      - name: upload the import graph
+        uses: actions/upload-artifact@v4
+        with:
+          name: import-graph
+          path: import_graph.dot
+          ## the default is 90, but we build often, so unless there's a reason
+          ## to care about old copies in the future, just say 7 days for now
+          retention-days: 7
+
+      - name: clean up the import graph file
+        run: rm import_graph.dot
 
       - name: build everything
         # make sure everything is available for test/import_all.lean
@@ -308,6 +318,23 @@ jobs:
           scripts/lean-pr-testing-comments.sh lean
           scripts/lean-pr-testing-comments.sh batteries
 
+      - name: build lean4checker, but don't run it
+        if: ${{ (always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure') && contains(github.event.pull_request.changed_files, 'lean-toolchain') }}
+        run: |
+          git clone https://github.com/leanprover/lean4checker
+          cd lean4checker
+          # Read lean-toolchain file and checkout appropriate branch
+          TOOLCHAIN=$(cat ../lean-toolchain)
+          if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v ]]; then
+            VERSION=${TOOLCHAIN#leanprover/lean4:}
+            git checkout "$VERSION"
+          else
+            git checkout master
+          fi
+          # Build lean4checker using the same toolchain
+          cp ../lean-toolchain .
+          lake build
+
   final:
     name: Post-CI job (fork)
     if: github.repository != 'leanprover-community/mathlib4'

.github/workflows/discover-lean-pr-testing.yml

@@ -12,10 +12,10 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-    - name: Checkout mathlib repository
+    - name: Checkout mathlib4 repository
       uses: actions/checkout@v4
       with:
-        repository: leanprover-community/mathlib
+        repository: leanprover-community/mathlib4
         ref: nightly-testing
         fetch-depth: 0  # Fetch all branches