LeanLsp.Runtime.Local (LeanLsp v0.2.0)

Copy Markdown View Source

Host-backed implementation of LeanLsp.Runtime.

This runtime executes Lean-related commands directly on the host machine. It is useful for local development environments where Lean, Lake, and Elan are already installed and Docker isolation is not required.

Docker remains the default runtime selected by LeanLsp.Runtime.Config; select this runtime explicitly when host execution is desired.

Runtime options

  • :workdir, :workspace_root, or :container_workspace_root - host directory where commands are executed. Defaults to File.cwd!/0.
  • :env - environment variables as a map, keyword/list of pairs, or "KEY=value" strings.
  • :timeout or :exec_timeout - default command timeout in milliseconds.

Examples

{:ok, runtime} =
  LeanLsp.start_runtime(
    runtime: LeanLsp.Runtime.Local,
    workdir: File.cwd!()
  )

{:ok, result} =
  LeanLsp.Runtime.Local.exec(runtime, ["lake", "--version"], timeout: 120_000)

:ok = LeanLsp.Runtime.Local.stop(runtime)

Lake builds can be executed through the same runtime contract:

{:ok, result} =
  LeanLsp.Runtime.Local.exec(runtime, ["lake", "build"], timeout: 120_000)

The runtime captures stdout, stderr, and exit_status. Observed non-zero exits return {:error, {:command_failed, failure}}; launch failures and timeouts return structured errors without requiring callers to parse text.

Summary

Types

runtime()

Runtime process handle for the host-backed runtime.

Functions

child_spec(init_arg)

Returns a child specification suitable for supervisors.

exec(runtime, command, opts)

Executes a command on the host.

start_link(opts)

Starts a host-backed runtime process.

stop(runtime)

Stops the host-backed runtime.

Types

runtime()

@type runtime() ::
  pid()
  | atom()
  | {atom(), node()}
  | {:global, term()}
  | {:via, module(), term()}

Runtime process handle for the host-backed runtime.

Functions

child_spec(init_arg)

@spec child_spec(keyword()) :: Supervisor.child_spec()

Returns a child specification suitable for supervisors.

exec(runtime, command, opts)

@spec exec(LeanLsp.Runtime.t(), LeanLsp.Runtime.command(), LeanLsp.Runtime.options()) ::
  {:ok, LeanLsp.Runtime.exec_result()}
  | {:error, LeanLsp.Runtime.error_reason()}

Executes a command on the host.

The command must be a non-empty list of strings, for example ["lake", "--version"]. Options include :workdir, :env, and :timeout.

start_link(opts)

@spec start_link(LeanLsp.Runtime.options()) :: GenServer.on_start()

Starts a host-backed runtime process.

stop(runtime)

@spec stop(LeanLsp.Runtime.t()) :: :ok | {:error, LeanLsp.Runtime.error_reason()}

Stops the host-backed runtime.

Cleanup is idempotent for a runtime process that has already stopped.