feat: support bundled Lean toolchain runtimes

.github/workflows/ci.yml

@@ -84,6 +84,12 @@ jobs:
         if: ${{ !cancelled() && steps.lean_setup.outcome == 'success' }}
         run: bash tests/test-beam-toolchain-compat.sh "$(head -n 1 lean-toolchain)"
 
+      - name: Native Toolchain Installation and Relocation Test
+        if: ${{ !cancelled() && steps.lean_setup.outcome == 'success' }}
+        run: |
+          lean_prefix="$(lean --print-prefix)"
+          python3 tests/test-native-toolchain.py "$lean_prefix" --crlf
+
       - name: Beam Install Test
         if: ${{ !cancelled() && steps.lean_setup.outcome == 'success' }}
         run: bash tests/test-beam-install.sh
@@ -109,6 +115,80 @@ jobs:
         if: ${{ !cancelled() && steps.lean_setup.outcome == 'success' && steps.rocq_deps.outcome == 'success' }}
         run: bash tests/test-beam-rocq.sh
 
+  native-toolchain:
+    name: native-toolchain (${{ matrix.os }})
+    runs-on: ${{ matrix.os }}
+    strategy:
+      fail-fast: false
+      matrix:
+        os: ${{ fromJSON(vars.BEAM_FULL_MACOS_CI == 'true' && '["ubuntu-latest","ubuntu-24.04-arm","macos-15-intel","macos-latest","windows-latest"]' || '["ubuntu-latest","ubuntu-24.04-arm","windows-latest"]') }}
+    steps:
+      - uses: actions/checkout@v6
+
+      - uses: actions/setup-python@v6
+        with:
+          python-version: '3.12'
+
+      - name: Install Linux dependencies
+        if: runner.os == 'Linux'
+        run: sudo apt-get update && sudo apt-get install -y clang lld
+
+      - name: Install elan
+        if: runner.os != 'Windows'
+        shell: bash
+        run: |
+          curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: Install Windows elan
+        if: runner.os == 'Windows'
+        shell: pwsh
+        run: |
+          Invoke-WebRequest https://github.com/leanprover/elan/releases/latest/download/elan-x86_64-pc-windows-msvc.zip -OutFile "$env:RUNNER_TEMP/elan.zip"
+          Expand-Archive "$env:RUNNER_TEMP/elan.zip" "$env:RUNNER_TEMP/elan"
+          & "$env:RUNNER_TEMP/elan/elan-init.exe" -y --default-toolchain none
+          "$env:USERPROFILE/.elan/bin" >> $env:GITHUB_PATH
+
+      - uses: msys2/setup-msys2@v2
+        id: native-msys2
+        if: runner.os == 'Windows'
+        with:
+          msystem: CLANG64
+          update: true
+          install: mingw-w64-clang-x86_64-clang mingw-w64-clang-x86_64-lld mingw-w64-clang-x86_64-gmp mingw-w64-clang-x86_64-libuv
+
+      - name: Select Windows compiler
+        if: runner.os == 'Windows'
+        shell: pwsh
+        env:
+          MSYS2_LOCATION: ${{ steps.native-msys2.outputs.msys2-location }}
+        run: '"$env:MSYS2_LOCATION/clang64/bin" >> $env:GITHUB_PATH'
+
+      - name: Build, relocate, and exercise native toolchain
+        shell: bash
+        run: |
+          lean --version
+          lean_prefix="$(python -c 'from pathlib import Path; import subprocess; print(Path(subprocess.check_output(["elan", "which", "lean"], text=True).strip()).parent.parent)')"
+          if [ "${{ matrix.os }}" = "ubuntu-latest" ]; then
+            elan toolchain install leanprover/lean4:v4.33.1
+            previous_prefix="$(elan run leanprover/lean4:v4.33.1 lean --print-prefix)"
+            python tests/test-native-toolchain.py "$lean_prefix" --crlf --previous-lean-prefix "$previous_prefix"
+          else
+            python tests/test-native-toolchain.py "$lean_prefix" --crlf
+          fi
+
+      - name: Retain native runtime diagnostics
+        if: failure()
+        uses: actions/upload-artifact@v6
+        with:
+          name: native-runtime-diagnostics-${{ matrix.os }}
+          include-hidden-files: true
+          path: |
+            .native-test/**/owner.log
+            .native-test/**/postponed-owner.log
+            .native-test/**/.beam/*.log
+            .native-test/**/.beam/*.json
+
   shell-lint:
     name: shell-lint (${{ matrix.os }})
     runs-on: ${{ matrix.os }}

.gitignore

@@ -6,6 +6,7 @@
 /.codex
 /.codex-worktrees/
 /.tmp/
+/.native-test/
 .beam/
 __pycache__/
 *.pyc

Beam/Cli/Commands.lean

@@ -255,12 +255,25 @@ private def sessionStatus (opts : CliOptions) : IO Unit := do
   printResponse <| Response.success (toJson result)
 
 def runCommand (home : System.FilePath) (opts : CliOptions) : IO Unit := do
+  if Toolchain.enabled && opts.args.head?.any (["install-layout", "install-manifest",
+      "install-manifest-with-source-commit", "install-runtime-validate"].contains ·) then
+    throw <| IO.userError
+      "bundled lean-beam does not provide standalone install or MCP setup commands; use its containing Lean toolchain's installer"
   match opts.args with
   | [] | ["-h"] | ["--help"] | ["help"] =>
-      IO.println usage
+      IO.println (usage Toolchain.enabled)
   | "version" :: [] | "--version" :: [] =>
       printVersion home
+  | "toolchain-build-info" :: [] =>
+      unless Toolchain.enabled do
+        throw <| IO.userError "this executable was not built with -KbeamToolchain=true"
+      printJsonLine <| Json.mkObj [
+        ("leanGithash", toJson Lean.githash),
+        ("lakeSupportsDeferredCompilation", toJson Toolchain.lakeSupportsDeferredCompilation)
+      ]
   | "bundle-install" :: toolchain :: [] =>
+      if Toolchain.enabled then
+        throw <| IO.userError "bundled lean-beam uses only its containing toolchain; reinstall that toolchain to repair its runtime"
       let cacheRoot ←
         match ← IO.getEnv "BEAM_INSTALL_BUNDLE_DIR" with
         | some path => pure <| System.FilePath.mk path
@@ -270,6 +283,8 @@ def runCommand (home : System.FilePath) (opts : CliOptions) : IO Unit := do
       let _ ← ensureToolchainBundleIn cacheRoot home toolchain
       pure ()
   | "prune" :: args =>
+      if Toolchain.enabled then
+        throw <| IO.userError "bundled lean-beam has no standalone runtimes to prune"
       runInstallPrune home args
   | "validated-toolchains" :: [] =>
       printValidatedToolchains home "lean"
@@ -486,6 +501,6 @@ def runCommand (home : System.FilePath) (opts : CliOptions) : IO Unit := do
   | "recover" :: args =>
       recoverProjectSession opts args
   | _ =>
-      throw <| IO.userError usage
+      throw <| IO.userError (usage Toolchain.enabled)
 
 end Beam.Cli

Beam/Cli/DaemonManager.lean

@@ -181,6 +181,15 @@ private def writePrivateFileAtomically
 private def openPrivateFileAtomically
     (dir : System.FilePath)
     (leaf stem : String) : IO IO.FS.Handle := do
+  if System.Platform.isWindows then
+    -- CRT handles cannot be renamed while open. Owner admission holds the control lock and the
+    -- parent has a private DACL; replace the old log, then create its new inode exclusively.
+    -- Retain that exact handle so later writes never reopen or follow a replaced path.
+    let path := dir / leaf
+    if ← path.pathExists then IO.FS.removeFile path
+    let handle ← IO.FS.Handle.mk path .writeNew
+    IO.setAccessRights path { user := { read := true, write := true } }
+    return handle
   let (tmp, handle) ← createPrivateTempFile dir stem
   try
     IO.FS.rename tmp (dir / leaf)
@@ -677,11 +686,11 @@ private def startDaemonEntry
       match ← waitForDaemonReady started identity with
       | .ok endpoint =>
           if (← started.child.tryWait).isSome then
-            pure <| .error "Beam daemon exited immediately after reporting readiness"
+            pure <| Except.error "Beam daemon exited immediately after reporting readiness"
           else
             let entry ← registryEntryFor desired identity capability started.child.pid.toNat endpoint
-            pure (.ok entry)
-      | .error detail => pure (.error detail)
+            pure (Except.ok entry)
+      | .error detail => pure (Except.error detail)
     catch err =>
       terminateStartedDaemon started
       throw err
@@ -1250,6 +1259,11 @@ private def lookupProjectDaemon
   match ← selectProjectControl root control with
   | .selected entry =>
       IO.ofExcept <| validateWorkspaceBackend root entry backend?
+      if Toolchain.enabled && entry.workspace.leanCmd?.isSome then
+        let desired ← desiredConfig (← Toolchain.home) root .lean
+        unless entry.configHash == desired.configHash do
+          throw <| IO.userError <|
+            configMismatchMessage root control.dir entry desired.configHash .lean
       pure <| .ofSessionDescriptor entry control.dir
   | .absent =>
       throw <| IO.userError (missingOwnerMessage root control.dir backend?)

Beam/Cli/Info.lean

@@ -21,6 +21,13 @@ namespace Beam.Cli
 open Beam.Broker
 
 def printVersion (home : System.FilePath) : IO Unit := do
+  if Toolchain.enabled then
+    let p ← Toolchain.provenance
+    IO.println s!"lean-beam {Beam.Version.projectVersion}"
+    IO.println s!"source commit: {p.sourceCommit}"
+    IO.println s!"runtime payload: {p.payloadHash}"
+    IO.println s!"bundled Lean: {p.leanVersion}"
+    return
   let appPath ← IO.appPath
   let wrapper? ← IO.getEnv "BEAM_WRAPPER_PATH"
   let publicCommand? ← IO.getEnv "BEAM_PUBLIC_COMMAND"
@@ -89,6 +96,22 @@ private def acceptedLeanBundleDoctorInfo
   }
 
 private def printLeanDoctorInfo (home root : System.FilePath) : IO Unit := do
+  if Toolchain.enabled then
+    let lean ← Toolchain.projectLean root
+    let p ← Toolchain.provenance
+    let (paths, id) ← ensureToolchainBundle root home p.leanVersion
+    IO.println "public command: lean-beam"
+    IO.println s!"source commit: {p.sourceCommit}"
+    IO.println s!"runtime payload: {p.payloadHash}"
+    IO.println s!"bundled Lean: {p.leanVersion}"
+    IO.println s!"bundled Lake: {p.lakeVersion}"
+    IO.println s!"lean binary: {lean}"
+    IO.println "bundle source: toolchain"
+    IO.println s!"bundle id: {id}"
+    IO.println "bundle ready: true"
+    IO.println s!"bundle daemon: {paths.daemon}"
+    IO.println s!"plugin: {paths.plugin}"
+    return
   let toolchain ← leanToolchain root
   let support ← leanToolchainSupport home toolchain
   let toolchainValidated := support.acceptance == .validated
@@ -189,6 +212,9 @@ def doctor (home : System.FilePath) (opts : CliOptions) (backend : Backend) : IO
   printDaemonFailureIncidentDoctorInfo root opts.explicitControlDir?
 
 def printValidatedToolchains (home : System.FilePath) (backendName : String) : IO Unit := do
+  if Toolchain.enabled then
+    throw <| IO.userError
+      "bundled lean-beam has no standalone toolchain registry; use version or doctor for its bundled Lean identity"
   match backendName with
   | "lean" =>
       let (_, toolchains) ← validatedLeanToolchains home
@@ -198,6 +224,8 @@ def printValidatedToolchains (home : System.FilePath) (backendName : String) : I
       throw <| IO.userError "usage: lean-beam validated-toolchains"
 
 def printCompatibleReleaseLines (home : System.FilePath) : IO Unit := do
+  if Toolchain.enabled then
+    throw <| IO.userError "bundled lean-beam supports its containing Lean installation only"
   let (_, lines) ← compatibleLeanReleaseLines home
   for line in lines do
     IO.println line.registryEntry

Beam/Cli/Project.lean

@@ -7,6 +7,7 @@ Author: Emilio J. Gallego Arias
 import Lean
 import Beam.Broker.Protocol
 import Beam.Cli.Args
+import Beam.Cli.Toolchain
 import Beam.Cli.RuntimeBundle
 import Beam.Lean.Workspace
 import Beam.Path
@@ -25,6 +26,8 @@ partial def climbParents (path : System.FilePath) (count : Nat) : System.FilePat
   | n + 1 => climbParents (path.parent.getD path) n
 
 def beamHome : IO System.FilePath := do
+  if Toolchain.enabled then
+    return ← Toolchain.home
   match ← IO.getEnv "BEAM_HOME" with
   | some root =>
       Beam.resolveExistingPath <| System.FilePath.mk root
@@ -100,12 +103,17 @@ def explicitProjectRoot (opts : CliOptions) (action : String) : IO System.FilePa
       throw <| IO.userError s!"{action} requires an explicit --root PATH"
 
 def leanToolchain (root : System.FilePath) : IO String := do
+  if Toolchain.enabled then
+    discard <| Toolchain.projectLean root
+    return ← Toolchain.version
   let path := root / "lean-toolchain"
   unless ← path.pathExists do
     throw <| IO.userError s!"missing lean-toolchain in {root}"
   pure <| Beam.trimLine (← IO.FS.readFile path)
 
-def leanBin (root : System.FilePath) : IO String :=
+def leanBin (root : System.FilePath) : IO String := do
+  if Toolchain.enabled then
+    return (← Toolchain.projectLean root).toString
   Beam.readCmdTrim "elan" #["which", "lean"] (some root)
 
 def rocqCandidates (root : System.FilePath) : List System.FilePath :=

Beam/Cli/RuntimeBundle/Build.lean

@@ -260,12 +260,19 @@ def ensureToolchainBundleInForFingerprint (cacheRoot home : System.FilePath) (to
 
 def ensureToolchainBundleIn (cacheRoot home : System.FilePath) (toolchain : String) :
     IO (LeanBundlePaths × String) := do
+  if Toolchain.enabled then
+    let paths : LeanBundlePaths := { daemon := ← Toolchain.daemon, plugin := ← Toolchain.plugin }
+    ensureLeanBundleExists paths
+    return (paths, ← Toolchain.runtimeId)
   ensureAcceptedLeanToolchain home toolchain
   let fingerprint ← toolchainFingerprint toolchain
   ensureToolchainBundleInForFingerprint cacheRoot home toolchain fingerprint
 
 def ensureToolchainBundle (root home : System.FilePath) (toolchain : String) :
     IO (LeanBundlePaths × String) := do
+  if Toolchain.enabled then
+    discard <| Toolchain.projectLean root
+    return ← ensureToolchainBundleIn home home toolchain
   ensureAcceptedLeanToolchain home toolchain
   let fingerprint ← toolchainFingerprint toolchain
   match ← existingToolchainBundleInAnyForFingerprint? (← installBundleCacheRoots) home toolchain fingerprint with
@@ -275,6 +282,10 @@ def ensureToolchainBundle (root home : System.FilePath) (toolchain : String) :
       ensureToolchainBundleInForFingerprint cacheRoot home toolchain fingerprint
 
 def ensureDefaultDaemon (home : System.FilePath) : IO System.FilePath := do
+  if Toolchain.enabled then
+    let daemon ← Toolchain.daemon
+    ensurePathExists "bundled Beam daemon (reinstall this toolchain)" daemon
+    return daemon
   let daemon ← defaultDaemonPath home
   if ← daemon.pathExists then
     pure daemon

Beam/Cli/RuntimeBundle/Paths.lean

@@ -5,6 +5,7 @@ Author: Emilio J. Gallego Arias
 -/
 
 import Lean
+import Beam.Cli.Toolchain
 import Beam.LSP.Lib.NativeLib
 import Beam.System