Merge pull request #1367 from leanprover-community/master

merge from master

Cache/IO.lean

@@ -100,27 +100,34 @@ def mkDir (path : FilePath) : IO Unit := do
   if !(← path.pathExists) then IO.FS.createDirAll path
 
 /-- Given a path to a Lean file, concatenates the paths to its build files -/
-def mkBuildPaths (path : FilePath) : IO $ Array String := do
+def mkBuildPaths (path : FilePath) : IO $ Array FilePath := do
   let packageDir ← getPackageDir path
   return #[
-    packageDir / LIBDIR / path.withExtension "olean"   |>.toString,
-    packageDir / LIBDIR / path.withExtension "ilean"   |>.toString,
-    packageDir / LIBDIR / path.withExtension "trace"   |>.toString,
-    packageDir / IRDIR  / path.withExtension "c"       |>.toString,
-    packageDir / IRDIR  / path.withExtension "c.trace" |>.toString]
-
-/-- Compresses build files into the local cache -/
+    packageDir / LIBDIR / path.withExtension "olean",
+    packageDir / LIBDIR / path.withExtension "ilean",
+    packageDir / LIBDIR / path.withExtension "trace",
+    packageDir / IRDIR  / path.withExtension "c",
+    packageDir / IRDIR  / path.withExtension "c.trace"]
+
+def allExist (paths : Array FilePath) : IO Bool := do
+  for path in paths do
+    if !(← path.pathExists) then return false
+  pure true
+
+/-- Compresses build files into the local cache and returns an array with the compressed files -/
 def mkCache (hashMap : HashMap) (overwrite : Bool) : IO $ Array String := do
   mkDir CACHEDIR
   IO.println "Compressing cache"
   let mut acc := default
   for (path, hash) in hashMap.toList do
     let zip := hash.asTarGz
     let zipPath := CACHEDIR / zip
-    if overwrite || !(← zipPath.pathExists) then
-      discard $ runCmd "tar" $ #["-I", "gzip -9", "-cf", zipPath.toString] ++
-        (← mkBuildPaths path)
-    acc := acc.push zip
+    let buildPaths ← mkBuildPaths path
+    if ← allExist buildPaths then
+      if (overwrite || !(← zipPath.pathExists)) then
+        discard $ runCmd "tar" $ #["-I", "gzip -9", "-cf", zipPath.toString] ++
+          (buildPaths.map toString)
+      acc := acc.push zip
   return acc
 
 /-- Gets the set of all cached files -/
@@ -153,15 +160,15 @@ def unpackCache (hashMap : HashMap) : IO Unit := do
           "-C", mathlibDepPath.toString]
   else IO.println "No cache files to decompress"
 
-instance : Ord FilePath where
-  compare x y := compare x.toString y.toString
-
 /-- Retrieves the azure token from the file system -/
 def getToken : IO String := do
   let some token ← IO.getEnv "MATHLIB_CACHE_SAS"
     | throw $ IO.userError "environment variable MATHLIB_CACHE_SAS must be set to upload caches"
   return token
 
+instance : Ord FilePath where
+  compare x y := compare x.toString y.toString
+
 /-- Removes all cache files except for what's in the `keep` set -/
 def cleanCache (keep : Lean.RBTree FilePath compare := default) : IO Unit := do
   for path in ← getFilesWithExtension CACHEDIR "gz" do

Mathlib.lean

@@ -147,6 +147,7 @@ import Mathlib.Algebra.Ring.Units
 import Mathlib.Algebra.SMulWithZero
 import Mathlib.Algebra.Star.Basic
 import Mathlib.Algebra.Tropical.Basic
+import Mathlib.Algebra.Tropical.Lattice
 import Mathlib.CategoryTheory.Category.Basic
 import Mathlib.CategoryTheory.Category.KleisliCat
 import Mathlib.CategoryTheory.Category.RelCat
@@ -238,12 +239,16 @@ import Mathlib.Data.List.Card
 import Mathlib.Data.List.Chain
 import Mathlib.Data.List.Defs
 import Mathlib.Data.List.Func
+import Mathlib.Data.List.Infix
 import Mathlib.Data.List.Lemmas
 import Mathlib.Data.List.Lex
+import Mathlib.Data.List.MinMax
 import Mathlib.Data.List.Nodup
 import Mathlib.Data.List.Pairwise
+import Mathlib.Data.List.Palindrome
 import Mathlib.Data.List.Perm
 import Mathlib.Data.List.Range
+import Mathlib.Data.List.TFAE
 import Mathlib.Data.Multiset.Basic
 import Mathlib.Data.Multiset.Nodup
 import Mathlib.Data.Nat.Basic
@@ -315,6 +320,7 @@ import Mathlib.Data.Set.Intervals.Group
 import Mathlib.Data.Set.Intervals.Monoid
 import Mathlib.Data.Set.Intervals.Monotone
 import Mathlib.Data.Set.Intervals.OrdConnected
