fix: make beam installer and daemon launch portable

Author: ejgallego

Beam/Cli.lean

@@ -7,6 +7,7 @@ Author: Emilio J. Gallego Arias
 import Lean
 import Beam.Broker.Client
 import Beam.Broker.Transport
+import RunAt.Lib.NativeLib
 import RunAt.Protocol
 import Std.Internal.UV.Signal
 
@@ -213,10 +214,25 @@ private def readCmdTrim (cmd : String) (args : Array String := #[]) (cwd? : Opti
     throw <| IO.userError s!"command failed: {cmd} {String.intercalate " " args.toList}\n{out.stderr}"
   pure <| trimLine out.stdout
 
-private def commandAvailable (cmd : String) : IO Bool := do
+private def commandAvailable (cmd : String) (args : Array String := #["--help"]) : IO Bool := do
   try
-    let out ← IO.Process.output { cmd := "sh", args := #["-c", s!"command -v {shellQuote cmd} >/dev/null 2>&1"] }
-    pure (out.exitCode == 0)
+    let child ← IO.Process.spawn {
+      cmd := cmd
+      args := args
+      stdin := .null
+      stdout := .null
+      stderr := .null
+    }
+    if (← child.tryWait).isNone then
+      try
+        child.kill
+      catch _ =>
+        pure ()
+      try
+        discard <| child.wait
+      catch _ =>
+        pure ()
+    pure true
   catch _ =>
     pure false
 
@@ -236,10 +252,10 @@ private def runAtHome : IO System.FilePath := do
 private def defaultBundlePaths (home : System.FilePath) : IO BundlePaths := do
   let installedDaemon := home / "libexec" / "beam-daemon"
   let installedClient := home / "libexec" / "beam-client"
-  let installedPlugin := home / "libexec" / "librunAt_RunAt.so"
+  let installedPlugin := RunAt.Lib.pluginSharedLibPath (home / "libexec")
   let checkoutDaemon := home / ".lake" / "build" / "bin" / "beam-daemon"
   let checkoutClient := home / ".lake" / "build" / "bin" / "beam-client"
-  let checkoutPlugin := home / ".lake" / "build" / "lib" / "librunAt_RunAt.so"
+  let checkoutPlugin := RunAt.Lib.pluginSharedLibPath (home / ".lake" / "build" / "lib")
   let installedReady :=
     (← installedDaemon.pathExists) &&
     (← installedClient.pathExists) &&
@@ -371,7 +387,7 @@ private def bundlePathsFor (workspace : System.FilePath) : BundlePaths :=
   {
     daemon := workspace / ".lake" / "build" / "bin" / "beam-daemon"
     client := workspace / ".lake" / "build" / "bin" / "beam-client"
-    plugin := workspace / ".lake" / "build" / "lib" / "librunAt_RunAt.so"
+    plugin := RunAt.Lib.pluginSharedLibPath (workspace / ".lake" / "build" / "lib")
   }
 
 private def bundleArtifactsReady (workspace : System.FilePath) : IO Bool := do
@@ -407,7 +423,7 @@ private def bundleSourceHashInputLabels : List String :=
 
 private def installRuntimePaths : List String :=
   ["libexec/beam-cli", "libexec/beam-daemon", "libexec/beam-client",
-    "libexec/librunAt_RunAt.so", ".lake/packages"]
+    s!"libexec/{RunAt.Lib.pluginSharedLibName}", ".lake/packages"]
 
 private def installWrapperPaths : List String :=
   ["bin/lean-beam", "bin/lean-beam-search"]
@@ -543,11 +559,18 @@ private def fallbackBuildFailureMessage (toolchain : String) (cacheRoot bundleDi
     stderr
   ]
 
+private def killCommand : IO String := do
+  let candidates := [System.FilePath.mk "/bin/kill", System.FilePath.mk "/usr/bin/kill"]
+  for candidate in candidates do
+    if ← candidate.pathExists then
+      return candidate.toString
+  if ← commandAvailable "kill" #["-l"] then
+    pure "kill"
+  else
+    throw <| IO.userError "could not find kill command"
+
 private def pidAlive (pid : Nat) : IO Bool := do
-  let out ← IO.Process.output {
-    cmd := "sh"
-    args := #["-c", s!"kill -0 {pid} >/dev/null 2>&1"]
-  }
+  let out ← IO.Process.output { cmd := (← killCommand), args := #["-0", toString pid] }
   pure (out.exitCode == 0)
 
 private partial def acquireLock (lockDir : System.FilePath) : IO Unit := do
@@ -718,19 +741,17 @@ private def leanBin (root : System.FilePath) : IO String := do
 private def rocqCandidates (root : System.FilePath) : List System.FilePath :=
   [root / "_opam" / "bin" / "coq-lsp", root / "_opam" / "_opam" / "bin" / "coq-lsp"]
 
-private def pathCmd? (cmd : String) : IO (Option String) := do
-  try
-    return some (← readCmdTrim "sh" #["-c", s!"command -v {shellQuote cmd}"])
-  catch _ =>
-    return none
-
 private def maybeRocqCmd (root : System.FilePath) : IO (Option String) := do
   for candidate in rocqCandidates root do
     if ← candidate.pathExists then
       return some candidate.toString
   match ← IO.getEnv "BEAM_ROCQ_CMD" with
   | some cmd => pure (some cmd)
-  | none => pathCmd? "coq-lsp"
+  | none =>
+      if ← commandAvailable "coq-lsp" then
+        pure (some "coq-lsp")
+      else
+        pure none
 
 private def rocqCmd (root : System.FilePath) : IO String := do
   match ← maybeRocqCmd root with
@@ -804,11 +825,11 @@ private def daemonResponds (endpoint : Transport.Endpoint) : IO Bool := do
     pure false
 
 private def killPid (pid : Nat) : IO Unit := do
-  let _ ← IO.Process.output {
-    cmd := "sh"
-    args := #["-c", s!"kill {pid} >/dev/null 2>&1 || true"]
-  }
-  pure ()
+  try
+    let _ ← IO.Process.output { cmd := (← killCommand), args := #[toString pid] }
+    pure ()
+  catch _ =>
+    pure ()
 
 private partial def waitForPidGone (pid : Nat) (tries : Nat := 20) : IO Unit := do
   if tries == 0 then
@@ -918,16 +939,16 @@ private def startDaemon (desired : DesiredConfig) (endpoint : Transport.Endpoint
     IO.FS.createDirAll parent
   IO.FS.writeFile logPath ""
   let cmd := String.intercalate " " ((desired.daemonBin.toString :: args).map shellQuote)
-  let shell := s!"cd {shellQuote desired.root.toString} && {cmd} >{shellQuote logPath.toString} 2>&1 < /dev/null & echo $!"
-  let out ← IO.Process.output {
+  let shell := s!"exec {cmd} >{shellQuote logPath.toString} 2>&1 < /dev/null"
+  let child ← IO.Process.spawn {
     cmd := "sh"
     args := #["-c", shell]
+    cwd := some desired.root
+    stdin := .null
+    stdout := .null
+    stderr := .null
   }
-  if out.exitCode != 0 then
-    throw <| IO.userError s!"failed to start Beam daemon for {desired.root}\n{out.stderr}"
-  let pidText := trimLine out.stdout
-  let some pid := pidText.toNat?
-    | throw <| IO.userError s!"failed to capture Beam daemon pid for {desired.root}"
+  let pid := child.pid.toNat
   pure pid
 
 private partial def waitForDaemon (pid : Nat) (endpoint : Transport.Endpoint) (logPath : System.FilePath)

RunAt/Lib/NativeLib.lean

@@ -0,0 +1,11 @@
+import Lake.Util.NativeLib
+
+namespace RunAt.Lib
+
+def pluginSharedLibName : String :=
+  Lake.nameToSharedLib "runAt_RunAt"
+
+def pluginSharedLibPath (dir : System.FilePath) : System.FilePath :=
+  dir / pluginSharedLibName
+
+end RunAt.Lib

scripts/install-beam.sh

@@ -7,6 +7,7 @@
 set -euo pipefail
 
 repo_root="$(cd "$(dirname "$0")/.." && pwd)"
+. "$repo_root/scripts/shared-lib.sh"
 codex_skills_home="${CODEX_HOME:-$HOME/.codex}/skills"
 claude_skills_home="${CLAUDE_HOME:-$HOME/.claude}/skills"
 bin_home="${HOME}/.local/bin"
@@ -29,6 +30,7 @@ style_green=""
 style_blue=""
 style_yellow=""
 style_dim=""
+runat_plugin_shared_lib="$(beam_shared_lib_name runAt_RunAt)"
 
 runtime_payload_spec=(
   "copy|rootFiles|RunAt.lean|RunAt.lean"
@@ -44,7 +46,7 @@ runtime_payload_spec=(
   "copy|runtimePaths|.lake/build/bin/beam-cli|libexec/beam-cli"
   "copy|runtimePaths|.lake/build/bin/beam-daemon|libexec/beam-daemon"
   "copy|runtimePaths|.lake/build/bin/beam-client|libexec/beam-client"
-  "copy|runtimePaths|.lake/build/lib/librunAt_RunAt.so|libexec/librunAt_RunAt.so"
+  "copy|runtimePaths|.lake/build/lib/$runat_plugin_shared_lib|libexec/$runat_plugin_shared_lib"
   "copy|runtimePaths|.lake/packages|.lake/packages"
   "copy|wrapperPaths|scripts/lean-beam|bin/lean-beam"
   "copy|wrapperPaths|scripts/lean-beam-search|bin/lean-beam-search"
@@ -219,7 +221,8 @@ replace_symlink_atomically() {
   require_path_within "$tmp_dir" "$link_dir" "$label temp dir"
   tmp_link="$tmp_dir/link"
   ln -s "$target" "$tmp_link"
-  mv -Tf "$tmp_link" "$link_path"
+  rm -f -- "$link_path"
+  mv "$tmp_link" "$link_path"
   rmdir "$tmp_dir"
 }
 
@@ -365,7 +368,7 @@ ensure_runtime_artifacts() {
   if [ -x "$beam_cli" ] \
     && [ -x "$repo_root/.lake/build/bin/beam-daemon" ] \
     && [ -x "$repo_root/.lake/build/bin/beam-client" ] \
-    && [ -f "$repo_root/.lake/build/lib/librunAt_RunAt.so" ]; then
+    && [ -f "$repo_root/.lake/build/lib/$runat_plugin_shared_lib" ]; then
     return 0
   fi
   echo "building beam runtime artifacts" >&2

scripts/shared-lib.sh

@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+
+# Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+# Released under Apache 2.0 license as described in the file LICENSE.
+# Author: Emilio J. Gallego Arias
+
+beam_shared_lib_ext() {
+  case "$(uname -s)" in
+    Darwin)
+      printf 'dylib\n'
+      ;;
+    CYGWIN*|MINGW*|MSYS*|Windows_NT)
+      printf 'dll\n'
+      ;;
+    *)
+      printf 'so\n'
+      ;;
+  esac
+}
+
+beam_shared_lib_name() {
+  local base="$1"
+  local ext
+  ext="$(beam_shared_lib_ext)"
+  case "$(uname -s)" in
+    CYGWIN*|MINGW*|MSYS*|Windows_NT)
+      printf '%s.%s\n' "$base" "$ext"
+      ;;
+    *)
+      printf 'lib%s.%s\n' "$base" "$ext"
+      ;;
+  esac
+}

tests/test-beam-wrapper.sh

@@ -74,6 +74,15 @@ else:
 PY
 }
 
+sed_in_place_portable() {
+  local expr="$1"
+  local path="$2"
+  local tmp
+  tmp="$(mktemp "${path}.sed-XXXXXX")"
+  sed "$expr" "$path" >"$tmp"
+  mv "$tmp" "$path"
+}
+
 read_json_array_len() {
   python3 - "$1" <<'PY'
 import json, os, sys
@@ -834,7 +843,7 @@ EOF
     exit 1
   fi
 
-  sed -i 's/1/2/' SaveSmoke/B.lean
+  sed_in_place_portable 's/1/2/' SaveSmoke/B.lean
   sync_out="$("$beam_script" lean-sync SaveSmoke/B.lean)"
   if [ "$(RUNAT_JSON_PAYLOAD="$sync_out" read_json_text_field ok)" != "true" ]; then
     echo "expected lean-sync after first edit to succeed" >&2
@@ -923,7 +932,7 @@ EOF
     exit 1
   fi
 
-  sed -i 's/2/3/' SaveSmoke/B.lean
+  sed_in_place_portable 's/2/3/' SaveSmoke/B.lean
   open_files_dirty="$("$beam_script" open-files)"
   if [ "$(RUNAT_JSON_PAYLOAD="$open_files_dirty" read_json_text_field result.sessions.lean.files.0.status)" != "notSaved" ]; then
     echo "expected open-files to detect an on-disk edit for an already known file incrementally" >&2
@@ -1722,7 +1731,7 @@ sleep 1
     printf '%s\n' "$doctor_out" >&2
     exit 1
   fi
-  sed -i 's/1/2/' SaveSmoke/B.lean
+  sed_in_place_portable 's/1/2/' SaveSmoke/B.lean
   sync_out="$("$beam_script" --port "$busy_port" lean-sync SaveSmoke/B.lean)"
   if [ "$(RUNAT_JSON_PAYLOAD="$sync_out" read_json_text_field ok)" != "true" ]; then
     echo "expected lean-sync with a busy requested port to reuse the live Beam daemon" >&2

tests/test-install.sh

@@ -7,6 +7,7 @@
 set -euo pipefail
 
 cd "$(dirname "$0")/.."
+. scripts/shared-lib.sh
 
 tmp_root="$(mktemp -d /tmp/runat-install-XXXXXX)"
 
@@ -61,6 +62,7 @@ mkdir -p "$HOME" "$BEAM_INSTALL_ROOT"
 mapfile -t supported_toolchains < <(grep -v '^[[:space:]]*#' supported-lean-toolchains | sed '/^[[:space:]]*$/d')
 toolchain="${supported_toolchains[0]}"
 source_checkout="$tmp_root/source-checkout"
+runat_plugin_shared_lib="$(beam_shared_lib_name runAt_RunAt)"
 
 assert_file() {
   local path="$1"
@@ -80,7 +82,7 @@ assert_not_exists() {
 
 assert_no_skill_socket_guidance() {
   local skill_doc="$1"
-  if rg -n -- '--socket|Unix domain socket|unix domain socket' "$skill_doc" > /dev/null; then
+  if grep -E -- '--socket|Unix domain socket|unix domain socket' "$skill_doc" > /dev/null; then
     echo "unexpected socket guidance in installed skill: $skill_doc" >&2
     exit 1
   fi
@@ -109,7 +111,7 @@ assert_runtime_layout() {
   assert_file "$runtime_root/libexec/beam-cli"
   assert_file "$runtime_root/libexec/beam-daemon"
   assert_file "$runtime_root/libexec/beam-client"
-  assert_file "$runtime_root/libexec/librunAt_RunAt.so"
+  assert_file "$runtime_root/libexec/$runat_plugin_shared_lib"
   assert_not_exists "$runtime_root/.lake/build"
   assert_file "$runtime_root/bin/lean-beam"
   assert_file "$runtime_root/bin/lean-beam-search"
@@ -222,12 +224,7 @@ assert_bundle_layout() {
   for expected_toolchain in "$@"; do
     found=""
     for metadata in "${metadata_files[@]}"; do
-      if command -v rg >/dev/null 2>&1; then
-        if rg -n --fixed-strings "\"toolchain\": \"$expected_toolchain\"" "$metadata" > /dev/null; then
-          found="$metadata"
-          break
-        fi
-      elif grep -F "\"toolchain\": \"$expected_toolchain\"" "$metadata" > /dev/null; then
+      if grep -F "\"toolchain\": \"$expected_toolchain\"" "$metadata" > /dev/null; then
         found="$metadata"
         break
       fi
@@ -245,7 +242,7 @@ assert_bundle_layout() {
     assert_file "$workspace/RunAt/Internal/DirectImports.lean"
     assert_file "$workspace/.lake/build/bin/beam-daemon"
     assert_file "$workspace/.lake/build/bin/beam-client"
-    assert_file "$workspace/.lake/build/lib/librunAt_RunAt.so"
+    assert_file "$workspace/.lake/build/lib/$runat_plugin_shared_lib"
   done
 }