Trigger CI for leanprover-community/batteries#1063

.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/dependabot.yml

@@ -3,7 +3,8 @@ version: 2  # Specifies the version of the Dependabot configuration file format
 updates:
   # Configuration for dependency updates
   - package-ecosystem: "github-actions"  # Specifies the ecosystem to check for updates
-    directory: "/"  # Specifies the directory to check for dependencies; "/" means the root directory
+    directories: 
+      - "/.github/*" # covers `build.in.yml` as well, which is not in `.github/workflows/` because it shouldn't be run in CI.
     schedule:
       # Check for updates to GitHub Actions every month
       interval: "monthly"

.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

@@ -100,8 +100,13 @@ 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"$'\n- '"$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
 

.github/workflows/maintainer_bors.yml

@@ -103,7 +103,6 @@ jobs:
 
       - uses: actions/checkout@v4
         with:
-          ref: master
           sparse-checkout: |
             scripts/zulip_emoji_merge_delegate.py
 

.github/workflows/zulip_emoji_awaiting_author.yaml

@@ -0,0 +1,34 @@
+on:
+  pull_request:
+    types: [labeled, unlabeled]
+jobs:
+  set_pr_emoji:
+    if: github.event.label.name == 'awaiting-author'
+    runs-on: ubuntu-latest
+    steps:
+    - name: Checkout mathlib repository
+      uses: actions/checkout@v4
+      with:
+          sparse-checkout: |
+            scripts/zulip_emoji_merge_delegate.py
+
+    - name: Set up Python
+      uses: actions/setup-python@v5
+      with:
+        python-version: '3.x'
+
+    - name: Install dependencies
+      run: |
+        python -m pip install --upgrade pip
+        pip install zulip
+
+    - name: Add or remove emoji
+      env:
+        ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
+        ZULIP_EMAIL: [email protected]
+        ZULIP_SITE: https://leanprover.zulipchat.com
+        PR_NUMBER: ${{ github.event.number}}
+        LABEL_STATUS: ${{ github.event.action }}
+      run: |
+        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" "$LABEL_STATUS" "$PR_NUMBER"

Archive/Imo/Imo2024Q5.lean

@@ -229,7 +229,7 @@ lemma find?_eq_eq_find?_le {l : List (Cell N)} {r : Fin (N + 2)} (hne : l ≠ []
     by_cases h : head.1 = r
     · simp [h]
     · have h' : ¬(r ≤ head.1) := fun hr' ↦ h (le_antisymm hf hr')
-      simp only [h, decide_False, Bool.false_eq_true, not_false_eq_true, List.find?_cons_of_neg, h']
+      simp only [h, decide_false, Bool.false_eq_true, not_false_eq_true, List.find?_cons_of_neg, h']
       rcases tail with ⟨⟩ | ⟨htail, ttail⟩
       · simp
       · simp only [List.chain'_cons] at ha
@@ -315,7 +315,7 @@ lemma Path.tail_findFstEq (p : Path N) {r : Fin (N + 2)} (hr : r ≠ 0) :
     rcases cells with ⟨⟩ | ⟨head, tail⟩
     · simp at nonempty
     · simp only [List.head_cons] at head_first_row
-      simp only [List.find?_cons, head_first_row, hr.symm, decide_False]
+      simp only [List.find?_cons, head_first_row, hr.symm, decide_false]
       rfl
   · simp_rw [Path.tail, if_neg h]
 
@@ -329,7 +329,7 @@ lemma Path.tail_firstMonster (p : Path N) (m : MonsterData N) :
     · simp at nonempty
     · simp only [List.head_cons] at head_first_row
       simp only [List.find?_cons, head_first_row,
-        m.not_mem_monsterCells_of_fst_eq_zero head_first_row, decide_False]
+        m.not_mem_monsterCells_of_fst_eq_zero head_first_row, decide_false]
       rfl
   · simp_rw [Path.tail, if_neg h]
 
@@ -352,17 +352,17 @@ lemma Path.firstMonster_eq_of_findFstEq_mem {p : Path N} {m : MonsterData N}
     · simp only [List.head_cons] at head_first_row
       simp only [List.getElem_cons_succ] at h1
       simp only [List.length_cons, lt_add_iff_pos_left, List.length_pos_iff_ne_nil] at hl
-      simp only [m.not_mem_monsterCells_of_fst_eq_zero head_first_row, decide_False,
+      simp only [m.not_mem_monsterCells_of_fst_eq_zero head_first_row, decide_false,
         Bool.false_eq_true, not_false_eq_true, List.find?_cons_of_neg, head_first_row,
         Fin.zero_eq_one_iff, Nat.reduceEqDiff, Option.some_get]
-      simp only [findFstEq, head_first_row, Fin.zero_eq_one_iff, Nat.reduceEqDiff, decide_False,
+      simp only [findFstEq, head_first_row, Fin.zero_eq_one_iff, Nat.reduceEqDiff, decide_false,
         Bool.false_eq_true, not_false_eq_true, List.find?_cons_of_neg] at h
       rcases tail with ⟨⟩ | ⟨htail, ttail⟩
       · simp at hl
       · simp only [List.getElem_cons_zero] at h1
         have h1' : htail.1 = 1 := by simp [Fin.ext_iff, h1]
-        simp only [h1', decide_True, List.find?_cons_of_pos, Option.get_some] at h
-        simp only [h1', h, decide_True, List.find?_cons_of_pos]
+        simp only [h1', decide_true, List.find?_cons_of_pos, Option.get_some] at h
+        simp only [h1', h, decide_true, List.find?_cons_of_pos]
   case ind p ht =>
     have h1 : (1 : Fin (N + 2)) ≠ 0 := by simp
     rw [p.tail_findFstEq h1, p.tail_firstMonster m] at ht
@@ -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

Archive/MiuLanguage/Basic.lean

@@ -106,9 +106,7 @@ instance : Repr MiuAtom :=
 
 /-- For simplicity, an `Miustr` is just a list of elements of type `MiuAtom`.
 -/
-def Miustr :=
-  List MiuAtom
-deriving Append
+abbrev Miustr := List MiuAtom
 
 instance : Membership MiuAtom Miustr := by unfold Miustr; infer_instance
 

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/HomogeneousPrimeNotPrime.lean

@@ -110,13 +110,8 @@ theorem grading.right_inv : Function.RightInverse (coeLinearMap (grading R)) gra
   induction' zz using DirectSum.induction_on with i zz d1 d2 ih1 ih2
   · simp only [map_zero]
   · rcases i with (_ | ⟨⟨⟩⟩) <;> rcases zz with ⟨⟨a, b⟩, hab : _ = _⟩ <;> dsimp at hab <;>
-      cases hab <;>
-      -- Porting note: proof was `decide`
-      -- now we need a `simp` and two `erw` subproofs...
-      simp only [coeLinearMap_of, decompose, AddMonoidHom.coe_mk,
-        ZeroHom.coe_mk, sub_self, sub_zero]
-    · erw [map_zero (of (grading R ·) 1), add_zero]; rfl
-    · erw [map_zero (of (grading R ·) 0), zero_add]; rfl
+      -- Porting note: proof was `decide` (without reverting any free variables).
+      cases hab <;> decide +revert
   · simp only [map_add, ih1, ih2]
 
 theorem grading.left_inv : Function.LeftInverse (coeLinearMap (grading R)) grading.decompose :=

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