Merge remote-tracking branch 'origin/master' into sperner-again

.docker/debian/lean/Dockerfile

@@ -26,7 +26,10 @@ RUN python3 -m pip install --user mathlibtools
 # now install `pyinstaller`, and run it on the installed copy of `leanproject`
 RUN python3 -m pip install --user pyinstaller
 WORKDIR /home/lean/.local/bin
-RUN pyinstaller --onefile --noconfirm leanproject
+# We need the `--hidden-import` flag here due to PyInstaller not knowing the dependencies
+# of PyNaCl (https://github.com/pyinstaller/pyinstaller/issues/3525), which is itself a transitive
+# dependency of mathlibtools via PyGithub.
+RUN pyinstaller --onefile --noconfirm --hidden-import _cffi_backend leanproject
 # this has created `/home/lean/.local/bin/dist/leanproject`,
 # which we'll now copy to a fresh container
 

.github/CODEOWNERS

@@ -0,0 +1,19 @@
+# By default, the mathlib maintainers own everything in the repo.
+# Later matches will take precedence over this match.
+
+# Disabled until we have better coverage by other patterns. Reenable in the future.
+# *        @leanprover-community/mathlib-maintainers
+
+src/category_theory/    @leanprover-community/mathlib-CT
+
+src/measure_theory/     @leanprover-community/mathlib-meas
+
+src/algebraic_topology/ @leanprover-community/mathlib-CT # for now the category theory team can take care of this
+
+src/algebraic_geometry/ @leanprover-community/mathlib-AG
+
+src/combinatorics/      @leanprover-community/mathlib-CO
+
+src/probability/        @leanprover-community/mathlib-PR
+
+src/tactic/             @leanprover-community/mathlib-meta

.github/workflows/add_port_comment.yml

@@ -0,0 +1,51 @@
+name: Add mathlib4 porting comments
+
+on:
+  schedule:
+    - cron: "0 0 * * *"
+  workflow_dispatch:
+
+jobs:
+  build:
+    name: Update comments
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+
+      - name: install Python
+        uses: actions/setup-python@v4
+        with:
+          python-version: 3.8
+
+      - name: install latest mathlibtools
+        run: |
+          pip install git+https://github.com/leanprover-community/mathlib-tools
+
+      # multiline outputs are only supported in javascript
+      - name: update docstrings and generate message
+        uses: actions/github-script@v5
+        id: generate-message
+        with:
+          script: |
+            proc = await exec.getExecOutput("python", ["./scripts/add_port_comments.py"]);
+            console.log(proc.stdout);
+            core.setOutput("FILE_LIST", proc.stdout);
+
+      - name: Create Pull Request
+        uses: peter-evans/create-pull-request@v4
+        with:
+          base: master
+          commit-message: "chore(*): add mathlib4 synchronization comments"
+          title: "chore(*): add mathlib4 synchronization comments"
+          author: leanprover-community-bot <[email protected]>
+          body: |
+            Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
+            Relates to the following files:
+            ${{ steps.generate-message.outputs.FILE_LIST }}
+
+            ---
+            I am a bot; please check that I have not put a comment in a bad place before running `bors merge`!
+          labels: |
+            easy
+            awaiting-review
+            mathlib4-synchronization

.github/workflows/add_ported_warnings.yml

@@ -0,0 +1,54 @@
+name: Add mathlib4 porting warnings
+
+on:
+  pull_request:
+
+jobs:
+  build:
+    name: Check for modifications to ported files
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+
+      - name: install Python
+        uses: actions/setup-python@v4
+        with:
+          python-version: 3.8
+
+      - name: install latest mathlibtools
+        run: |
+          pip install git+https://github.com/leanprover-community/mathlib-tools
+
+      # TODO: is this really faster than just calling git from python?
+      - name: Get changed files
+        id: changed-files
+        uses: Ana06/[email protected]
+
+      - name: run the script
+        id: script
+        run: |
+          python scripts/detect_ported_files.py ${{ steps.changed-files.outputs.all }}
+
+      - id: PR
+        uses: 8BitJonny/[email protected]
+        # TODO: this may not work properly if the same commit is pushed to multiple branches:
+        # https://github.com/8BitJonny/gh-get-current-pr/issues/8
+        with:
+          github-token: ${{ secrets.GITHUB_TOKEN }}
+          sha: ${{ github.event.pull_request.head.sha }}
+          # Only return if PR is still open
+          filterOutClosed: true
+
+      - if: steps.script.outputs.modifies_ported == 'True'
+        id: add_label
+        name: add "modifies-synchronized-file"
+        # we use curl rather than octokit/request-action so that the job won't fail
+        # (and send an annoying email) if the labels don't exist
+        run: |
+          curl -L \
+            -X POST \
+            -H "Accept: application/vnd.github+json" \
+            -H "Authorization: Bearer ${{ secrets.GITHUB_TOKEN }}"\
+            -H "X-GitHub-Api-Version: 2022-11-28" \
+            https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.PR.outputs.number }}/labels \
+            -d '{"labels":["modifies-synchronized-file"]}'

