fix for nightly-2024-03-15

ImportGraph/Imports.lean

@@ -236,7 +236,7 @@ def Lean.Name.findHome (n : Name) (env : Option Environment) : CoreM NameSet :=
         candidates := candidates.erase i
   return candidates
 
-open Elab in
+open Elab Command in
 /--
 Find locations as high as possible in the import hierarchy
 where the named declaration could live.
@@ -254,7 +254,7 @@ uses one lemma from each, then `#find_home! lemma` returns the current file.
 elab "#find_home" bang:"!"? n:ident : command => do
   let stx ← getRef
   let mut homes := #[]
-  let n ← resolveGlobalConstNoOverloadWithInfo n
+  let n ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo n
   let env := if bang.isSome then some (← getEnv) else none
   for i in (← Elab.Command.liftCoreM do n.findHome env) do
     homes := homes.push i

lake-manifest.json

@@ -13,10 +13,10 @@
   {"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "2a1b7546b2df0f8e65a70d3b228c30d91752acc4",
+   "rev": "2c55b6bdd2a48362316f6ca24ddb5a2f1e8536a7",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "importGraph",

lakefile.lean

@@ -5,7 +5,7 @@ package «importGraph» where
   -- add package configuration options here
 
 require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"
-require std from git "https://github.com/leanprover/std4" @ "main"
+require std from git "https://github.com/leanprover/std4" @ "nightly-testing"
 
 @[default_target]
 lean_lib «ImportGraph» where

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.6.1
+leanprover/lean4:nightly-2024-03-15