LeanLsp.Runtime.Config (LeanLsp v0.1.0)

Normalized runtime configuration for LeanLsp.

This module keeps runtime selection and runtime defaults explicit. It does not start Docker, create containers, or allocate external resources; it only validates options and converts them into the option shape expected by the selected runtime implementation.

The default runtime is LeanLsp.Runtime.Docker, but callers can pass :runtime to use a test runtime or another module that implements LeanLsp.Runtime.

Supported options

:runtime - runtime implementation module.
:docker_image - Docker image used by the default Docker runtime.
:container_workspace_root - working directory inside the container.
:workspace_root - alias for :container_workspace_root.
:runtime_options - keyword options passed directly to the selected runtime.

Additional keyword options are merged into :runtime_options. This lets callers pass runtime-specific options such as :mounts, :env, or timeouts without changing the top-level LeanLsp API.

Defaults

:runtime - LeanLsp.Runtime.Docker
:docker_image - "leanprovercommunity/lean4:latest"
:container_workspace_root - "/workspace"

The v0.1.0 preview keeps leanprovercommunity/lean4:latest as a convenience default. It is not a reproducibility guarantee; callers that need reproducible Lean versions should pass a pinned tag or immutable digest with :docker_image.

:container_workspace_root is the path inside the container. It does not mount a host directory by itself. Host workspace mounting remains a runtime concern and can be configured with runtime-specific options such as :mounts.

Summary

Types

t()

Defaults

default_container_workspace_root()

Returns the default working directory inside the Docker container.

default_docker_image()

Returns the Docker image used by the default Docker runtime.

default_runtime()

Returns the runtime module used by default.

Normalization

normalize(opts)

Validates and normalizes user-provided runtime options.

to_runtime_options(config)

Converts a normalized config into options for the selected runtime.

Types

t()

@type t() :: %LeanLsp.Runtime.Config{
  container_workspace_root: String.t(),
  docker_image: String.t(),
  runtime: module(),
  runtime_options: keyword()
}

Defaults

default_container_workspace_root()

@spec default_container_workspace_root() :: String.t()

Returns the default working directory inside the Docker container.

default_docker_image()

@spec default_docker_image() :: String.t()

Returns the Docker image used by the default Docker runtime.

default_runtime()

@spec default_runtime() :: module()

Returns the runtime module used by default.

In v0.1.0 this is LeanLsp.Runtime.Docker.

Normalization

normalize(opts)

@spec normalize(keyword()) :: {:ok, t()} | {:error, term()}

Validates and normalizes user-provided runtime options.

Returns {:ok, config} when the options are a keyword list, the runtime module implements LeanLsp.Runtime, Docker-specific defaults are valid, and :runtime_options is a keyword list.

Returns {:error, {:invalid_options, value}} when the input is not a keyword list, or {:error, {:invalid_option, key}} when a specific option is invalid. This function does not start Docker or create a runtime.

to_runtime_options(config)

@spec to_runtime_options(t()) :: keyword()

Converts a normalized config into options for the selected runtime.

For LeanLsp.Runtime.Docker, this maps the public configuration fields to the Docker runtime option names by setting :image and :workdir, then merges any runtime-specific options.

For non-Docker runtimes, this returns config.runtime_options unchanged.