Bump lean and mathlib

Loogle.lean

@@ -109,7 +109,7 @@ unsafe def work (opts : LoogleOptions) (act : CoreM Unit) : IO Unit := do
   then searchPathRef.set [p]
   else searchPathRef.set compileTimeSearchPath
 
-  let imports := [{module := opts.module.toName}, {module := `Mathlib.Tactic.Find}]
+  let imports := #[{module := opts.module.toName}, {module := `Mathlib.Tactic.Find}]
   withImportModules imports {} 0 fun env => do
     let ctx := {fileName := "/", fileMap := Inhabited.default}
     let state := {env}

flake.nix

@@ -1,18 +1,18 @@
 {
-  inputs.lean.url = github:nomeata/lean4/joachim/nix-dir-as-src;
+  inputs.lean.url = github:leanprover/lean4/v4.1.0-rc1;
 
   inputs.nixpkgs.url = github:NixOS/nixpkgs;
   inputs.nixpkgs.follows = "lean/nixpkgs";
 
   inputs.mathlib4.url = "github:leanprover-community/mathlib4/joachim/find";
   inputs.mathlib4.flake = false;
-  inputs.std4.url = "github:leanprover/std4/7194b6b9b074e15c490e59491843bcd0f0feda68";
+  inputs.std4.url = "github:leanprover/std4/67855403d60daf181775fa1ec63b04e70bcc3921";
   inputs.std4.flake = false;
-  inputs.quote4.url = "github:gebner/quote4/81cc13c524a68d0072561dbac276cd61b65872a6";
+  inputs.quote4.url = "github:gebner/quote4/e75daed95ad1c92af4e577fea95e234d7a8401c1";
   inputs.quote4.flake = false;
-  inputs.aesop.url = "github:JLimperg/aesop/086c98bb129ca856381d4414dc0afd6e3e4ae2ef";
+  inputs.aesop.url = "github:JLimperg/aesop/1a0cded2be292b5496e659b730d2accc742de098";
   inputs.aesop.flake = false;
-  inputs.ProofWidgets.url = "github:EdAyers/ProofWidgets4/a0c2cd0ac3245a0dade4f925bcfa97e06dd84229";
+  inputs.ProofWidgets.url = "github:EdAyers/ProofWidgets4/65bba7286e2395f3163fd0277110578f19b8170f";
   inputs.ProofWidgets.flake = false;
 
   outputs = { self, nixpkgs, ...}@inputs:
@@ -71,7 +71,10 @@
           "ProofWidgets.Component.GoalTypePanel" = [ "build/js/goalTypePanel.js" ];
           "ProofWidgets.Component.Recharts" = [ "build/js/recharts.js" ];
           "ProofWidgets.Component.PenroseDiagram" = [ "build/js/penroseDisplay.js" ];
-          "ProofWidgets.Component.SelectionPanel" = [ "build/js/presentSelection.js" ];
+          "ProofWidgets.Component.Panel.SelectionPanel" = [ "build/js/presentSelection.js" ];
+          "ProofWidgets.Component.Panel.GoalTypePanel" = [ "build/js/goalTypePanel.js" ];
+          "ProofWidgets.Component.MakeEditLink" = [ "build/js/makeEditLink.js" ];
+          "ProofWidgets.Component.OfRpcMethod" = [ "build/js/ofRpcMethod.js" ];
           "ProofWidgets.Component.HtmlDisplay" =
             [ "build/js/htmlDisplay.js" "build/js/htmlDisplayPanel.js"];
           "ProofWidgets.Presentation.Expr" = [ "build/js/exprPresentation.js" ];

lake-manifest.json

@@ -4,47 +4,47 @@
  [{"git":
    {"url": "https://github.com/EdAyers/ProofWidgets4",
     "subDir?": null,
-    "rev": "a0c2cd0ac3245a0dade4f925bcfa97e06dd84229",
+    "rev": "65bba7286e2395f3163fd0277110578f19b8170f",
     "opts": {},
     "name": "proofwidgets",
-    "inputRev?": "v0.0.13",
+    "inputRev?": "v0.0.16",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,
-    "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
+    "rev": "21dac2e9cc7e3cf7da5800814787b833e680b2fd",
     "opts": {},
     "name": "Cli",
     "inputRev?": "nightly",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4",
     "subDir?": null,
-    "rev": "60e74fe402d88eb42d655ec6ff33093683dee2e3",
+    "rev": "b7854e3e43525b9784f97276970f865b8a7314fb",
     "opts": {},
     "name": "mathlib",
     "inputRev?": "joachim/find",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
-    "rev": "81cc13c524a68d0072561dbac276cd61b65872a6",
+    "rev": "e75daed95ad1c92af4e577fea95e234d7a8401c1",
     "opts": {},
     "name": "Qq",
     "inputRev?": "master",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "086c98bb129ca856381d4414dc0afd6e3e4ae2ef",
+    "rev": "1a0cded2be292b5496e659b730d2accc742de098",
     "opts": {},
     "name": "aesop",
     "inputRev?": "master",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "7194b6b9b074e15c490e59491843bcd0f0feda68",
+    "rev": "67855403d60daf181775fa1ec63b04e70bcc3921",
     "opts": {},
     "name": "std",
     "inputRev?": "main",