chore: bump lean

Mathport.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Daniel Selsam
 -/
 import Mathlib.Data.List.EditDistance.Defs
-import Lake.Load.Elab
+import Lake.Load.Lean.Elab
 import Mathport.Binary
 import Mathport.Syntax
 

Mathport/Binary/Apply.lean

@@ -379,14 +379,14 @@ def applyInductiveDecl (lps : List Name) (nParams : Nat) (indType : InductiveTyp
   | none => pure ()
 
 where
-  mkAuxDecls (name : Name) : BinportM Unit := do
+  mkAuxDecls (name : Name) : BinportM Unit := liftMetaM do
     try
       -- these may fail for the invalid inductive types currently being accepted
       -- by the temporary patch
       -- https://github.com/dselsam/lean4/commit/1bef1cb3498cf81f93095bda16ed8bc65af42535
       mkRecOn name
       mkCasesOn name
-      liftMetaM $ Lean.mkNoConfusion name
+      Lean.mkNoConfusion name
       mkBelow name
       mkIBelow name
       mkBRecOn name

lake-manifest.json

@@ -1,10 +1,11 @@
-{"version": "1.0.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "555ec79bc6effe7009036184a5f73f7d8d4850ed",
+   "scope": "leanprover-community",
+   "rev": "bba0af6e930ebcbabfacf021b21dd881d58aaa9d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,6 +14,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
+   "scope": "leanprover-community",
    "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
@@ -22,7 +24,8 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "aea83a8a13ae4144e9e5d86f8749238f17814ef3",
+   "scope": "leanprover-community",
+   "rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,25 +34,28 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9",
+   "scope": "leanprover-community",
+   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.38",
+   "inputRev": "v0.0.39",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
+   "scope": "",
    "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96",
+   "scope": "leanprover-community",
+   "rev": "d366a602cc4a325a6f9db3a3991dfa6d6cf409c5",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +64,8 @@
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "754ba19de1471fd928c4fa0cc102d1f06f90e902",
+   "scope": "",
+   "rev": "4f76c653e261de1da9ba36bac58f4ca0eb22cc38",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

lakefile.lean

@@ -9,7 +9,7 @@ require mathlib from git "https://github.com/leanprover-community/mathlib4"@"mas
 
 target ffi.o pkg : FilePath := do
   let oFile := pkg.buildDir / "c" / "ffi.o"
-  let srcJob ← inputFile <| pkg.dir / "Mathport" / "FFI.cpp"
+  let srcJob ← inputTextFile <| pkg.dir / "Mathport" / "FFI.cpp"
   let flags := #["-I", (← getLeanIncludeDir).toString, "-fPIC"]
   buildO oFile srcJob flags (compiler := "c++")
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.9.0-rc3
+leanprover/lean4:v4.10.0-rc1