.github/workflows/bors.yml

@@ -22,7 +22,7 @@ jobs:
     runs-on: ubuntu-latest
     # timeout-minutes: 3
     steps:
-      - uses: styfle/cancel-workflow-action@0.9.0
+      - uses: styfle/cancel-workflow-action@0.11.0
         with:
           all_but_latest: true
           access_token: ${{ github.token }}
@@ -32,18 +32,28 @@ jobs:
     name: Lint style
     runs-on: bors
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
+
+      - name: Install bibtool
+        if: ${{ 'bors' == 'ubuntu-latest' }}
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y bibtool
 
       - name: install Python
         if: ${{ 'bors' == 'ubuntu-latest' }}
-        uses: actions/setup-python@v2
+        uses: actions/setup-python@v4
         with:
           python-version: 3.8
 
-      - name: lint
+      - name: lint style
         run: |
           ./scripts/lint-style.sh
 
+      - name: lint references.bib
+        run: |
+          ./scripts/lint-bib.sh
+
   build:
     if: github.repository == 'leanprover-community/mathlib'
     name: Build mathlib
@@ -54,7 +64,7 @@ jobs:
     outputs:
       artifact_name: ${{ steps.setup_precompiled.outputs.artifact_name }}
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
         with:
           fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}
 
@@ -68,7 +78,7 @@ jobs:
 
       - name: install Python
         if: ${{ ! 1 }}
-        uses: actions/setup-python@v1
+        uses: actions/setup-python@v4
         with:
           python-version: 3.8
 
@@ -78,10 +88,11 @@ jobs:
       - name: leanpkg build
         id: build
         run: |
+          set -o pipefail
           leanpkg configure
-          echo "::set-output name=started::true"
-          lean --json -T100000 --make src | python3 scripts/detect_errors.py
+          echo "started=true" >> $GITHUB_OUTPUT
           lean --json -T100000 --make src | python3 scripts/detect_errors.py
+          lean --json -T400000 --make src | python3 scripts/detect_errors.py
 
       - name: push release to azure
         if: always() && github.repository == 'leanprover-community/mathlib' && steps.build.outputs.started == 'true'
@@ -100,7 +111,7 @@ jobs:
           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"
+          echo "artifact_name=precompiled-mathlib-$short_lean_version-$git_hash" >> $GITHUB_OUTPUT
 
       - name: upload precompiled mathlib zip file
         if: always() && steps.build.outputs.started == 'true'
@@ -132,7 +143,7 @@ jobs:
         run: rm -rf ./* ./.??*
 
       - name: retrieve build
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v3
         with:
           name: ${{ needs.build.outputs.artifact_name }}
 
@@ -169,7 +180,7 @@ jobs:
         run: rm -rf ./* ./.??*
 
       - name: retrieve build
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v3
         with:
           name: ${{ needs.build.outputs.artifact_name }}
 
@@ -185,19 +196,32 @@ jobs:
 
       - name: install Python
         if: ${{ ! 1 }}
-        uses: actions/setup-python@v1
+        uses: actions/setup-python@v4
         with:
           python-version: 3.8
 
       - name: install Python dependencies
         if: ${{ ! 1 }}
-        run: python3 -m pip install --upgrade pip pyyaml
+        run: python3 -m pip install --upgrade pip pyyaml requests mathlibtools
 
       - name: tests
         run: |
           set -o pipefail
           lean --json -T100000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py
 
+      - name: check archive and counterexample directories have unique identifiers
+        run: |
+          pip install mathlibtools
+          (cd archive && python -m mathlibtools.leanproject mk-all && mv all.lean archive_all.lean)
+          (cd counterexamples && python -m mathlibtools.leanproject mk-all && mv all.lean counterexamples_all.lean)
+          python -m mathlibtools.leanproject mk-all
+          echo "import all" >> all_all.lean
+          echo "import counterexamples_all" >> all_all.lean
+          echo "import archive_all" >> all_all.lean
+          echo "path ./archive" >> leanpkg.path
+          echo "path ./counterexamples" >> leanpkg.path
+          lean --json -T100000 --make all_all.lean | python3 scripts/detect_errors.py
+
       - uses: actions/setup-java@v2
         if: ${{ ! 1 }}
         with:
@@ -233,10 +257,10 @@ jobs:
     needs: [style_lint, build, lint, tests]
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
 
       - id: PR
-        uses: 8BitJonny/gh-get-current-pr@1.2.0
+        uses: 8BitJonny/gh-get-current-pr@2.2.0
         # TODO: this may not work properly if the same commit is pushed to multiple branches:
         # https://github.com/8BitJonny/gh-get-current-pr/issues/8
         with: