Update the lean dependencies and update IList

5 files changed, 12 insertions, 9 deletions

diff --git a/backends/lean/Base.lean b/backends/lean/Base.lean
index 51211704..2077d410 100644
--- a/backends/lean/Base.lean
+++ b/backends/lean/Base.lean
@@ -3,3 +3,4 @@ import Base.Primitives
 import Base.Diverge
 import Base.Arith
 import Base.Progress
+import Base.IList
diff --git a/backends/lean/Base/IList.lean b/backends/lean/Base/IList.lean
index 7e764d63..3db00cbb 100644
--- a/backends/lean/Base/IList.lean
+++ b/backends/lean/Base/IList.lean
@@ -7,7 +7,6 @@ import Base.Arith
 
 namespace List
 
-#check List.get
 def len (ls : List α) : Int :=
   match ls with
   | [] => 0
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 835dc468..35a3c25a 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -15,7 +15,6 @@ namespace Test
   @[pspec]
   theorem vec_index_test (α : Type u) (v: Vec α) (i: Usize) (h: i.val < v.val.length) :
     ∃ x, v.index α i = .ret x := by
-      apply
       sorry
 
   #eval pspecAttr.find? ``Primitives.Vec.index
@@ -195,7 +194,6 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
       args.map Syntax.getId
     else #[]
   trace[Progress] "Ids: {ids}"
-  --if args[0] ≠ some "as" then throwError "Invalid syntax: should be: `progress as ⟨ ... ⟩`"
   progressAsmsOrLookupTheorem ids (firstTac [assumptionTac, Arith.scalarTac])
 
 elab "progress" args:progressArgs : tactic =>
@@ -205,7 +203,6 @@ namespace Test
   open Primitives
 
   set_option trace.Progress true
-  set_option pp.rawOnError true
 
   @[pspec]
   theorem vec_index_test2 (α : Type u) (v: Vec α) (i: Usize) (h: i.val < v.val.length) :
diff --git a/backends/lean/lake-manifest.json b/backends/lean/lake-manifest.json
index f4759ad3..5a089838 100644
--- a/backends/lean/lake-manifest.json
+++ b/backends/lean/lake-manifest.json
@@ -8,26 +8,32 @@
     "name": "proofwidgets",
     "inputRev?": "v0.0.11"}},
   {"git":
+   {"url": "https://github.com/mhuisi/lean4-cli.git",
+    "subDir?": null,
+    "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
+    "name": "Cli",
+    "inputRev?": "nightly"}},
+  {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "cc5d11f24e1b92db65ec3389bb5142f4b2d7670e",
+    "rev": "fa05951a270fef2873666c46f138e90338cd48d6",
     "name": "mathlib",
     "inputRev?": null}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
-    "rev": "c71f94e34c1cda52eef5c93dc9da409ab2727420",
+    "rev": "c0d9516f44d07feee01c1103c8f2f7c24a822b55",
     "name": "Qq",
     "inputRev?": "master"}},
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "ca73109cc40837bc61df8024c9016da4b4f99d4c",
+    "rev": "f04538ab6ad07642368cf11d2702acc0a9b4bcee",
     "name": "aesop",
     "inputRev?": "master"}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "e68aa8f5fe47aad78987df45f99094afbcb5e936",
+    "rev": "dff883c55395438ae2a5c65ad5ddba084b600feb",
     "name": "std",
     "inputRev?": "main"}}]}
diff --git a/backends/lean/lean-toolchain b/backends/lean/lean-toolchain
index 42e7d786..334c5053 100644
--- a/backends/lean/lean-toolchain
+++ b/backends/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-06-20
\ No newline at end of file
+leanprover/lean4:nightly-2023-07-12
\ No newline at end of file