Merge pull request #4 from leanprover-community/bump/v4.8.0

chore: move to v4.8.0-rc1

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,8 +254,8 @@ 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 env := if bang.isSome then some (← getEnv) else none
+  let n ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo n
+  let env ← if bang.isSome then some <$> getEnv else pure none
   for i in (← Elab.Command.liftCoreM do n.findHome env) do
     homes := homes.push i
   logInfoAt stx[0] m!"{homes}"

ImportGraph/Lean/Name.lean

@@ -64,6 +64,6 @@ returns `ImportGraph`.
 -/
 def getModule (name : Name) (s := "") : Name :=
   match name with
-    | .anonymous => s
+    | .anonymous => .mkSimple s
     | .num _ _ => panic s!"panic in `getModule`: did not expect numerical name: {name}."
     | .str pre s => getModule pre s

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
+   "rev": "3025cb124492b423070f20cf0a70636f757d117f",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.8.0-rc1