From cc8eaa1f1744ae0d2f1c0f34897368c205c822b5 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Fri, 28 Jul 2023 20:35:22 -0400
Subject: [PATCH] chore: bump lean

---
 .../Syntax/Translate/Tactic/Mathlib/Interactive.lean |  2 +-
 lake-manifest.json                                   | 12 ++++++------
 lakefile.lean                                        |  6 +++---
 lean-toolchain                                       |  2 +-
 4 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/Mathport/Syntax/Translate/Tactic/Mathlib/Interactive.lean b/Mathport/Syntax/Translate/Tactic/Mathlib/Interactive.lean
index 3ca296853..4d489c9d1 100644
--- a/Mathport/Syntax/Translate/Tactic/Mathlib/Interactive.lean
+++ b/Mathport/Syntax/Translate/Tactic/Mathlib/Interactive.lean
@@ -170,7 +170,7 @@ open AST3 Mathport.Translate.Parser
 @[tr_tactic triv] def trTriv : TacM Syntax.Tactic := `(tactic| triv)
 
 @[tr_tactic use] def trUse : TacM Syntax.Tactic := do
-  `(tactic| use $(← liftM $ (← parse pExprListOrTExpr).mapM trExpr),*)
+  `(tactic| use $(← liftM $ (← parse pExprListOrTExpr).mapM trExpr):term,*)
 
 @[tr_tactic clear_aux_decl] def trClearAuxDecl : TacM Syntax.Tactic := `(tactic| clear_aux_decl)
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 8a74bbb84..a06df5514 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,9 +4,9 @@
  [{"git":
    {"url": "https://github.com/EdAyers/ProofWidgets4",
     "subDir?": null,
-    "rev": "c43db94a8f495dad37829e9d7ad65483d68c86b8",
+    "rev": "a0c2cd0ac3245a0dade4f925bcfa97e06dd84229",
     "name": "proofwidgets",
-    "inputRev?": "v0.0.11"}},
+    "inputRev?": "v0.0.13"}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,
@@ -16,24 +16,24 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4",
     "subDir?": null,
-    "rev": "e266a1ed2c7099a2b00b0b488cd25022e4c25c05",
+    "rev": "6220e1d0219e245327c603be771b67aea0fdeb4d",
     "name": "mathlib",
     "inputRev?": "master"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
-    "rev": "ae84bd82cca324dc958583d6f1ae08429877dcb0",
+    "rev": "81cc13c524a68d0072561dbac276cd61b65872a6",
     "name": "Qq",
     "inputRev?": "master"}},
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "f04538ab6ad07642368cf11d2702acc0a9b4bcee",
+    "rev": "354432d437fb37738ed93ac6988669d78a870ed0",
     "name": "aesop",
     "inputRev?": "master"}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "dff883c55395438ae2a5c65ad5ddba084b600feb",
+    "rev": "e3c2be331da9ddeef7f82ca363f072a68d7210b3",
     "name": "std",
     "inputRev?": "main"}}]}
diff --git a/lakefile.lean b/lakefile.lean
index 1955e48a5..81fecbca9 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -7,16 +7,16 @@ package mathport
 -- as this commit of mathlib4 uses.
 require mathlib from git "https://github.com/leanprover-community/mathlib4"@"master"
 
-target ffi.o (pkg : Package) : FilePath := do
+target ffi.o pkg : FilePath := do
   let oFile := pkg.buildDir / "c" / "ffi.o"
   let srcJob ← inputFile <| pkg.dir / "Mathport" / "FFI.cpp"
   let flags := #["-I", (← getLeanIncludeDir).toString, "-fPIC"]
   buildO "FFI.c" oFile srcJob flags "c++"
 
-extern_lib libleanffi (pkg : Package) := do
+extern_lib libleanffi (pkg : NPackage `mathport) := do
   let name := nameToStaticLib "leanffi"
   let ffiO ← fetch <| pkg.target ``ffi.o
-  buildStaticLib (pkg.libDir / name) #[ffiO]
+  buildStaticLib (pkg.nativeLibDir / name) #[ffiO]
 
 lean_lib Mathport
 
diff --git a/lean-toolchain b/lean-toolchain
index d2d165ee7..4a54a0e55 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-07-15
+leanprover/lean4:nightly-2023-07-24