bump mathlib version

lecopivo · Aug 18, 2023 · 20890ab · 20890ab
1 parent 363465c
commit 20890ab
Show file tree

Hide file tree

Showing 5 changed files with 27 additions and 17 deletions.
diff --git a/SciLean/Core/FunctionTransformations/Adjoint.lean b/SciLean/Core/FunctionTransformations/Adjoint.lean
@@ -21,7 +21,7 @@ variable
 
 
 -- TODO: move to mathlib
-instance {E : ι → Type _} [∀ i, UniformSpace (E i)] [∀ i, CompleteSpace (E i)] : CompleteSpace (PiLp 2 E) := by unfold PiLp; infer_instance
+instance {E : ι → Type _} [∀ i, UniformSpace (E i)] [∀ i, CompleteSpace (E i)] : CompleteSpace (PiLp 2 E) := by unfold PiLp; unfold WithLp; infer_instance
 
 
 -- Set up custom notation for adjoint. Mathlib's notation for adjoint seems to be broken

diff --git a/SciLean/Core/FunctionTransformations/RevCDeriv.lean b/SciLean/Core/FunctionTransformations/RevCDeriv.lean
@@ -647,7 +647,7 @@ def HPow.hPow.arg_a0.revCDeriv_rule
       (ydf.1 ^ n, fun dx' => (n * (conj ydf.1 ^ (n-1))) • ydf.2 dx') :=
 by 
   have ⟨_,_⟩ := hf
-  unfold revCDeriv; simp; ftrans; ftrans; simp; sorry_proof 
+  unfold revCDeriv; simp; ftrans; ftrans; sorry_proof
   -- just missing (a * b) • x = b • a • x
 
 #exit

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -1,39 +1,51 @@
-{"version": 4,
+{"version": 5,
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
    {"url": "https://github.com/EdAyers/ProofWidgets4",
     "subDir?": null,
-    "rev": "066001572cec4513a762035b794bd7725f54224d",
+    "rev": "a0c2cd0ac3245a0dade4f925bcfa97e06dd84229",
+    "opts": {},
     "name": "proofwidgets",
-    "inputRev?": "v0.0.7"}},
+    "inputRev?": "v0.0.13",
+    "inherited": true}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,
     "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
+    "opts": {},
     "name": "Cli",
-    "inputRev?": "nightly"}},
+    "inputRev?": "nightly",
+    "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4",
     "subDir?": null,
-    "rev": "eaa216ee095843c23a39937a0dfc2111af74d5c3",
+    "rev": "96f0a9003a1032e51a21b807aa9fe772112b5816",
+    "opts": {},
     "name": "mathlib",
-    "inputRev?": "master"}},
+    "inputRev?": "master",
+    "inherited": false}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
-    "rev": "c71f94e34c1cda52eef5c93dc9da409ab2727420",
+    "rev": "81cc13c524a68d0072561dbac276cd61b65872a6",
+    "opts": {},
     "name": "Qq",
-    "inputRev?": "master"}},
+    "inputRev?": "master",
+    "inherited": true}},
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "ca73109cc40837bc61df8024c9016da4b4f99d4c",
+    "rev": "086c98bb129ca856381d4414dc0afd6e3e4ae2ef",
+    "opts": {},
     "name": "aesop",
-    "inputRev?": "master"}},
+    "inputRev?": "master",
+    "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "e68aa8f5fe47aad78987df45f99094afbcb5e936",
+    "rev": "49353fa54abdac7221fe27f7b57a6ed9ff559d5c",
+    "opts": {},
     "name": "std",
-    "inputRev?": "main"}}]}
+    "inputRev?": "main",
+    "inherited": true}}]}
diff --git a/lakefile.lean b/lakefile.lean
@@ -38,8 +38,6 @@ require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "master
 
 require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "master"
 
-require proofwidgets from git "https://github.com/EdAyers/ProofWidgets4"@"v0.0.7"
-
 set_option linter.unusedVariables false
 
 /--

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-06-20
+leanprover/lean4:nightly-2023-08-17