Merge branch 'leanprover-community:master' into main

Author: CoolRmal

.github/actionlint.yml

@@ -2,3 +2,4 @@ self-hosted-runner:
   labels:
     - bors
     - pr
+    - doc-gen

.github/build.in.yml

@@ -186,6 +186,33 @@ jobs:
           cd pr-branch
           lake env
 
+      - name: validate lake-manifest.json inputRevs
+        # Only enforce this on the main mathlib4 repository, not on nightly-testing
+        if: github.repository == 'leanprover-community/mathlib4'
+        shell: bash
+        run: |
+          cd pr-branch
+
+          # Check that all inputRevs in lake-manifest.json match the required pattern
+          echo "Validating lake-manifest.json inputRevs..."
+
+          # Extract all inputRevs from the manifest
+          invalid_revs=$(jq -r '.packages[].inputRev // empty' lake-manifest.json | \
+            grep -v -E '^(main|master|v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?)$' || true)
+
+          if [ -n "$invalid_revs" ]; then
+            echo "❌ Error: Found invalid inputRevs in lake-manifest.json:"
+            echo "$invalid_revs"
+            echo ""
+            echo "All inputRevs must be one of:"
+            echo "  - 'main'"
+            echo "  - 'master'"
+            echo "  - 'vX.Y.Z' (semantic version, e.g., v1.2.3 or v1.2.3-pre)"
+            exit 1
+          else
+            echo "✅ All inputRevs in lake-manifest.json are valid"
+          fi
+
       - name: get cache (1/3 - setup and initial fetch)
         id: get_cache_part1_setup
         shell: bash # only runs `cache get` from `master-branch`, so doesn't need to be inside landrun
@@ -598,6 +625,12 @@ jobs:
         run: |
           lake build Batteries Qq Aesop ProofWidgets Plausible
 
+      - name: build AesopTest (nightly-testing only)
+        # Only run on the mathlib4-nightly-testing repository
+        if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
+        run: |
+          lake build AesopTest
+
       # We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
       # Instead we run it in a cron job on master: see `lean4checker.yml`.
       # Output is posted to the zulip topic
@@ -654,9 +687,7 @@ jobs:
     needs: [style_lint, build, post_steps]
     runs-on: ubuntu-latest
     steps:
-      # This action is used to determine the PR metadata in the event of a push.
-      - if: github.event_name != 'pull_request_target'
-        id: PR_from_push
+      - id: PR_from_push
         uses: 8BitJonny/gh-get-current-pr@4056877062a1f3b624d5d4c2bedefa9cf51435c9 # 4.0.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
@@ -665,6 +696,7 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
+      # TODO: delete this step and rename `PR_from_push` to `PR` if the above step seems to work properly
       # Combine the output from the previous action with the metadata supplied by GitHub itself.
       # Note that if we fall back to github.event.pull_request data, the list of labels is generated when this workflow is triggered
       # and not updated afterwards!

.github/workflows/bors.yml

@@ -196,6 +196,33 @@ jobs:
           cd pr-branch
           lake env
 
+      - name: validate lake-manifest.json inputRevs
+        # Only enforce this on the main mathlib4 repository, not on nightly-testing
+        if: github.repository == 'leanprover-community/mathlib4'
+        shell: bash
+        run: |
+          cd pr-branch
+
+          # Check that all inputRevs in lake-manifest.json match the required pattern
+          echo "Validating lake-manifest.json inputRevs..."
+
+          # Extract all inputRevs from the manifest
+          invalid_revs=$(jq -r '.packages[].inputRev // empty' lake-manifest.json | \
+            grep -v -E '^(main|master|v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?)$' || true)
+
+          if [ -n "$invalid_revs" ]; then
+            echo "❌ Error: Found invalid inputRevs in lake-manifest.json:"
+            echo "$invalid_revs"
+            echo ""
+            echo "All inputRevs must be one of:"
+            echo "  - 'main'"
+            echo "  - 'master'"
+            echo "  - 'vX.Y.Z' (semantic version, e.g., v1.2.3 or v1.2.3-pre)"
+            exit 1
+          else
+            echo "✅ All inputRevs in lake-manifest.json are valid"
+          fi
+
       - name: get cache (1/3 - setup and initial fetch)
         id: get_cache_part1_setup
         shell: bash # only runs `cache get` from `master-branch`, so doesn't need to be inside landrun
@@ -608,6 +635,12 @@ jobs:
         run: |
           lake build Batteries Qq Aesop ProofWidgets Plausible
 
+      - name: build AesopTest (nightly-testing only)
+        # Only run on the mathlib4-nightly-testing repository
+        if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
+        run: |
+          lake build AesopTest
+
       # We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
       # Instead we run it in a cron job on master: see `lean4checker.yml`.
       # Output is posted to the zulip topic
@@ -664,9 +697,7 @@ jobs:
     needs: [style_lint, build, post_steps]
     runs-on: ubuntu-latest
     steps:
-      # This action is used to determine the PR metadata in the event of a push.
-      - if: github.event_name != 'pull_request_target'
-        id: PR_from_push
+      - id: PR_from_push
         uses: 8BitJonny/gh-get-current-pr@4056877062a1f3b624d5d4c2bedefa9cf51435c9 # 4.0.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
@@ -675,6 +706,7 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
+      # TODO: delete this step and rename `PR_from_push` to `PR` if the above step seems to work properly
       # Combine the output from the previous action with the metadata supplied by GitHub itself.
       # Note that if we fall back to github.event.pull_request data, the list of labels is generated when this workflow is triggered
       # and not updated afterwards!

.github/workflows/build.yml

@@ -203,6 +203,33 @@ jobs:
           cd pr-branch
           lake env
 
+      - name: validate lake-manifest.json inputRevs
+        # Only enforce this on the main mathlib4 repository, not on nightly-testing
+        if: github.repository == 'leanprover-community/mathlib4'
+        shell: bash
+        run: |
+          cd pr-branch
+
+          # Check that all inputRevs in lake-manifest.json match the required pattern
+          echo "Validating lake-manifest.json inputRevs..."
+
+          # Extract all inputRevs from the manifest
+          invalid_revs=$(jq -r '.packages[].inputRev // empty' lake-manifest.json | \
+            grep -v -E '^(main|master|v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?)$' || true)
+
+          if [ -n "$invalid_revs" ]; then
+            echo "❌ Error: Found invalid inputRevs in lake-manifest.json:"
+            echo "$invalid_revs"
+            echo ""
+            echo "All inputRevs must be one of:"
+            echo "  - 'main'"
+            echo "  - 'master'"
+            echo "  - 'vX.Y.Z' (semantic version, e.g., v1.2.3 or v1.2.3-pre)"
+            exit 1
+          else
+            echo "✅ All inputRevs in lake-manifest.json are valid"
+          fi
+
       - name: get cache (1/3 - setup and initial fetch)
         id: get_cache_part1_setup
         shell: bash # only runs `cache get` from `master-branch`, so doesn't need to be inside landrun
@@ -615,6 +642,12 @@ jobs:
         run: |
           lake build Batteries Qq Aesop ProofWidgets Plausible
 
+      - name: build AesopTest (nightly-testing only)
+        # Only run on the mathlib4-nightly-testing repository
+        if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
+        run: |
+          lake build AesopTest
+
       # We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
       # Instead we run it in a cron job on master: see `lean4checker.yml`.
       # Output is posted to the zulip topic
@@ -671,9 +704,7 @@ jobs:
     needs: [style_lint, build, post_steps]
     runs-on: ubuntu-latest
     steps:
-      # This action is used to determine the PR metadata in the event of a push.
-      - if: github.event_name != 'pull_request_target'
-        id: PR_from_push
+      - id: PR_from_push
         uses: 8BitJonny/gh-get-current-pr@4056877062a1f3b624d5d4c2bedefa9cf51435c9 # 4.0.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
@@ -682,6 +713,7 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
+      # TODO: delete this step and rename `PR_from_push` to `PR` if the above step seems to work properly
       # Combine the output from the previous action with the metadata supplied by GitHub itself.
       # Note that if we fall back to github.event.pull_request data, the list of labels is generated when this workflow is triggered
       # and not updated afterwards!

.github/workflows/build_fork.yml

@@ -200,6 +200,33 @@ jobs:
           cd pr-branch
           lake env
 
+      - name: validate lake-manifest.json inputRevs
+        # Only enforce this on the main mathlib4 repository, not on nightly-testing
+        if: github.repository == 'leanprover-community/mathlib4'
+        shell: bash
+        run: |
+          cd pr-branch
+
+          # Check that all inputRevs in lake-manifest.json match the required pattern
+          echo "Validating lake-manifest.json inputRevs..."
+
+          # Extract all inputRevs from the manifest
+          invalid_revs=$(jq -r '.packages[].inputRev // empty' lake-manifest.json | \
+            grep -v -E '^(main|master|v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?)$' || true)
+
+          if [ -n "$invalid_revs" ]; then
+            echo "❌ Error: Found invalid inputRevs in lake-manifest.json:"
+            echo "$invalid_revs"
+            echo ""
+            echo "All inputRevs must be one of:"
+            echo "  - 'main'"
+            echo "  - 'master'"
+            echo "  - 'vX.Y.Z' (semantic version, e.g., v1.2.3 or v1.2.3-pre)"
+            exit 1
+          else
+            echo "✅ All inputRevs in lake-manifest.json are valid"
+          fi
+
       - name: get cache (1/3 - setup and initial fetch)
         id: get_cache_part1_setup
         shell: bash # only runs `cache get` from `master-branch`, so doesn't need to be inside landrun
@@ -612,6 +639,12 @@ jobs:
         run: |
           lake build Batteries Qq Aesop ProofWidgets Plausible
 
+      - name: build AesopTest (nightly-testing only)
+        # Only run on the mathlib4-nightly-testing repository
+        if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
+        run: |
+          lake build AesopTest
+
       # We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
       # Instead we run it in a cron job on master: see `lean4checker.yml`.
       # Output is posted to the zulip topic
@@ -668,9 +701,7 @@ jobs:
     needs: [style_lint, build, post_steps]
     runs-on: ubuntu-latest
     steps:
-      # This action is used to determine the PR metadata in the event of a push.
-      - if: github.event_name != 'pull_request_target'
-        id: PR_from_push
+      - id: PR_from_push
         uses: 8BitJonny/gh-get-current-pr@4056877062a1f3b624d5d4c2bedefa9cf51435c9 # 4.0.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
@@ -679,6 +710,7 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
+      # TODO: delete this step and rename `PR_from_push` to `PR` if the above step seems to work properly
       # Combine the output from the previous action with the metadata supplied by GitHub itself.
       # Note that if we fall back to github.event.pull_request data, the list of labels is generated when this workflow is triggered
       # and not updated afterwards!

.github/workflows/nightly-docgen.yml

@@ -0,0 +1,126 @@
+name: Docgen test on nightly-testing
+
+on:
+  schedule:
+    - cron: '37 1 * * *'  # Run at 01:37 UTC every day (generated by fair dice roll)
+  workflow_dispatch:
+
+jobs:
+  build:
+    name: build mathlib4-nightly-testing docs
+    runs-on: doc-gen
+    if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
+    steps:
+      - name: clean up
+        run: |
+          rm -rf docbuild
+          rm -rf "$HOME/.elan"
+          rm -rf "$HOME/.cache/mathlib"
+
+      - name: Checkout mathlib
+        uses: actions/checkout@v4
+        with:
+          repository: leanprover-community/mathlib4-nightly-testing
+          ref: nightly-testing-green
+
+      - name: Add upstream
+        run: |
+          # Add the nightly-testing remote if it does not exist already, otherwise `lake exe cache` gets confused.
+          (git remote | grep -q '^nightly-testing$') || git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git
+
+      - name: Build and lint the project.
+        id: build-lean
+        uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # v1.2.0
+        with:
+          use-mathlib-cache: true
+
+      # This is not quite the same as `docgen-action` does, since we do not actually want to upload the result.
+      - name: create dummy docs project
+        run: |
+          # Build HTML documentation for the project
+          # The output will be located in docbuild/docs
+
+          # Create a temporary docbuild folder
+          mkdir -p docbuild
+
+          # Template lakefile.toml
+          cat << EOF > docbuild/lakefile.toml
+          name = "docbuild"
+          reservoir = false
+          version = "0.1.0"
+          packagesDir = "../.lake/packages"
+
+          [[require]]
+          name = "mathlib"
+          path = "../"
+
+          [[require]]
+          scope = "leanprover"
+          name = "doc-gen4"
+          rev = "main"
+          EOF
+
+          # Initialise docbuild as a Lean project
+          cd docbuild
+
+          # No need to reinstall packages if we can just copy them from Mathlib.
+          mkdir -p .lake/packages
+          cp -r ../.lake/packages/* .lake/packages
+          cp ../lean-toolchain . # Use Mathlib's (nightly) toolchain.
+
+          # Disable an error message due to a non-blocking bug. See Zulip
+          MATHLIB_NO_CACHE_ON_UPDATE=1 lake update "$NAME"
+
+          # Copy references.bib over while doc-gen lacks support for subproject references.bib
+          mkdir docs/
+          cp ../docs/references.bib docs/references.bib
+
+      - name: build doc-gen4
+        working-directory: docbuild
+        run: |
+          env DISABLE_EQUATIONS=1 lake build doc-gen4
+
+      - name: build import graph
+        working-directory: .
+        run: |
+          lake exe graph mathlib.html
+
+      - name: generate docs
+        working-directory: docbuild
+        run: |
+          lake build Batteries:docs Qq:docs Aesop:docs ProofWidgets:docs Mathlib:docs Archive:docs Counterexamples:docs docs:docs
+          lake build Mathlib:docsHeader
+
+      - name: clean up
+        if: always()
+        run: |
+          rm -rf docbuild
+          rm -rf "$HOME/.elan"
+          rm -rf "$HOME/.cache/mathlib"
+
+      - name: Send success message on Zulip
+        uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
+        if: success()
+        with:
+          api-key: ${{ secrets.ZULIP_API_KEY }}
+          email: 'github-mathlib4-bot@leanprover.zulipchat.com'
+          organization-url: 'https://leanprover.zulipchat.com'
+          to: 'nightly-testing'
+          type: 'stream'
+          topic: 'Docgen status updates'
+          content: |
+            ✅ The docgen run for Mathlib's [nightly-testing branch](https://github.com/leanprover-community/mathlib4-nightly-testing/tree/nightly-testing) has [succeeded](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) ([${{ github.sha }}](https://github.com/${{ github.repository }}/commit/${{ github.sha }})).
+
+      - name: Send failure message on Zulip
+        uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
+        if: failure()
+        with:
+          api-key: ${{ secrets.ZULIP_API_KEY }}
+          email: 'github-mathlib4-bot@leanprover.zulipchat.com'
+          organization-url: 'https://leanprover.zulipchat.com'
+          to: 'nightly-testing'
+          type: 'stream'
+          topic: 'Docgen status updates'
+          content: |
+            ❌ The docgen run for Mathlib's [nightly-testing branch](https://github.com/leanprover-community/mathlib4-nightly-testing/tree/nightly-testing) has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) ([${{ github.sha }}](https://github.com/${{ github.repository }}/commit/${{ github.sha }})).
+            This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.