chore: bump toolchain to v4.30.0-rc1

REPL/Lean/Environment.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 import REPL.Util.Pickle
-import Lean.Replay
+import REPL.Lean.Replay
 
 open System (FilePath)
 
@@ -30,7 +30,8 @@ and then replace the new constants.
 -/
 def unpickle (path : FilePath) : IO (Environment × CompactedRegion) := unsafe do
   let ((imports, map₂), region) ← _root_.unpickle (Array Import × PHashMap Name ConstantInfo) path
+  enableInitializersExecution
   let env ← importModules imports {} 0 (loadExts := true)
-  return (← env.replay (Std.HashMap.ofList map₂.toList), region)
+  return (replayToElabEnv env (Std.HashMap.ofList map₂.toList), region)
 
 end Lean.Environment

REPL/Lean/Replay.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+import Lean.Environment
+
+/-!
+# Replay constants into an elaboration environment
+
+In Lean v4.30+, `Environment.replay` returns an environment via `ofKernelEnv` whose
+constants live in `Kernel.Environment.constants.map₂`. However, `Environment.find?`
+only checks `constants.map₁` and `asyncConstsMap`, so replayed constants are invisible
+to elaboration. (LeanChecker confirms this: in v4.30 it discards the env after replay
+— `replay` is purely a verification tool now.)
+
+This module provides `replayToElabEnv`, which uses the FFI export `lake_environment_add`
+that Lake declares in `src/lake/Lake/Load/Lean/Elab.lean` (the export of the private
+`Lean.Environment.lakeAdd`). That helper inserts a `ConstantInfo` into both the kernel
+environment's constant map *and* `asyncConstsMap`, which is what `Environment.find?`
+needs.
+
+## Trust model
+
+`replayToElabEnv` bypasses kernel type-checking. The REPL produces and consumes its own
+pickles, so the constants being replayed have already been checked by the kernel once.
+**Pickles are trusted artifacts; this is not a verifier boundary.** A malicious or
+corrupt `.olean` could install unchecked constants directly into the environment.
+
+## Caveats
+
+* This only restores constants — *not* environment extension entries (which Lake's
+  `importConfigFileCore` partially handles via `IR.declMapExt`). This matches the
+  existing REPL limitation around scoped extensions.
+* `lake_environment_add` is a private Lean export ("only needed for the lakefile.lean
+  cache", per the comment in `Lean.Environment`). It is not a stable public API. If
+  this file stops compiling against a future Lean release, search lean4 for
+  `lake_environment_add` and adapt. The REPL is unlikely to get a supported public API
+  for this since it is on a deprecation path.
+-/
+
+namespace Lean.Environment
+
+-- `compiler.ignoreBorrowAnnotation` matches the C ABI of the exported `lake_environment_add`
+-- symbol; Lake uses the same option for the same wrapper.
+set_option compiler.ignoreBorrowAnnotation true in
+/--
+Insert an already-kernel-checked `ConstantInfo` directly into an `Environment`,
+populating both the kernel constant map and `asyncConstsMap`. **No type checking.**
+This is the FFI symbol Lake uses in `importConfigFileCore`.
+-/
+@[extern "lake_environment_add"]
+private opaque addAlreadyCheckedConstantInfo
+    (env : Environment) (_ : ConstantInfo) : Environment
+
+/--
+Add new constants to an elaboration `Environment`, ensuring they are visible to
+`Environment.find?`.
+
+This replaces `Environment.replay` for use cases where the resulting environment
+needs to be used for elaboration (not just verification). It does not perform kernel
+checking; see the trust model in the module docstring.
+-/
+def replayToElabEnv (env : Environment)
+    (newConstants : Std.HashMap Name ConstantInfo) : Environment :=
+  newConstants.fold (init := env) fun env _ ci =>
+    if ci.isUnsafe || ci.isPartial then env else addAlreadyCheckedConstantInfo env ci
+
+end Lean.Environment

REPL/Snapshots.lean

@@ -3,9 +3,9 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Lean.Replay
 import Lean.Elab.Command
 import REPL.Util.Pickle
+import REPL.Lean.Replay
 
 open Lean Elab
 
@@ -83,7 +83,9 @@ def unpickle (path : FilePath) : IO (CommandSnapshot × CompactedRegion) := unsa
   let ((imports, map₂, cmdState, cmdContext), region) ←
     _root_.unpickle (Array Import × PHashMap Name ConstantInfo × CompactableCommandSnapshot ×
       Command.Context) path
-  let env ← (← importModules imports {} 0 (loadExts := true)).replay (Std.HashMap.ofList map₂.toList)
+  enableInitializersExecution
+  let env ← importModules imports {} 0 (loadExts := true)
+  let env := Lean.Environment.replayToElabEnv env (Std.HashMap.ofList map₂.toList)
   let p' : CommandSnapshot :=
   { cmdState := { cmdState with env }
     cmdContext }
@@ -291,9 +293,10 @@ def unpickle (path : FilePath) (cmd? : Option CommandSnapshot) :
   let env ← match cmd? with
   | none =>
     enableInitializersExecution
-    (← importModules imports {} 0 (loadExts := true)).replay (Std.HashMap.ofList map₂.toList)
+    let env ← importModules imports {} 0 (loadExts := true)
+    pure <| Lean.Environment.replayToElabEnv env (Std.HashMap.ofList map₂.toList)
   | some cmd =>
-    cmd.cmdState.env.replay (Std.HashMap.ofList map₂.toList)
+    pure <| Lean.Environment.replayToElabEnv cmd.cmdState.env (Std.HashMap.ofList map₂.toList)
   let p' : ProofSnapshot :=
   { coreState := { coreState with env }
     coreContext

lake-manifest.json

@@ -1,5 +1,6 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages": [],
  "name": "REPL",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.29.0
+leanprover/lean4:v4.30.0-rc1

test/Mathlib/lake-manifest.json

@@ -1,21 +1,21 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8a178386ffc0f5fef0b77738bb5449d50efeea95",
+   "rev": "0c154d67103f74be3a0f2c509f72ccbf5be9f2a7",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0",
+   "inputRev": "v4.30.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3",
+   "rev": "f449eabb8f7e3feef0366856c20e28a6d2c97ee3",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "48d5698bc464786347c1b0d859b18f938420f060",
+   "rev": "86503d416c875fdcf3b6b6c54c22581e96c6bda7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,51 +45,52 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3",
+   "rev": "82d457fb3bdd9efadbae06608ff337d689efdddf",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.95",
+   "inputRev": "v0.0.97",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7152850e7b216a0d409701617721b6e469d34bf6",
+   "rev": "f74c7555aaa94eadd7b7bff9170f7983f92aac21",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d",
+   "rev": "7aa86cb20b8458748dc24d55dab2d7ea01161057",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "756e3321fd3b02a85ffda19fef789916223e578c",
+   "rev": "bf597c77bf9b8e66720d724928207f5911533113",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.30.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29",
+   "rev": "f7d0ca7c926cdde0562af20394dd25d028b839a5",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0",
+   "inputRev": "v4.30.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "«repl-mathlib-tests»",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

test/Mathlib/lakefile.toml

@@ -4,7 +4,7 @@ defaultTargets = ["ReplMathlibTests"]
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "v4.29.0"
+rev = "v4.30.0-rc1"
 
 [[lean_lib]]
 name = "ReplMathlibTests"

test/Mathlib/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.29.0
+leanprover/lean4:v4.30.0-rc1