chore: only use mathlib 4

verified-optimization · May 9, 2023 · 5cb71d5 · 5cb71d5
1 parent e8bb773
commit 5cb71d5
Show file tree

Hide file tree

Showing 11 changed files with 16 additions and 81 deletions.
diff --git a/CvxLean.lean b/CvxLean.lean
@@ -1,3 +1 @@
-import Mathbin
-import Optbin
 import CvxLean.Command.Solve
diff --git a/CvxLean/Examples/CovarianceEstimation.lean b/CvxLean/Examples/CovarianceEstimation.lean
@@ -1,12 +1,12 @@
-import Mathbin.Analysis.SpecialFunctions.Trigonometric.Basic
-import Mathbin.LinearAlgebra.QuadraticForm.Basic
+import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
+import Mathlib.LinearAlgebra.QuadraticForm.Basic
 import CvxLean.Lib.Missing.Mathlib
 import CvxLean.Lib.Missing.Vec
 import CvxLean.Syntax.Minimization
 import CvxLean.Tactic.DCP.AtomLibrary
 import CvxLean.Tactic.Conv.ConvOpt
 import CvxLean.Command.Reduction
-import Mathbin.Algebra.Hom.Units
+import Mathlib.Algebra.Hom.Units
 import Mathlib.Algebra.Order.Ring
 import Optbin.CovarianceEstimation
 import CvxLean.Command.Solve

diff --git a/CvxLean/Lib/ExpCone.lean b/CvxLean/Lib/ExpCone.lean
@@ -1,7 +1,4 @@
-import Mathbin.Data.Complex.Exponential
-
-attribute [-instance] Real.hasLt Real.hasLe Real.hasOne Real.hasZero Real.hasMul 
-  Real.linearOrderedField
+import Mathlib.Data.Complex.Exponential
 
 namespace Real
 

diff --git a/CvxLean/Lib/Missing/Matrix.lean b/CvxLean/Lib/Missing/Matrix.lean
@@ -1,8 +1,6 @@
 import Mathlib.Data.Real.Basic
+import Mathlib.Data.Matrix.Basic
 import Mathlib.Data.Array.Defs
-import Mathbin.Data.Real.Basic
-import Mathbin.LinearAlgebra.Matrix.Default
-import Mathbin.LinearAlgebra.Matrix.PosDef
 import CvxLean.Lib.Missing.List
 
 namespace Matrix

diff --git a/CvxLean/Lib/Missing/Real.lean b/CvxLean/Lib/Missing/Real.lean
@@ -1,5 +1,5 @@
 import Mathlib.Data.Real.Basic
-import Mathbin.Data.Complex.Exponential
+import Mathlib.Data.Complex.Exponential
 import Mathbin.Analysis.SpecialFunctions.Log.Basic
 
 attribute [-instance] coeDecidableEq Real.hasLe

diff --git a/CvxLean/Lib/PSDCone.lean b/CvxLean/Lib/PSDCone.lean
@@ -1,4 +1,4 @@
-import Mathbin.LinearAlgebra.Matrix.PosDef
+import Mathbin.LinearAlgebra.Matrix.DotProduct
 
 namespace Real 
 

diff --git a/CvxLeanTest.lean b/CvxLeanTest.lean
@@ -1,4 +1,2 @@
-import Mathbin
-import Optbin
 import CvxLean.Test.All
 import CvxLean.Examples.CovarianceEstimation
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -2,39 +2,26 @@
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
-   {"url": "https://github.com/leanprover-community/mathlib3port.git",
+   {"url": "https://github.com/leanprover-community/mathlib4",
     "subDir?": null,
-    "rev": "e1ef11de97cea5fcd3772993509fa5bd19a2521d",
-    "name": "mathlibport",
-    "inputRev?": "e1ef11de97cea5fcd3772993509fa5bd19a2521d"}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/lean3port.git",
-    "subDir?": null,
-    "rev": "c2e2458ed2ee1c157340b77685da26e7d51676aa",
-    "name": "lean3port",
-    "inputRev?": "c2e2458ed2ee1c157340b77685da26e7d51676aa"}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/mathlib4.git",
-    "subDir?": null,
-    "rev": "bac7310cc18d6ed292606d26ccb5fb9ffc697c7a",
+    "rev": "68b21e12e6d612e77f34febea2e00a9358ce2f76",
     "name": "mathlib",
-    "inputRev?": "bac7310cc18d6ed292606d26ccb5fb9ffc697c7a"}},
+    "inputRev?": "68b21e12e6d612e77f34febea2e00a9358ce2f76"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
-    "rev": "7ac99aa3fac487bec1d5860e751b99c7418298cf",
+    "rev": "c71f94e34c1cda52eef5c93dc9da409ab2727420",
     "name": "Qq",
     "inputRev?": "master"}},
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "ba61f7fec6174d8c7d2796457da5a8d0b0da44c6",
+    "rev": "cdc00b640d0179910ebaa9c931e3b733a04b881c",
     "name": "aesop",
     "inputRev?": "master"}},
-  {"path": {"name": "ffi", "dir": "./ffi"}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "de7e2a79905a3f87cad1ad5bf57045206f9738c7",
+    "rev": "6006307d2ceb8743fea7e00ba0036af8654d0347",
     "name": "std",
     "inputRev?": "main"}}]}
diff --git a/lakefile.lean b/lakefile.lean
@@ -3,10 +3,8 @@ open System Lake DSL
 
 package CvxLean
 
-require mathlibport from git
-  "https://github.com/leanprover-community/mathlib3port.git"@"e1ef11de97cea5fcd3772993509fa5bd19a2521d"
-
-require ffi from "ffi"
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4"@"68b21e12e6d612e77f34febea2e00a9358ce2f76"
 
 @[default_target]
 lean_lib CvxLeanTest

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-02-03
+leanprover/lean4:nightly-2023-05-06
diff --git a/lean_packages/manifest.json b/lean_packages/manifest.json
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:nightly-2023-02-03
		leanprover/lean4:nightly-2023-05-06