Trigger CI for leanprover/lean4#8470

Author: leanprover-community-mathlib4-bot

Archive/ZagierTwoSquares.lean

@@ -19,7 +19,7 @@ has exactly one fixed point, so `|S|` is odd and the involution defined by
 `(x, y, z) ↦ (x, z, y)` also has a fixed point." — [Don Zagier](Zagier1990)
 
 This elementary proof (`Nat.Prime.sq_add_sq'`) is independent of `Nat.Prime.sq_add_sq` in
-`Mathlib.NumberTheory.SumTwoSquares`, which uses the unique factorisation of `ℤ[i]`.
+`Mathlib/NumberTheory/SumTwoSquares.lean`, which uses the unique factorisation of `ℤ[i]`.
 For a geometric interpretation of the piecewise involution (`Zagier.complexInvo`)
 see [Moritz Firsching's MathOverflow answer](https://mathoverflow.net/a/299696).
 -/

Cache/Main.lean

@@ -56,6 +56,16 @@ def curlArgs : List String :=
 def leanTarArgs : List String :=
   ["get", "get!", "pack", "pack!", "unpack", "lookup"]
 
+/-- Parses an optional `--repo` option. -/
+def parseRepo (args : List String) : IO (Option String × List String) := do
+  if let arg :: args := args then
+    if arg.startsWith "--" then
+      if let some repo := arg.dropPrefix? "--repo=" then
+        return (some repo.toString, args)
+      else
+        throw <| IO.userError s!"unknown option: {arg}"
+  return (none, args)
+
 open Cache IO Hashing Requests System in
 def main (args : List String) : IO Unit := do
   if Lean.versionString == "4.8.0-rc1" && Lean.githash == "b470eb522bfd68ca96938c23f6a1bce79da8a99f" then do
@@ -67,6 +77,7 @@ def main (args : List String) : IO Unit := do
     Process.exit 0
   CacheM.run do
 
+  let (repo?, args) ← parseRepo args
   let mut roots : Std.HashMap Lean.Name FilePath ← parseArgs args
   if roots.isEmpty then do
     -- No arguments means to start from `Mathlib.lean`
@@ -82,11 +93,12 @@ def main (args : List String) : IO Unit := do
   if leanTarArgs.contains (args.headD "") then validateLeanTar
   let get (args : List String) (force := false) (decompress := true) := do
     let hashMap ← if args.isEmpty then pure hashMap else hashMemo.filterByRootModules roots.keys
-    getFiles hashMap force force goodCurl decompress
+    getFiles repo? hashMap force force goodCurl decompress
   let pack (overwrite verbose unpackedOnly := false) := do
     packCache hashMap overwrite verbose unpackedOnly (← getGitCommitHash)
   let put (overwrite unpackedOnly := false) := do
-    putFiles (← pack overwrite (verbose := true) unpackedOnly) overwrite (← getToken)
+    let repo := repo?.getD MATHLIBREPO
+    putFiles repo (← pack overwrite (verbose := true) unpackedOnly) overwrite (← getToken)
   match args with
   | "get"  :: args => get args
   | "get!" :: args => get args (force := true)

Cache/Requests.lean

@@ -8,6 +8,29 @@ import Cache.Hashing
 
 namespace Cache.Requests
 
+/-- Attempts to determine the running project's GitHub repository from its `origin` Git remote. -/
+def getRemoteRepo : IO String := do
+  let out ← IO.Process.output {cmd := "git", args := #["remote", "get-url", "origin"]}
+  unless out.exitCode == 0 do
+    throw <| IO.userError s!"\
+      Failed to run Git to determine project repository (exit code: {out.exitCode}).\n\
+      Ensure Git is installed and the `origin` remote points to the project's GitHub repository.\n\
+      Stdout:\n{out.stdout.trim}\nStderr:{out.stderr.trim}\n"
+  -- No strong validation is done here because this is simply used as a smart default
+  -- for `lake exe cache get`, which is freely modifiable by any user.
+  let url := out.stdout.trim.stripSuffix ".git"
+  let repo? : Option String := do
+    let pos ← url.revFind (· == '/')
+    let pos ← url.revFindAux (fun c => c == '/'  || c == ':') pos
+    return url.extract (url.next pos) url.endPos
+  if let some repo := repo? then
+    return repo
+  else
+    throw <| IO.userError s!"\
+      Failed to determine project repository from remote URL.\n\
+      Ensure the `origin` Git remote points to the project's GitHub repository.\n\
+      Detected URL: {url}"
+
 -- FRO cache is flaky so disable until we work out the kinks: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/The.20cache.20doesn't.20work/near/411058849
 def useFROCache : Bool := false
 
@@ -27,18 +50,22 @@ def getToken : IO String := do
 
 open System (FilePath)
 
+/-- 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.
 
 The `f/` prefix means that it's a common file for caching.
 -/
-def mkFileURL (URL fileName : String) : String :=
-  s!"{URL}/f/{fileName}"
+def mkFileURL (repo URL fileName : String) : String :=
+  let pre := if repo == MATHLIBREPO then "" else s!"{repo}/"
+  s!"{URL}/f/{pre}{fileName}"
 
 section Get
 
 /-- Formats the config file for `curl`, containing the list of files to be downloaded -/
-def mkGetConfigContent (hashMap : IO.ModuleHashMap) : IO String := do
+def mkGetConfigContent (repo : String) (hashMap : IO.ModuleHashMap) : IO String := do
   hashMap.toArray.foldlM (init := "") fun acc ⟨_, hash⟩ => do
     let fileName := hash.asLTar
     -- Below we use `String.quote`, which is intended for quoting for use in Lean code
@@ -54,13 +81,13 @@ def mkGetConfigContent (hashMap : IO.ModuleHashMap) : IO String := do
 
     -- Note we append a '.part' to the filenames here,
     -- which `downloadFiles` then removes when the download is successful.
-    pure <| acc ++ s!"url = {mkFileURL URL fileName}\n\
+    pure <| acc ++ s!"url = {mkFileURL repo URL fileName}\n\
       -o {(IO.CACHEDIR / (fileName ++ ".part")).toString.quote}\n"
 
 /-- Calls `curl` to download a single file from the server to `CACHEDIR` (`.cache`) -/
-def downloadFile (hash : UInt64) : IO Bool := do
+def downloadFile (repo : String) (hash : UInt64) : IO Bool := do
   let fileName := hash.asLTar
-  let url := mkFileURL URL fileName
+  let url := mkFileURL repo URL fileName
   let path := IO.CACHEDIR / fileName
   let partFileName := fileName ++ ".part"
   let partPath := IO.CACHEDIR / partFileName
@@ -75,15 +102,16 @@ def downloadFile (hash : UInt64) : IO Bool := do
 
 /-- Call `curl` to download files from the server to `CACHEDIR` (`.cache`).
 Exit the process with exit code 1 if any files failed to download. -/
-def downloadFiles (hashMap : IO.ModuleHashMap) (forceDownload : Bool) (parallel : Bool) :
-    IO Unit := do
+def downloadFiles
+    (repo : String) (hashMap : IO.ModuleHashMap)
+    (forceDownload : Bool) (parallel : Bool) (warnOnMissing : Bool): IO Unit := do
   let hashMap ← if forceDownload then pure hashMap else hashMap.filterExists false
   let size := hashMap.size
   if size > 0 then
     IO.FS.createDirAll IO.CACHEDIR
-    IO.println s!"Attempting to download {size} file(s)"
+    IO.println s!"Attempting to download {size} file(s) from {repo} cache"
     let failed ← if parallel then
-      IO.FS.writeFile IO.CURLCFG (← mkGetConfigContent hashMap)
+      IO.FS.writeFile IO.CURLCFG (← mkGetConfigContent repo hashMap)
       let args := #["--request", "GET", "--parallel", "--fail", "--silent",
           "--retry", "5", -- there seem to be some intermittent failures
           "--write-out", "%{json}\n", "--config", IO.CURLCFG.toString]
@@ -125,15 +153,15 @@ def downloadFiles (hashMap : IO.ModuleHashMap) (forceDownload : Bool) (parallel
           msg := msg ++ s!", {failed} failed"
         IO.eprintln msg
       IO.FS.removeFile IO.CURLCFG
-      if success + failed < done then
+      if warnOnMissing && success + failed < done then
         IO.eprintln "Warning: some files were not found in the cache."
         IO.eprintln "This usually means that your local checkout of mathlib4 has diverged from upstream."
         IO.eprintln "If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later."
         IO.eprintln "Alternatively, if you already have pushed your commits to a branch, this may mean the CI build has failed part-way through building."
       pure failed
     else
       let r ← hashMap.foldM (init := []) fun acc _ hash => do
-        pure <| (← IO.asTask do downloadFile hash) :: acc
+        pure <| (← IO.asTask do downloadFile repo hash) :: acc
       pure <| r.foldl (init := 0) fun f t => if let .ok true := t.get then f else f + 1
     if failed > 0 then
       IO.println s!"{failed} download(s) failed"
@@ -186,12 +214,21 @@ def getProofWidgets (buildDir : FilePath) : IO Unit := do
     throw <| IO.userError s!"Failed to prune ProofWidgets cloud release: {e}"
 
 /-- Downloads missing files, and unpacks files. -/
-def getFiles (hashMap : IO.ModuleHashMap) (forceDownload forceUnpack parallel decompress : Bool) :
-    IO.CacheM Unit := do
+def getFiles
+    (repo? : Option String) (hashMap : IO.ModuleHashMap)
+    (forceDownload forceUnpack parallel decompress : Bool)
+    : IO.CacheM Unit := do
   let isMathlibRoot ← IO.isMathlibRoot
   unless isMathlibRoot do checkForToolchainMismatch
   getProofWidgets (← read).proofWidgetsBuildDir
-  downloadFiles hashMap forceDownload parallel
+  if let some repo := repo? then
+    downloadFiles repo hashMap forceDownload parallel (warnOnMissing := true)
+  else
+    let repo ← getRemoteRepo
+    IO.println s!"Project repository: {repo}"
+    downloadFiles repo hashMap forceDownload parallel (warnOnMissing := false)
+    unless repo == MATHLIBREPO do
+      downloadFiles MATHLIBREPO hashMap forceDownload parallel (warnOnMissing := true)
   if decompress then
     IO.unpackCache hashMap forceUnpack
   else
@@ -209,20 +246,22 @@ def UPLOAD_URL : String :=
     URL
 
 /-- Formats the config file for `curl`, containing the list of files to be uploaded -/
-def mkPutConfigContent (fileNames : Array String) (token : String) : IO String := do
+def mkPutConfigContent (repo : String) (fileNames : Array String) (token : String) : IO String := do
   let token := if useFROCache then "" else s!"?{token}" -- the FRO cache doesn't pass the token here
   let l ← fileNames.toList.mapM fun fileName : String => do
-    pure s!"-T {(IO.CACHEDIR / fileName).toString}\nurl = {mkFileURL UPLOAD_URL fileName}{token}"
+    pure s!"-T {(IO.CACHEDIR / fileName).toString}\nurl = {mkFileURL repo UPLOAD_URL fileName}{token}"
   return "\n".intercalate l
 
 /-- Calls `curl` to send a set of cached files to the server -/
-def putFiles (fileNames : Array String) (overwrite : Bool) (token : String) : IO Unit := do
+def putFiles
+  (repo : String) (fileNames : Array String)
+  (overwrite : Bool) (token : String) : IO Unit := do
   -- TODO: reimplement using HEAD requests?
   let _ := overwrite
   let size := fileNames.size
   if size > 0 then
-    IO.FS.writeFile IO.CURLCFG (← mkPutConfigContent fileNames token)
-    IO.println s!"Attempting to upload {size} file(s)"
+    IO.FS.writeFile IO.CURLCFG (← mkPutConfigContent repo fileNames token)
+    IO.println s!"Attempting to upload {size} file(s) to {repo} cache"
     let args := if useFROCache then
       -- TODO: reimplement using HEAD requests?
       let _ := overwrite

Mathlib.lean

@@ -4875,6 +4875,7 @@ import Mathlib.Order.UpperLower.Hom
 import Mathlib.Order.UpperLower.LocallyFinite
 import Mathlib.Order.UpperLower.Principal
 import Mathlib.Order.UpperLower.Prod
+import Mathlib.Order.UpperLower.Relative
 import Mathlib.Order.WellFounded
 import Mathlib.Order.WellFoundedSet
 import Mathlib.Order.WellQuasiOrder
@@ -5182,6 +5183,8 @@ import Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
 import Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs
 import Mathlib.RingTheory.IntegralDomain
 import Mathlib.RingTheory.Invariant
+import Mathlib.RingTheory.Invariant.Basic
+import Mathlib.RingTheory.Invariant.Profinite
 import Mathlib.RingTheory.IsAdjoinRoot
 import Mathlib.RingTheory.IsPrimary
 import Mathlib.RingTheory.IsTensorProduct

Mathlib/Algebra/AddTorsor/Basic.lean

@@ -11,8 +11,8 @@ import Mathlib.Algebra.Group.Pointwise.Set.Scalar
 /-!
 # Torsors of additive group actions
 
-Further results for torsors, that are not in `Mathlib.Algebra.AddTorsor.Defs` to avoid increasing
-imports there.
+Further results for torsors, that are not in `Mathlib/Algebra/AddTorsor/Defs.lean` to avoid
+increasing imports there.
 -/
 
 open scoped Pointwise

Mathlib/Algebra/Algebra/Defs.lean

@@ -10,14 +10,14 @@ import Mathlib.Algebra.Module.LinearMap.Defs
 
 In this file we define associative unital `Algebra`s over commutative (semi)rings.
 
-* algebra homomorphisms `AlgHom` are defined in `Mathlib.Algebra.Algebra.Hom`;
+* algebra homomorphisms `AlgHom` are defined in `Mathlib/Algebra/Algebra/Hom.lean`;
 
-* algebra equivalences `AlgEquiv` are defined in `Mathlib.Algebra.Algebra.Equiv`;
+* algebra equivalences `AlgEquiv` are defined in `Mathlib/Algebra/Algebra/Equiv.lean`;
 
-* `Subalgebra`s are defined in `Mathlib.Algebra.Algebra.Subalgebra`;
+* `Subalgebra`s are defined in `Mathlib/Algebra/Algebra/Subalgebra.lean`;
 
 * The category `AlgCat R` of `R`-algebras is defined in the file
-  `Mathlib.Algebra.Category.Algebra.Basic`.
+  `Mathlib/Algebra/Category/Algebra/Basic.lean`.
 
 See the implementation notes for remarks about non-associative and non-unital algebras.
 

Mathlib/Algebra/Algebra/Hom.lean

@@ -52,7 +52,7 @@ class AlgHomClass (F : Type*) (R A B : outParam Type*)
   commutes : ∀ (f : F) (r : R), f (algebraMap R A r) = algebraMap R B r
 
 -- For now, don't replace `AlgHom.commutes` and `AlgHomClass.commutes` with the more generic lemma.
--- The file `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` slows down by
+-- The file `Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean` slows down by
 -- 15% if we would do so (see benchmark on PR https://github.com/leanprover-community/mathlib4/pull/18040).
 -- attribute [simp] AlgHomClass.commutes
 

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -13,7 +13,7 @@ import Mathlib.RingTheory.SimpleRing.Basic
 In this file we define `Subalgebra`s and the usual operations on them (`map`, `comap`).
 
 The `Algebra.adjoin` operation and complete lattice structure can be found in
-`Mathlib.Algebra.Algebra.Subalgebra.Lattice`.
+`Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean`.
 -/
 
 universe u u' v w w'

Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

@@ -11,7 +11,7 @@ import Mathlib.Algebra.Algebra.Subalgebra.Basic
 
 In this file we define `Algebra.adjoin` and the complete lattice structure on subalgebras.
 
-More lemmas about `adjoin` can be found in `Mathlib.RingTheory.Adjoin.Basic`.
+More lemmas about `adjoin` can be found in `Mathlib/RingTheory/Adjoin/Basic.lean`.
 -/
 
 assert_not_exists Polynomial

Mathlib/Algebra/Algebra/Subalgebra/Operations.lean

@@ -5,14 +5,15 @@ Authors: Andrew Yang, Antoine Chambert-Loir
 -/
 import Mathlib.Algebra.Algebra.Subalgebra.Basic
 import Mathlib.RingTheory.Ideal.Maps
+import Mathlib.Algebra.Ring.Action.Submonoid
 
 /-!
 # More operations on subalgebras
 
-In this file we relate the definitions in `Mathlib.RingTheory.Ideal.Operations` to subalgebras.
-The contents of this file are somewhat random since both `Mathlib.Algebra.Algebra.Subalgebra.Basic`
-and `Mathlib.RingTheory.Ideal.Operations` are somewhat of a grab-bag of definitions, and this is
-whatever ends up in the intersection.
+In this file we relate the definitions in `Mathlib/RingTheory/Ideal/Operations.lean` to subalgebras.
+The contents of this file are somewhat random since both
+`Mathlib/Algebra/Algebra/Subalgebra/Basic.lean` and `Mathlib/RingTheory/Ideal/Operations.lean` are
+somewhat of a grab-bag of definitions, and this is whatever ends up in the intersection.
 -/
 
 assert_not_exists Cardinal
@@ -71,3 +72,21 @@ theorem mem_of_span_eq_top_of_smul_pow_mem
   mem_of_finset_sum_eq_one_of_pow_smul_mem S' l.support (↑) l hs (fun x => hs' x.2) hl x H
 
 end Subalgebra
+
+section MulSemiringAction
+
+variable (A B : Type*) [CommRing A] [CommRing B] [Algebra A B]
+variable (G : Type*) [Monoid G] [MulSemiringAction G B] [SMulCommClass G A B]
+
+/-- The set of fixed points under a group action, as a subring. -/
+def FixedPoints.subring : Subring B where
+  __ := FixedPoints.addSubgroup G B
+  __ := FixedPoints.submonoid G B
+
+/-- The set of fixed points under a group action, as a subalgebra. -/
+def FixedPoints.subalgebra : Subalgebra A B where
+  __ := FixedPoints.addSubgroup G B
+  __ := FixedPoints.submonoid G B
+  algebraMap_mem' r := by simp
+
+end MulSemiringAction