Merge branch 'master' into J-Simplicity

Author: AntoineChambert-Loir

Cache/Requests.lean

@@ -13,6 +13,9 @@ namespace Cache.Requests
 
 open System (FilePath)
 
+/-- The full name of the main Mathlib GitHub repository. -/
+def MATHLIBREPO := "leanprover-community/mathlib4"
+
 /--
 Structure to hold repository information with priority ordering
 -/
@@ -37,7 +40,7 @@ def isRemoteURL (url : String) : Bool :=
 /--
 Helper function to get repository from a remote name
 -/
-def getRepoFromRemote (mathlibDepPath : FilePath) (remoteName : String) (errorContext : String) : IO String := do
+def getRepoFromRemote (mathlibDepPath : FilePath) (remoteName : String) (errorContext : String) : IO (Option String) := do
   -- If the remote is already a valid URL, attempt to extract the repo from it. This happens with `gh pr checkout`
   if isRemoteURL remoteName then
     repoFromURL remoteName
@@ -46,23 +49,25 @@ def getRepoFromRemote (mathlibDepPath : FilePath) (remoteName : String) (errorCo
   -- standard name like `origin` or `upstream` or it errors out.
   let out ← IO.Process.output
     {cmd := "git", args := #["remote", "get-url", remoteName], cwd := mathlibDepPath}
-  -- If `git remote get-url` fails then bail out with an error to help debug
+  -- If `git remote get-url` fails then return none.
   let output := out.stdout.trimAscii
   unless out.exitCode == 0 do
-    throw <| IO.userError s!"\
-      Failed to run Git to determine Mathlib's repository from {remoteName} remote (exit code: {out.exitCode}).\n\
+    IO.println s!"\
+      Warning: failed to run Git to determine Mathlib's repository from {remoteName} remote\n\
       {errorContext}\n\
-      Stdout:\n{output}\nStderr:\n{out.stderr.trimAscii}\n"
+      Continuing to fetch the cache from {MATHLIBREPO}."
+    return none
   -- Finally attempt to extract the repository from the remote URL returned by `git remote get-url`
   repoFromURL output.copy
-where repoFromURL (url : String) : IO String := do
+where repoFromURL (url : String) : IO (Option String) := do
     if let some repo := extractRepoFromUrl url then
-      return repo
+      return some repo
     else
-      throw <| IO.userError s!"\
-        Failed to extract repository from remote URL: {url}.\n\
+      IO.println s!"\
+        Warning: Failed to extract repository from remote URL: {url}.\n\
         {errorContext}\n\
-        Please ensure the remote URL is valid and points to a GitHub repository."
+        Continuing to fetch the cache from {MATHLIBREPO}."
+      return none
 
 /--
 Finds the remote name that points to `leanprover-community/mathlib4` repository.
@@ -146,7 +151,7 @@ Attempts to determine the GitHub repository of a version of Mathlib from its Git
 If the current commit coincides with a PR ref, it will determine the source fork
 of that PR rather than just using the origin remote.
 -/
-def getRemoteRepo (mathlibDepPath : FilePath) : IO RepoInfo := do
+def getRemoteRepo (mathlibDepPath : FilePath) : IO (Option RepoInfo) := do
 
   -- Since currently we need to push a PR to `leanprover-community/mathlib` build a user cache,
   -- we check if we are a special branch or a branch with PR. This leaves out non-PRed fork
@@ -176,7 +181,7 @@ def getRemoteRepo (mathlibDepPath : FilePath) : IO RepoInfo := do
       let repo := "leanprover-community/mathlib4-nightly-testing"
       let cacheService := if useCloudflareCache then "Cloudflare" else "Azure"
       IO.println s!"Using cache ({cacheService}) from nightly-testing remote: {repo}"
-      return {repo := repo, useFirst := true}
+      return some {repo := repo, useFirst := true}
 
     -- Only search for PR refs if we're not on a regular branch like master, bump/*, or nightly-testing*
     -- let isSpecialBranch := branchName == "master" || branchName.startsWith "bump/" ||
@@ -234,11 +239,16 @@ def getRemoteRepo (mathlibDepPath : FilePath) : IO RepoInfo := do
     -- If no tracking remote is configured, fall back to origin
     "origin"
 
-  let repo ← getRepoFromRemote mathlibDepPath remoteName
+  let repo? ← getRepoFromRemote mathlibDepPath remoteName
     s!"Ensure Git is installed and the '{remoteName}' remote points to its GitHub repository."
   let cacheService := if useCloudflareCache then "Cloudflare" else "Azure"
-  IO.println s!"Using cache ({cacheService}) from {remoteName}: {repo}"
-  return {repo := repo, useFirst := false}
+  match repo? with
+  | some repo =>
+    IO.println s!"Using cache ({cacheService}) from {remoteName}: {repo?}"
+    return some {repo := repo, useFirst := false}
+  | none =>
+    IO.println s!"Using cache ({cacheService}) from {MATHLIBREPO}."
+    return none
 
 /-- Public URL for mathlib cache -/
 initialize URL : String ← do
@@ -275,9 +285,6 @@ def getUploadAuth : IO UploadAuth := do
     throw <| IO.userError
       "environment variable MATHLIB_CACHE_AZURE_BEARER_TOKEN or MATHLIB_CACHE_SAS must be set to upload caches"
 
-/-- The full name of the main Mathlib GitHub repository. -/
-def MATHLIBREPO := "leanprover-community/mathlib4"
-
 /--
 Given a file name like `"1234.tar.gz"`, makes the URL to that file on the server.
 
@@ -663,16 +670,19 @@ def getFiles
       isMathlibRoot mathlibDepPath
     if failed > 0 then IO.Process.exit 1
   else
-    let repoInfo ← getRemoteRepo (← read).mathlibDepPath
+    let repoInfo? ← getRemoteRepo (← read).mathlibDepPath
 
     -- Build list of repositories to download from in order
     let repos : List String :=
-      if repoInfo.repo == MATHLIBREPO then
-        [repoInfo.repo]
-      else if repoInfo.useFirst then
-        [repoInfo.repo, MATHLIBREPO]
+      if let some repoInfo := repoInfo? then
+        if repoInfo.repo == MATHLIBREPO then
+          [MATHLIBREPO]
+        else if repoInfo.useFirst then
+          [repoInfo.repo, MATHLIBREPO]
+        else
+          [MATHLIBREPO, repoInfo.repo]
       else
-        [MATHLIBREPO, repoInfo.repo]
+        [MATHLIBREPO]
 
     let mut failed : Nat := 0
     for h : i in [0:repos.length] do

Mathlib/Algebra/Exact.lean

@@ -92,7 +92,7 @@ lemma iff_rangeFactorization [One P] (hg : 1 ∈ Set.range g) :
     MulExact f g ↔ MulExact ((↑) : Set.range f → N) (Set.rangeFactorization g) := by
   letI : One (Set.range g) := ⟨⟨1, hg⟩⟩
   have : ((1 : Set.range g) : P) = 1 := rfl
-  simp [MulExact, Set.rangeFactorization, Subtype.ext_iff, this]
+  simp [MulExact, Subtype.ext_iff, this]
 
 /-- If two maps `f : M → N` and `g : N → P` are exact, then the induced maps
 `Set.range f → N → Set.range g` are exact.
@@ -430,8 +430,7 @@ def Exact.splitInjectiveEquiv
     · intro x y e
       simp only [prod_apply, Pi.prod, Prod.mk.injEq] at e
       obtain ⟨z, hz⟩ := (h (x - y)).mp (by simpa [sub_eq_zero] using e.2)
-      suffices z = 0 by rw [← sub_eq_zero, ← hz, this, map_zero]
-      rw [← h₁ z, hz, map_sub, e.1, sub_self]
+      rw [← sub_eq_zero, ← hz, ← h₁ z, hz, map_sub, e.1, sub_self, map_zero]
     · rintro ⟨x, y⟩
       obtain ⟨y, rfl⟩ := hg y
       refine ⟨f x + y - f (l.1 y), by ext <;> simp [h₁, h₂]⟩

Mathlib/Algebra/Star/Basic.lean

@@ -485,11 +485,8 @@ protected instance Invertible.star {R : Type*} [MulOneClass R] [StarMul R] (r :
 
 theorem star_invOf {R : Type*} [Monoid R] [StarMul R] (r : R) [Invertible r]
     [Invertible (star r)] : star (⅟r) = ⅟(star r) := by
-  have : star (⅟r) = star (⅟r) * ((star r) * ⅟(star r)) := by
-    simp only [mul_invOf_self, mul_one]
-  rw [this, ← mul_assoc]
-  have : (star (⅟r)) * (star r) = star 1 := by rw [← star_mul, mul_invOf_self]
-  rw [this, star_one, one_mul]
+  rw [← mul_one (star (⅟r)), ← mul_invOf_self (star r), ← mul_assoc, ← star_mul]
+  simp
 
 section Regular
 

Mathlib/CategoryTheory/Sites/Grothendieck.lean

@@ -306,7 +306,7 @@ theorem isGLB_sInf (s : Set (GrothendieckTopology C)) : IsGLB s (sInf s) := by
 definitionally equal to the bottom and top respectively.
 -/
 instance : CompleteLattice (GrothendieckTopology C) :=
-  CompleteLattice.copy (completeLatticeOfInf _ isGLB_sInf) _ rfl (discrete C)
+  fast_instance% CompleteLattice.copy (completeLatticeOfInf _ isGLB_sInf) _ rfl (discrete C)
     (by
       apply le_antisymm
       · exact (completeLatticeOfInf _ isGLB_sInf).le_top (discrete C)

Mathlib/Init.lean

@@ -123,6 +123,7 @@ register_linter_set linter.nightlyRegressionSet :=
 register_linter_set linter.weeklyLintSet :=
   linter.tacticAnalysis.mergeWithGrind
   linter.style.docStringVerso
+  linter.tacticAnalysis.verifyGrindOnly
 
 -- Check that all linter options mentioned in the mathlib standard linter set exist.
 open Lean Elab.Command Linter Mathlib.Linter Style UnusedInstancesInType

Mathlib/Order/Copy.lean

@@ -24,39 +24,35 @@ universe u
 
 variable {α : Type u}
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- A function to create a provable equal copy of a top order
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def OrderTop.copy {h : LE α} {h' : LE α} (c : @OrderTop α h')
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
     (le_eq : ∀ x y : α, (@LE.le α h) x y ↔ x ≤ y) : @OrderTop α h :=
   @OrderTop.mk α h { top := top } fun _ ↦ by simp [eq_top, le_eq]
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- A function to create a provable equal copy of a bottom order
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def OrderBot.copy {h : LE α} {h' : LE α} (c : @OrderBot α h')
     (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
     (le_eq : ∀ x y : α, (@LE.le α h) x y ↔ x ≤ y) : @OrderBot α h :=
   @OrderBot.mk α h { bot := bot } fun _ ↦ by simp [eq_bot, le_eq]
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- A function to create a provable equal copy of a bounded order
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def BoundedOrder.copy {h : LE α} {h' : LE α} (c : @BoundedOrder α h')
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
     (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
     (le_eq : ∀ x y : α, (@LE.le α h) x y ↔ x ≤ y) : @BoundedOrder α h :=
   @BoundedOrder.mk α h (@OrderTop.mk α h { top := top } (fun _ ↦ by simp [eq_top, le_eq]))
     (@OrderBot.mk α h { bot := bot } (fun _ ↦ by simp [eq_bot, le_eq]))
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- A function to create a provable equal copy of a lattice
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def Lattice.copy (c : Lattice α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)
@@ -75,23 +71,19 @@ def Lattice.copy (c : Lattice α)
   inf_le_right := by intros; simp [eq_le, eq_inf]
   le_inf := by intro _ _ _ hac hbc; simp_rw [eq_le] at hac hbc ⊢; simp [eq_inf, hac, hbc]
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
-set_option backward.isDefEq.respectTransparency false in
 /-- A function to create a provable equal copy of a distributive lattice
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def DistribLattice.copy (c : DistribLattice α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)
     (inf : α → α → α) (eq_inf : inf = (by infer_instance : Min α).min) : DistribLattice α where
   toLattice := Lattice.copy (@DistribLattice.toLattice α c) le eq_le sup eq_sup inf eq_inf
   le_sup_inf := by intros; simp +instances [eq_le, eq_sup, eq_inf, le_sup_inf]
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
-set_option backward.isDefEq.respectTransparency false in
 /-- A function to create a provable equal copy of a generalised heyting algebra
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def GeneralizedHeytingAlgebra.copy (c : GeneralizedHeytingAlgebra α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
@@ -105,11 +97,9 @@ def GeneralizedHeytingAlgebra.copy (c : GeneralizedHeytingAlgebra α)
   himp := himp
   le_himp_iff _ _ _ := by simp +instances [eq_le, eq_himp, eq_inf]
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
-set_option backward.isDefEq.respectTransparency false in
 /-- A function to create a provable equal copy of a generalised co-Heyting algebra
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def GeneralizedCoheytingAlgebra.copy (c : GeneralizedCoheytingAlgebra α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
@@ -123,11 +113,9 @@ def GeneralizedCoheytingAlgebra.copy (c : GeneralizedCoheytingAlgebra α)
   sdiff := sdiff
   sdiff_le_iff := by simp +instances [eq_le, eq_sdiff, eq_sup]
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
-set_option backward.isDefEq.respectTransparency false in
 /-- A function to create a provable equal copy of a heyting algebra
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def HeytingAlgebra.copy (c : HeytingAlgebra α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
@@ -145,11 +133,9 @@ def HeytingAlgebra.copy (c : HeytingAlgebra α)
   compl := compl
   himp_bot := by simp +instances [eq_le, eq_himp, eq_bot, eq_compl]
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
-set_option backward.isDefEq.respectTransparency false in
 /-- A function to create a provable equal copy of a co-Heyting algebra
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def CoheytingAlgebra.copy (c : CoheytingAlgebra α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
@@ -167,10 +153,9 @@ def CoheytingAlgebra.copy (c : CoheytingAlgebra α)
   hnot := hnot
   top_sdiff := by simp +instances [eq_le, eq_sdiff, eq_top, eq_hnot]
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- A function to create a provable equal copy of a bi-Heyting algebra
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def BiheytingAlgebra.copy (c : BiheytingAlgebra α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
@@ -187,11 +172,9 @@ def BiheytingAlgebra.copy (c : BiheytingAlgebra α)
   __ := CoheytingAlgebra.copy (@BiheytingAlgebra.toCoheytingAlgebra α c) le eq_le top eq_top bot
     eq_bot sup eq_sup inf eq_inf sdiff eq_sdiff hnot eq_hnot
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
-set_option backward.isDefEq.respectTransparency false in
 /-- A function to create a provable equal copy of a complete lattice
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def CompleteLattice.copy (c : CompleteLattice α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
@@ -211,10 +194,9 @@ def CompleteLattice.copy (c : CompleteLattice α)
   le_top := by intros; simp +instances [eq_le, eq_top]
   bot_le := by intros; simp +instances [eq_le, eq_bot]
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- A function to create a provable equal copy of a frame with possibly different definitional
 equalities. -/
+@[implicit_reducible]
 def Frame.copy (c : Frame α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
     (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
@@ -229,10 +211,9 @@ def Frame.copy (c : Frame α) (le : α → α → Prop) (eq_le : le = (by infer_
   __ := HeytingAlgebra.copy (@Frame.toHeytingAlgebra α c)
     le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf himp eq_himp compl eq_compl
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- A function to create a provable equal copy of a coframe with possibly different definitional
 equalities. -/
+@[implicit_reducible]
 def Coframe.copy (c : Coframe α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
     (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
@@ -247,10 +228,9 @@ def Coframe.copy (c : Coframe α) (le : α → α → Prop) (eq_le : le = (by in
   __ := CoheytingAlgebra.copy (@Coframe.toCoheytingAlgebra α c)
     le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf sdiff eq_sdiff hnot eq_hnot
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- A function to create a provable equal copy of a complete distributive lattice
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def CompleteDistribLattice.copy (c : CompleteDistribLattice α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (top : α) (eq_top : top = (by infer_instance : Top α).top)
@@ -269,10 +249,9 @@ def CompleteDistribLattice.copy (c : CompleteDistribLattice α)
   __ := Coframe.copy (@CompleteDistribLattice.toCoframe α c) le eq_le top eq_top bot eq_bot sup
     eq_sup inf eq_inf sdiff eq_sdiff hnot eq_hnot sSup eq_sSup sInf eq_sInf
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- A function to create a provable equal copy of a conditionally complete lattice
 with possibly different definitional equalities. -/
+@[implicit_reducible]
 def ConditionallyCompleteLattice.copy (c : ConditionallyCompleteLattice α)
     (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le)
     (sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max)

Mathlib/Tactic/TacticAnalysis/Declarations.lean

@@ -596,7 +596,7 @@ Runs the given tactic at each proof step, captures any "Try this:" suggestions,
 then re-runs the suggested tactic to verify it succeeds.
 Only reports failures (where the suggestion doesn't close the goal). -/
 def Mathlib.TacticAnalysis.verifyTryThisSuggestions
-    (tac : Syntax → MVarId → CommandElabM (TSyntax `tactic))
+    (tac : Syntax → MVarId → CommandElabM (Option (TSyntax `tactic)))
     (label : String) : TacticAnalysis.Config where
   run seq := do
     let opts ← getOptions
@@ -608,7 +608,7 @@ def Mathlib.TacticAnalysis.verifyTryThisSuggestions
           withOptions (·.setBool `pp.mvars.anonymous false) do
             return toString (← Meta.ppGoal goal)
         if (hash goalPP) % fraction = 0 then
-          let tac ← tac i.tacI.stx goal
+          if let some tac ← tac i.tacI.stx goal then
           -- Save message state to suppress "Try this:" info messages from grind?
           let savedMessages := (← get).messages
           -- Run tactic and capture InfoTree
@@ -693,3 +693,18 @@ register_option linter.tacticAnalysis.verifyGrindSuggestions : Bool := {
 def verifyGrindSuggestions := verifyTryThisSuggestions
   (fun _ _ => `(tactic| grind? +suggestions))
   "grind? +suggestions"
+
+/-- Verify that replacing `grind` with `grind?` produces a valid `grind only` suggestion. -/
+register_option linter.tacticAnalysis.verifyGrindOnly : Bool := {
+  defValue := false
+}
+
+@[tacticAnalysis linter.tacticAnalysis.verifyGrindOnly,
+   inherit_doc linter.tacticAnalysis.verifyGrindOnly]
+def verifyGrindOnly := verifyTryThisSuggestions
+  (fun stx _ =>
+    return match stx with
+    | .node info ``Lean.Parser.Tactic.grind args => some ⟨.node info ``Lean.Parser.Tactic.grindTrace args⟩
+    | _ => none
+  )
+  "grind?"