chore: update lean

Author: digama0

.gitignore

@@ -10,3 +10,4 @@ sources/
 config.oneshot.json
 config.lean.json
 config.mathlib.json
+lakefile.olean

Mathport.lean

@@ -34,7 +34,7 @@ def mathport1 (config : Config) (path : Path) : IO Unit := do
     |>.setBool `pp.rawOnError true
 
   try
-    withImportModulesConst imports.toList (opts := opts) (trustLevel := 0) $ λ env => do
+    withImportModulesConst imports (opts := opts) (trustLevel := 0) $ λ env => do
       let env := env.setMainModule path.mod4
       let cmdCtx : Elab.Command.Context := {
         fileName := path.toLean3 pcfg ".lean" |>.toString

Mathport/Util/Import.lean

@@ -7,4 +7,4 @@ import Lean
 open Lean
 
 @[implemented_by withImportModules]
-opaque withImportModulesConst (imports : List Import) (opts : Options) (trustLevel : UInt32 := 0) (x : Environment → IO α) : IO α
+opaque withImportModulesConst (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0) (x : Environment → IO α) : IO α

lake-manifest.json

@@ -2,6 +2,14 @@
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
+   {"url": "https://github.com/leanprover-community/mathlib4",
+    "subDir?": null,
+    "rev": "8da7f369150d3ab5cb843226b2d91d84c55c0e7e",
+    "opts": {},
+    "name": "mathlib",
+    "inputRev?": "master",
+    "inherited": false}},
+  {"git":
    {"url": "https://github.com/EdAyers/ProofWidgets4",
     "subDir?": null,
     "rev": "44e6673a20fc0449d003983d1e1f472df40f7107",
@@ -17,14 +25,6 @@
     "name": "Cli",
     "inputRev?": "nightly",
     "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/mathlib4",
-    "subDir?": null,
-    "rev": "193761250a9869327056b499a7f49d676ed5e3a9",
-    "opts": {},
-    "name": "mathlib",
-    "inputRev?": "master",
-    "inherited": false}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
@@ -44,7 +44,7 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "ba5e5e3af519b4fc5221ad0fa4b2c87276f1d323",
+    "rev": "67855403d60daf181775fa1ec63b04e70bcc3921",
     "opts": {},
     "name": "std",
     "inputRev?": "main",

lakefile.lean

@@ -11,7 +11,7 @@ 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++"
+  buildO "FFI.c" oFile srcJob flags (compiler := "c++")
 
 extern_lib libleanffi (pkg : NPackage `mathport) := do
   let name := nameToStaticLib "leanffi"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.0.0
+leanprover/lean4:v4.1.0-rc1