Runtime dependency and Docker image policy

LeanLsp v0.1.0 exposes a Docker-backed Lean runtime preview. Users can install and inspect configuration without Docker, but starting the default runtime requires Docker.

External runtime requirement

Docker is required for the default runtime path:

• LeanLsp.runtime_config/1 validates and normalizes options without starting Docker.
• LeanLsp.start_runtime/1 starts LeanLsp.Runtime.Docker by default and needs a reachable Docker executable.
• The calling environment must have permission to run Docker containers.
• The selected image must be available locally or pullable by Docker.

A local Lean installation on the host is not required for this Docker-first runtime path.

Default image policy

The v0.1.0 preview default image is:

leanprovercommunity/lean4:latest

The package keeps latest as the default for the initial preview so users get a small, convenient Lean runtime without choosing an image up front. This is a convenience default, not a reproducibility guarantee.

For reproducible workflows, pass a pinned tag or immutable digest explicitly with the public :docker_image option:

{:ok, runtime} =
  LeanLsp.start_runtime(
    docker_image: "leanprovercommunity/lean4:<pinned-tag-or-digest>"
  )

When calling LeanLsp.Runtime.Docker.start_link/1 directly, use the runtime :image option name:

{:ok, runtime} =
  LeanLsp.Runtime.Docker.start_link(
    image: "leanprovercommunity/lean4:<pinned-tag-or-digest>"
  )

Workspace and mount behaviour

:container_workspace_root configures the working directory inside the container. It does not automatically mount a host directory.

Host filesystem access is opt-in through the runtime-specific :mounts option:

{:ok, runtime} =
  LeanLsp.start_runtime(
    container_workspace_root: "/workspace",
    mounts: [{File.cwd!(), "/workspace", "ro"}]
  )

Docker bind mounts can expose host files to the container. Use read-only mounts such as "ro" when the runtime only needs to read project files.

Container lifecycle and cleanup

LeanLsp.start_runtime/1 starts a long-lived Docker container. The returned runtime handle is opaque and should be passed to LeanLsp.Runtime.Docker.exec/3 and LeanLsp.Runtime.Docker.stop/1.

Callers that start the runtime directly are responsible for stopping it:

{:ok, runtime} = LeanLsp.start_runtime()

try do
  LeanLsp.Runtime.Docker.exec(runtime, ["lean", "--version"], [])
after
  LeanLsp.Runtime.Docker.stop(runtime)
end

The Docker implementation uses docker stop during cleanup and treats an already-missing container as cleaned up. Supervised callers can use LeanLsp.Runtime.Docker.child_spec/1 and let the supervisor lifecycle stop the runtime process.

Expected Docker-related errors

When Docker is unavailable, the runtime cannot start and returns {:error, reason}. The exact reason is implementation-specific during the v0.1.0 preview, but common causes include:

• Docker is not installed.
• Docker is not running or is unreachable from the BEAM process.
• The current user does not have permission to run Docker.
• The selected image cannot be pulled or started.
• Invalid runtime options such as malformed mounts, environment variables, or timeouts.

Code should match on {:ok, runtime} / {:error, reason} rather than relying on undocumented nested Docker error details.