+import Mathlib.Data.Set.Intervals.OrdConnectedComponent
 import Mathlib.Data.Set.Intervals.OrderIso
 import Mathlib.Data.Set.Intervals.Pi
 import Mathlib.Data.Set.Intervals.ProjIcc
@@ -448,6 +454,7 @@ import Mathlib.Order.Compare
 import Mathlib.Order.CompleteBooleanAlgebra
 import Mathlib.Order.CompleteLattice
 import Mathlib.Order.CompleteLatticeIntervals
+import Mathlib.Order.Concept
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Order.ConditionallyCompleteLattice.Group
 import Mathlib.Order.Copy

Mathlib/Algebra/Tropical/Lattice.lean

@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2021 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky
+
+! This file was ported from Lean 3 source module algebra.tropical.lattice
+! leanprover-community/mathlib commit 6d0adfa76594f304b4650d098273d4366edeb61b
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Algebra.Tropical.Basic
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
+
+/-!
+
+# Order on tropical algebraic structure
+
+This file defines the orders induced on tropical algebraic structures by the underlying type.
+
+## Main declarations
+
+* `ConditionallyCompleteLattice (Tropical R)`
+* `ConditionallyCompleteLinearOrder (Tropical R)`
+
+## Implementation notes
+
+The order induced is the definitionally equal underlying order, which makes the proofs and
+constructions quicker to implement.
+
+-/
+
+
+variable {R S : Type _}
+
+open Tropical
+
+instance [HasSup R] : HasSup (Tropical R) where
+  sup x y := trop (untrop x ⊔ untrop y)
+
+instance [HasInf R] : HasInf (Tropical R) where
+  inf x y := trop (untrop x ⊓ untrop y)
+
+instance [SemilatticeInf R] : SemilatticeInf (Tropical R) :=
+  { instHasInfTropical,
+    Tropical.instPartialOrderTropical with
+    le_inf := fun _ _ _ ↦ @SemilatticeInf.le_inf R _ _ _ _
+    inf_le_left := fun _ _ ↦ inf_le_left
+    inf_le_right := fun _ _ ↦ inf_le_right }
+
+instance [SemilatticeSup R] : SemilatticeSup (Tropical R) :=
+  { instHasSupTropical,
+    Tropical.instPartialOrderTropical with
+    sup_le := fun _ _ _ ↦ @SemilatticeSup.sup_le R _ _ _ _
+    le_sup_left := fun _ _ ↦ le_sup_left
+    le_sup_right := fun _ _ ↦ le_sup_right }
+
+instance [Lattice R] : Lattice (Tropical R) :=
+  { instSemilatticeInfTropical, instSemilatticeSupTropical with }
+
+instance [SupSet R] : SupSet (Tropical R) where supₛ s := trop (supₛ (untrop '' s))
+
+instance [InfSet R] : InfSet (Tropical R) where infₛ s := trop (infₛ (untrop '' s))
+
+instance [ConditionallyCompleteLattice R] : ConditionallyCompleteLattice (Tropical R) :=
+  { @instHasInfTropical R _, @instHasSupTropical R _,
+    instLatticeTropical with
+    le_csupₛ  := fun _s _x hs hx ↦
+      le_csupₛ (untrop_monotone.map_bddAbove hs) (Set.mem_image_of_mem untrop hx)
+    csupₛ_le := fun _s _x hs hx ↦
+      csupₛ_le (hs.image untrop) (untrop_monotone.mem_upperBounds_image hx)
+    le_cinfₛ := fun _s _x hs hx ↦
+      le_cinfₛ (hs.image untrop) (untrop_monotone.mem_lowerBounds_image hx)
+    cinfₛ_le := fun _s _x hs hx ↦
+      cinfₛ_le (untrop_monotone.map_bddBelow hs) (Set.mem_image_of_mem untrop hx) }
+
+instance [ConditionallyCompleteLinearOrder R] : ConditionallyCompleteLinearOrder (Tropical R) :=
+  { instConditionallyCompleteLatticeTropical, Tropical.instLinearOrderTropical with }

Mathlib/Data/List/Defs.lean

@@ -209,16 +209,6 @@ end mapIdxM
 #align list.is_prefix List.isPrefix
 #align list.is_suffix List.isSuffix
 #align list.is_infix List.isInfix
-/-- Notation for `List.isPrefix`
--/
-infixl:50 " <+: " => isPrefix
-/--  Notation for `List.isSuffix`
--/
-infixl:50 " <:+ " => isSuffix
-/-- Notation for `List.isInfix`
--/
-infixl:50 " <:+: " => isInfix
-
 #align list.inits List.inits
 #align list.tails List.tails
 #align list.sublists' List.sublists'