LeanLsp.Runtime.Docker (LeanLsp v0.1.0)

Copy Markdown View Source

Docker-backed implementation of LeanLsp.Runtime.

This runtime owns the Docker-specific side effects for the v0.1.0 preview. On startup it checks that Docker is available, starts a long-lived container from a configurable image, and keeps the container identifier in GenServer state. exec/3 runs commands inside that container with docker exec. stop/1 and process termination attempt to stop the backing container.

The module is intended for runtime-boundary experimentation, not as a complete Lean LSP client. It can run Lean-related commands inside Docker, but it does not manage JSON-RPC framing, Lean document lifecycle, diagnostics, hover, completion, or go-to-definition requests.

External requirements

  • Docker must be installed and reachable by the BEAM process.
  • The current user must have permission to run Docker containers.
  • The selected image must be pullable or already available locally.
  • Host paths used in mounts must be accessible to Docker.

Default image policy

The default image is leanprovercommunity/lean4:latest. The v0.1.0 preview uses latest as a convenience default so callers can experiment without choosing an image first. It is not a reproducibility guarantee. Use a pinned tag or immutable digest through LeanLsp.start_runtime/1's :docker_image option, or through this module's direct :image option, when reproducible Lean versions matter.

Runtime options

  • :image - Docker image to start. Defaults to LeanLsp.Runtime.Config.default_docker_image/0.
  • :workdir, :container_workspace_root, or :workspace_root - working directory inside the container.
  • :mounts - Docker volume mounts as strings, {host, container}, or {host, container, mode} tuples. Bind mounts can expose host files to the container; use modes such as "ro" for read-only project access.
  • :env - environment variables as a map, keyword/list of pairs, or Docker KEY=value strings.
  • :container_name - optional Docker container name.
  • :docker_run_args - additional raw arguments passed to docker run.
  • :container_command - command used to keep the container alive.
  • :start_timeout and :stop_timeout - Docker command timeouts.

Execution accepts :workdir, :env, :docker_exec_args, and :timeout.

Workspace behaviour

The default workdir is /workspace inside the container. Setting the workdir does not automatically mount host files. Host filesystem access is opt-in via :mounts.

Lifecycle and cleanup

start_link/1 creates a long-lived container with docker run --detach --rm. stop/1 calls docker stop; cleanup is idempotent for an already-stopped runtime and treats a missing container as already cleaned up. If startup fails after a container is created, the implementation attempts to stop that container before returning the startup error.

When Docker is unavailable, startup returns {:error, reason}. Common causes include a missing Docker executable, Docker not running, insufficient permissions, an image that cannot be pulled or started, or invalid runtime options. The v0.1.0 public contract is the {:ok, runtime} / {:error, reason} shape; nested Docker error details are implementation-specific preview details.

Summary

Types

runtime()

Runtime process handle for the Docker-backed runtime.

Functions

child_spec(init_arg)

Returns a child specification suitable for supervisors.

exec(runtime, command, opts)

Executes a command inside the running Docker container.

start_link(opts)

Starts a Docker-backed runtime process.

stop(runtime)

Stops the Docker-backed runtime and cleans up its container.

Types

runtime()

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

Runtime process handle for the Docker-backed runtime.

This is usually the pid or registered name of the GenServer. Treat it as opaque and pass it to exec/3 and stop/1.

Functions

child_spec(init_arg)

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

Returns a child specification suitable for supervisors.

Runtime options are passed to start_link/1. The supervision-specific keys :id, :restart, and :shutdown are consumed while building the child spec.

The default restart mode is :transient, so an explicit normal stop does not cause the supervisor to restart the runtime. The default shutdown timeout is slightly longer than the Docker stop timeout to give container cleanup time to finish.

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 inside the running Docker container.

The command must be a non-empty list of strings, for example ["lean", "--version"]. The implementation runs it through docker exec and captures stdout, stderr, and the exit status.

Options include :workdir, :env, :docker_exec_args, and :timeout.

Returns {:ok, result} for exit status 0, {:error, {:command_failed, failure}} for observed non-zero exits, or {:error, reason} when the command cannot be executed or observed.

start_link(opts)

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

Starts a Docker-backed runtime process.

Startup checks Docker availability, runs docker run --detach --rm, and stores the resulting container id in the GenServer state. If the GenServer cannot be started after the container is created, the implementation attempts to stop the container before returning the startup error.

Important options include :image, :workdir, :mounts, :env, :container_name, :docker_run_args, :container_command, and :start_timeout.

stop(runtime)

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

Stops the Docker-backed runtime and cleans up its container.

This calls docker stop for the container owned by the runtime. Cleanup is idempotent for an already-stopped runtime and treats a missing container as already cleaned up.

Returns :ok when cleanup completes or {:error, reason} when Docker cleanup fails.