Merge master into YK-card-fiber-eq (using imerge)

.github/workflows/add_port_comment.yml

@@ -13,7 +13,7 @@ jobs:
       - uses: actions/checkout@v3
 
       - name: install Python
-        uses: actions/setup-python@v3
+        uses: actions/setup-python@v4
         with:
           python-version: 3.8
 
@@ -29,7 +29,7 @@ jobs:
           script: |
             proc = await exec.getExecOutput("python", ["./scripts/add_port_comments.py"]);
             console.log(proc.stdout);
-            core.setOutput("PR_LIST", proc.stdout); 
+            core.setOutput("FILE_LIST", proc.stdout);
 
       - name: Create Pull Request
         uses: peter-evans/create-pull-request@v4
@@ -40,12 +40,11 @@ jobs:
           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 PRs:
-            ${{ steps.generate-message.outputs.PR_LIST }}
+            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`!
-            If the PRs above don't match the file they are listed after, that means the port status page is wrong.
           labels: |
             easy
             awaiting-review

.github/workflows/add_ported_warnings.yml

@@ -11,7 +11,7 @@ jobs:
       - uses: actions/checkout@v3
 
       - name: install Python
-        uses: actions/setup-python@v3
+        uses: actions/setup-python@v4
         with:
           python-version: 3.8
 
@@ -22,8 +22,33 @@ jobs:
       # TODO: is this really faster than just calling git from python?
       - name: Get changed files
         id: changed-files
-        uses: tj-actions/changed-files@v34
+        uses: Ana06/get-changed-files@v2.2.0
 
       - name: run the script
+        id: script
         run: |
-          python scripts/detect_ported_files.py ${{ steps.changed-files.outputs.all_changed_files }}
+          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
 
@@ -80,7 +90,7 @@ jobs:
         run: |
           set -o pipefail
           leanpkg configure
-          echo "::set-output name=started::true"
+          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
 
@@ -101,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'
@@ -133,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 }}
 
@@ -170,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 }}
 
@@ -186,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 requests
+        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:
@@ -234,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:

.github/workflows/build.yml

@@ -30,7 +30,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 }}
@@ -40,18 +40,28 @@ jobs:
     name: Lint style
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
+
+      - name: Install bibtool
+        if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y bibtool
 
       - name: install Python
         if: ${{ 'ubuntu-latest' == '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
@@ -62,7 +72,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 }}
 
@@ -76,7 +86,7 @@ jobs:
 
       - name: install Python
         if: ${{ ! 1 }}
-        uses: actions/setup-python@v1
+        uses: actions/setup-python@v4
         with:
           python-version: 3.8
 
@@ -88,7 +98,7 @@ jobs:
         run: |
           set -o pipefail
           leanpkg configure
-          echo "::set-output name=started::true"
+          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
 
@@ -109,7 +119,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'
@@ -141,7 +151,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 }}
 
@@ -178,7 +188,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 }}
 
@@ -194,19 +204,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 requests
+        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:
@@ -242,10 +265,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: