Trigger CI for leanprover/lean4#6123

.github/build.in.yml

@@ -4,6 +4,14 @@
 ### NB: and regenerate those files by manually running
 ### NB: .github/workflows/mk_build_yml.sh
 
+env:
+  # Disable Lake's automatic fetching of cloud builds.
+  # Lake's cache is currently incompatible with Mathlib's `lake exe cache`.
+  # This is because Mathlib's Cache assumes all build aritfacts present in the build directory
+  # are valid by-products of the Mathlib build. Build artifacts fetched from Lake's cache do
+  # not necessarily satisfy this property.
+  LAKE_NO_CACHE: true
+
 jobs:
   # Cancels previous runs of jobs in this file
   cancel:
@@ -121,6 +129,7 @@ jobs:
 
       - name: prune ProofWidgets .lake
         run: |
+          lake build proofwidgets:release
           # The ProofWidgets release contains not just the `.js` (which we need in order to build)
           # but also `.oleans`, which may have been built with the wrong toolchain.
           # This removes them.

.github/workflows/PR_summary.yml

@@ -5,6 +5,7 @@ on:
 
 jobs:
   build:
+    name: "post-or-update-summary-comment"
     runs-on: ubuntu-latest
 
     steps:

.github/workflows/bench_summary_comment.yml

@@ -27,7 +27,7 @@ jobs:
         run: |
           {
             cat scripts/bench_summary.lean
-            printf $'run_cmd BenchAction.addBenchSummaryComment %s "leanprover-community/mathlib4"' "${PR}"
+            printf $'run_cmd BenchAction.addBenchSummaryComment %s "leanprover-community/mathlib4" %s' "${PR}" "${{ github.run_id }}"
           } |
             lake env lean --stdin
         env:

.github/workflows/bors.yml

@@ -14,6 +14,14 @@ on:
 
 name: continuous integration (staging)
 
+env:
+  # Disable Lake's automatic fetching of cloud builds.
+  # Lake's cache is currently incompatible with Mathlib's `lake exe cache`.
+  # This is because Mathlib's Cache assumes all build aritfacts present in the build directory
+  # are valid by-products of the Mathlib build. Build artifacts fetched from Lake's cache do
+  # not necessarily satisfy this property.
+  LAKE_NO_CACHE: true
+
 jobs:
   # Cancels previous runs of jobs in this file
   cancel:
@@ -131,6 +139,7 @@ jobs:
 
       - name: prune ProofWidgets .lake
         run: |
+          lake build proofwidgets:release
           # The ProofWidgets release contains not just the `.js` (which we need in order to build)
           # but also `.oleans`, which may have been built with the wrong toolchain.
           # This removes them.

.github/workflows/build.yml

@@ -21,6 +21,14 @@ on:
 
 name: continuous integration
 
+env:
+  # Disable Lake's automatic fetching of cloud builds.
+  # Lake's cache is currently incompatible with Mathlib's `lake exe cache`.
+  # This is because Mathlib's Cache assumes all build aritfacts present in the build directory
+  # are valid by-products of the Mathlib build. Build artifacts fetched from Lake's cache do
+  # not necessarily satisfy this property.
+  LAKE_NO_CACHE: true
+
 jobs:
   # Cancels previous runs of jobs in this file
   cancel:
@@ -138,6 +146,7 @@ jobs:
 
       - name: prune ProofWidgets .lake
         run: |
+          lake build proofwidgets:release
           # The ProofWidgets release contains not just the `.js` (which we need in order to build)
           # but also `.oleans`, which may have been built with the wrong toolchain.
           # This removes them.

.github/workflows/build_fork.yml

@@ -18,6 +18,14 @@ on:
 
 name: continuous integration (mathlib forks)
 
+env:
+  # Disable Lake's automatic fetching of cloud builds.
+  # Lake's cache is currently incompatible with Mathlib's `lake exe cache`.
+  # This is because Mathlib's Cache assumes all build aritfacts present in the build directory
+  # are valid by-products of the Mathlib build. Build artifacts fetched from Lake's cache do
+  # not necessarily satisfy this property.
+  LAKE_NO_CACHE: true
+
 jobs:
   # Cancels previous runs of jobs in this file
   cancel:
@@ -135,6 +143,7 @@ jobs:
 
       - name: prune ProofWidgets .lake
         run: |
+          lake build proofwidgets:release
           # The ProofWidgets release contains not just the `.js` (which we need in order to build)
           # but also `.oleans`, which may have been built with the wrong toolchain.
           # This removes them.

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

@@ -38,8 +38,10 @@ jobs:
         # The "./" in front of the path is important for `git show`
         OLD=$(git show "$PREV_COMMIT":./lean-toolchain | cut -f2 -d:)
 
-        echo "new=$NEW" >> "$GITHUB_OUTPUT"
+        echo "old=$OLD"
+        echo "new=$NEW"
         echo "old=$OLD" >> "$GITHUB_OUTPUT"
+        echo "new=$NEW" >> "$GITHUB_OUTPUT"
 
     - name: Clone lean4 repository and get PRs
       id: get-prs
@@ -65,19 +67,27 @@ jobs:
         # This will only fetch commits newer than previously fetched commits (ie $OLD)
         git fetch origin tag "$NEW" --no-tags
 
-        PRS=$(git log --oneline "$OLD..$NEW" | sed 's/.*(#\([0-9]\+\))$/\1/')
+        # Find all commits to lean4 between the $OLD and $NEW toolchains
+        # and extract the github PR numbers
+        # (drop anything that doesn't look like a PR number from the final result)
+        PRS=$(git log --oneline "$OLD..$NEW" | sed 's/.*(#\([0-9]\+\))$/\1/' | grep -E '^[0-9]+$')
         
         # Output the PRs
         echo "$PRS"
-        echo "prs=$PRS" >> "$GITHUB_OUTPUT"
+        printf "prs<<EOF\n%s\nEOF" "$PRS" >> "$GITHUB_OUTPUT"
 
     - name: Use merged PRs information
       id: find-branches
       run: |
         # Use the PRs from the previous step
         PRS="${{ steps.get-prs.outputs.prs }}"
+        echo "=== PRS ========================="
+        echo "$PRS"
         echo "$PRS" | tr ' ' '\n' > prs.txt
+        echo "=== prs.txt ====================="
+        cat prs.txt
         MATCHING_BRANCHES=$(git branch -r | grep -f prs.txt)
+        echo "=== MATCHING_BRANCHES ==========="
         echo "$MATCHING_BRANCHES"
 
         # Initialize an empty variable to store branches with relevant diffs
@@ -90,26 +100,32 @@ jobs:
             
             # Check if the diff contains files other than the specified ones
             if echo "$DIFF_FILES" | grep -v -e 'lake-manifest.json' -e 'lakefile.lean' -e 'lean-toolchain'; then
-                # If it does, add the branch to RELEVANT_BRANCHES
-                RELEVANT_BRANCHES="$RELEVANT_BRANCHES $BRANCH"
+                # Extract the PR number and actual branch name
+                PR_NUMBER=$(echo "$BRANCH" | grep -oP '\d+$')
+                ACTUAL_BRANCH=${BRANCH#origin/}
+                GITHUB_DIFF="https://github.com/leanprover-community/mathlib4/compare/nightly-testing...$ACTUAL_BRANCH"
+                
+                # Append the branch details to RELEVANT_BRANCHES
+                RELEVANT_BRANCHES="$RELEVANT_BRANCHES"$'\n- '"$ACTUAL_BRANCH (lean4#$PR_NUMBER) ([diff with \`nightly-testing\`]($GITHUB_DIFF))"
             fi
         done
 
         # Output the relevant branches
+        echo "=== RELEVANT_BRANCHES ==========="
         echo "'$RELEVANT_BRANCHES'"
-        echo "branches=$RELEVANT_BRANCHES" >> "$GITHUB_OUTPUT"
+        printf "branches<<EOF\n%s\nEOF" "$RELEVANT_BRANCHES" >> "$GITHUB_OUTPUT"
 
     - name: Check if there are relevant branches
       id: check-branches
       run: |
         if [ -z "${{ steps.find-branches.outputs.branches }}" ]; then
-          echo "no_branches=true" >> "$GITHUB_ENV"
+          echo "branches_exist=false" >> "$GITHUB_ENV"
         else
-          echo "no_branches=false" >> "$GITHUB_ENV"
+          echo "branches_exist=true" >> "$GITHUB_ENV"
         fi
 
     - name: Send message on Zulip
-      if: env.no_branches == 'false'
+      if: env.branches_exist == 'true'
       uses: zulip/github-actions-zulip/send-message@v1
       with:
         api-key: ${{ secrets.ZULIP_API_KEY }}

.github/workflows/maintainer_bors.yml

@@ -84,4 +84,35 @@ jobs:
           curl --request DELETE \
             --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}${{ github.event.pull_request.number }}/labels/awaiting-author" \
             --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
-            # comment uses ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Set up Python
+        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
+          ( steps.user_permission.outputs.require-result == 'true' ||
+            steps.merge_or_delegate.outputs.bot == 'true' ) }}
+        uses: actions/setup-python@v5
+        with:
+          python-version: '3.x'
+
+      - name: Install dependencies
+        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
+          ( steps.user_permission.outputs.require-result == 'true' ||
+            steps.merge_or_delegate.outputs.bot == 'true' ) }}
+        run: |
+          python -m pip install --upgrade pip
+          pip install zulip
+
+      - uses: actions/checkout@v4
+        with:
+          sparse-checkout: |
+            scripts/zulip_emoji_merge_delegate.py
+
+      - name: Run Zulip Emoji Merge Delegate Script
+        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
+          ( steps.user_permission.outputs.require-result == 'true' ||
+            steps.merge_or_delegate.outputs.bot == 'true' ) }}
+        env:
+          ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
+          ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com
+          ZULIP_SITE: https://leanprover.zulipchat.com
+        run: |
+          python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "${{ steps.merge_or_delegate.outputs.mOrD }}" "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"

.github/workflows/sync_closed_tasks.yaml

@@ -12,6 +12,7 @@ on:
 
 jobs:
   build:
+    name: "Cross off linked issues"
     runs-on: ubuntu-latest
     steps:
       - name: Cross off any linked issue and PR references

.github/workflows/zulip_emoji_merge_delegate.yaml

@@ -1,19 +1,19 @@
 name: Zulip Emoji Merge Delegate
 
 on:
-  schedule:
-    - cron: '0 * * * *'  # Runs every hour
+  push:
+    branches:
+      - master
 
 jobs:
-  zulip-emoji-merge-delegate:
+  zulip-emoji-merged:
     runs-on: ubuntu-latest
 
     steps:
     - name: Checkout mathlib repository
       uses: actions/checkout@v4
       with:
-        sparse-checkout: |
-          scripts
+        fetch-depth: 0 # donwload the full repository
 
     - name: Set up Python
       uses: actions/setup-python@v5
@@ -30,6 +30,13 @@ jobs:
         ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
         ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com
         ZULIP_SITE: https://leanprover.zulipchat.com
-        GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
       run: |
-        python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "$GITHUB_TOKEN"
+          # scan the commits of the past 10 minutes, assuming that the timezone of the current machine
+          # is the same that performed the commit
+          git log --since="10 minutes ago" --pretty=oneline
+
+          printf $'Scanning commits:\n%s\n\nContinuing\n' "$(git log --since="10 minutes ago" --pretty=oneline)"
+          while read -r pr_number; do
+            printf $'Running the python script with pr "%s"\n' "${pr_number}"
+            python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "[Merged by Bors]" "${pr_number}"
+          done < <(git log --oneline -n 10 | awk -F# '{ gsub(/)$/, ""); print $NF}')

Archive/Hairer.lean

@@ -26,6 +26,7 @@ noncomputable section
 open Metric Set MeasureTheory
 open MvPolynomial hiding support
 open Function hiding eval
+open scoped ContDiff
 
 variable {ι : Type*} [Fintype ι]
 
@@ -110,7 +111,7 @@ lemma inj_L : Injective (L ι) :=
     apply subset_closure
 
 lemma hairer (N : ℕ) (ι : Type*) [Fintype ι] :
-    ∃ (ρ : EuclideanSpace ℝ ι → ℝ), tsupport ρ ⊆ closedBall 0 1 ∧ ContDiff ℝ ⊤ ρ ∧
+    ∃ (ρ : EuclideanSpace ℝ ι → ℝ), tsupport ρ ⊆ closedBall 0 1 ∧ ContDiff ℝ ∞ ρ ∧
     ∀ (p : MvPolynomial ι ℝ), p.totalDegree ≤ N →
     ∫ x : EuclideanSpace ℝ ι, eval x p • ρ x = eval 0 p := by
   have := (inj_L ι).comp (restrictTotalDegree ι ℝ N).injective_subtype

Archive/Imo/Imo2024Q5.lean

@@ -509,7 +509,7 @@ lemma Strategy.play_two (s : Strategy N) (m : MonsterData N) {k : ℕ} (hk : 2 <
   fin_cases i
   · rfl
   · have h : (1 : Fin 2) = Fin.last 1 := rfl
-    simp only [Fin.snoc_zero, Nat.reduceAdd, Fin.mk_one, Fin.isValue, Matrix.cons_val_one,
+    simp only [Fin.snoc_zero, Nat.reduceAdd, Fin.mk_one, Fin.isValue, id_eq, Matrix.cons_val_one,
       Matrix.head_cons]
     simp only [h, Fin.snoc_last]
     convert rfl

Cache/IO.lean

@@ -92,6 +92,7 @@ abbrev PackageDirs := Lean.RBMap String FilePath compare
 structure CacheM.Context where
   mathlibDepPath : FilePath
   packageDirs : PackageDirs
+  proofWidgetsBuildDir : FilePath
 
 abbrev CacheM := ReaderT CacheM.Context IO
 
@@ -141,7 +142,7 @@ private def CacheM.getContext : IO CacheM.Context := do
     ("ImportGraph", LAKEPACKAGESDIR / "importGraph"),
     ("LeanSearchClient", LAKEPACKAGESDIR / "LeanSearchClient"),
     ("Plausible", LAKEPACKAGESDIR / "plausible")
-  ]⟩
+  ], LAKEPACKAGESDIR / "proofwidgets" / ".lake" / "build"⟩
 
 def CacheM.run (f : CacheM α) : IO α := do ReaderT.run f (← getContext)
 

Cache/Requests.lean

@@ -159,11 +159,23 @@ into the `lean-toolchain` file at the root directory of your project"
     IO.Process.exit 1
   return ()
 
+/-- Fetches the ProofWidgets cloud release and prunes non-JS files. -/
+def getProofWidgets (buildDir : FilePath) : IO Unit := do
+  if (← buildDir.pathExists) then return
+  -- Unpack the ProofWidgets cloud release (for its `.js` files)
+  let exitCode ← (← IO.Process.spawn {cmd := "lake", args := #["-q", "build", "proofwidgets:release"]}).wait
+  if exitCode != 0 then
+    throw <| IO.userError s!"Failed to fetch ProofWidgets cloud release: lake failed with error code {exitCode}"
+  -- prune non-js ProofWidgets files (e.g., `olean`, `.c`)
+  IO.FS.removeDirAll (buildDir / "lib")
+  IO.FS.removeDirAll (buildDir / "ir")
+
 /-- Downloads missing files, and unpacks files. -/
 def getFiles (hashMap : IO.HashMap) (forceDownload forceUnpack parallel decompress : Bool) :
     IO.CacheM Unit := do
   let isMathlibRoot ← IO.isMathlibRoot
-  if !isMathlibRoot then checkForToolchainMismatch
+  unless isMathlibRoot do checkForToolchainMismatch
+  getProofWidgets (← read).proofWidgetsBuildDir
   downloadFiles hashMap forceDownload parallel
   if decompress then
     IO.unpackCache hashMap forceUnpack

Counterexamples/DirectSumIsInternal.lean

@@ -12,10 +12,10 @@ import Mathlib.Tactic.FinCases
 # Not all complementary decompositions of a module over a semiring make up a direct sum
 
 This shows that while `ℤ≤0` and `ℤ≥0` are complementary `ℕ`-submodules of `ℤ`, which in turn
-implies as a collection they are `CompleteLattice.Independent` and that they span all of `ℤ`, they
+implies as a collection they are `iSupIndep` and that they span all of `ℤ`, they
 do not form a decomposition into a direct sum.
 
-This file demonstrates why `DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top` must
+This file demonstrates why `DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top` must
 take `Ring R` and not `Semiring R`.
 -/
 
@@ -57,9 +57,9 @@ theorem withSign.isCompl : IsCompl ℤ≥0 ℤ≤0 := by
     · exact Submodule.mem_sup_left (mem_withSign_one.mpr hp)
     · exact Submodule.mem_sup_right (mem_withSign_neg_one.mpr hn)
 
-def withSign.independent : CompleteLattice.Independent withSign := by
+def withSign.independent : iSupIndep withSign := by
   apply
-    (CompleteLattice.independent_pair UnitsInt.one_ne_neg_one _).mpr withSign.isCompl.disjoint
+    (iSupIndep_pair UnitsInt.one_ne_neg_one _).mpr withSign.isCompl.disjoint
   intro i
   fin_cases i <;> simp
 

Counterexamples/OrderedCancelAddCommMonoidWithBounds.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Martin Dvorak
 -/
 import Mathlib.Algebra.Order.Monoid.Defs
-import Mathlib.Order.BoundedOrder
+import Mathlib.Order.BoundedOrder.Lattice
 
 /-!
 # Do not combine OrderedCancelAddCommMonoid with BoundedOrder