# `LeanLsp.Runtime.Docker`
[🔗](https://github.com/zacky1972/lean_lsp/blob/main/lib/lean_lsp/runtime/docker.ex#L1)

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.

## Docker-related failures

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.

# `runtime`

```elixir
@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`.

# `child_spec`

```elixir
@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`

```elixir
@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`

```elixir
@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`

```elixir
@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.

---

*Consult [api-reference.md](api-reference.md) for complete listing*