chore: bump lean

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)
 

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"}}]}

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
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-07-15
+leanprover/lean4:nightly-2023-07-24