LeanLsp

LeanLsp is an experimental Lean LSP foundation and Docker runtime preview for Elixir.

Version 0.1.0 is an initial Hex release for the runtime layer. It lets users install the package, normalize runtime configuration, start the Docker-backed runtime, and execute commands through the runtime behaviour. It is not a production-ready Lean LSP client yet.

Installation

For the v0.1.0 Hex release, add lean_lsp to your dependencies:

def deps do
  [
    {:lean_lsp, "~> 0.1.0"}
  ]
end

Package links

The package and documentation use these canonical public locations:

The Hex package and HexDocs links become live after v0.1.0 is published.

Requirements

For package users:

• Elixir ~> 1.19, as declared in mix.exs.
• An Erlang/OTP version supported by the Elixir version used in your project.
• Docker installed and reachable from the environment that starts the runtime.
• Permission to run Docker containers and either pull or already have access to the default image, leanprovercommunity/lean4:latest.

A local Lean installation is not required for the Docker-first runtime path. LeanLsp.runtime_config/1 can be used without Docker; LeanLsp.start_runtime/1 uses Docker by default.

Docker image policy

The v0.1.0 default image is leanprovercommunity/lean4:latest. This is a convenience default for the runtime preview, not a reproducibility guarantee. For reproducible workflows, pass a pinned tag or immutable digest with :docker_image:

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

When calling LeanLsp.Runtime.Docker.start_link/1 directly, use :image.

Workspace mounts and cleanup

:container_workspace_root controls the working directory inside the container. It does not automatically mount host files. Host filesystem access is opt-in via runtime-specific :mounts; use read-only mount modes such as "ro" when the container only needs to read project files.

The Docker runtime starts a long-lived container. Callers that start it directly should stop it with LeanLsp.Runtime.Docker.stop/1 when finished. If Docker is not installed, unavailable, or not permitted for the current user, runtime startup returns {:error, reason}.

Quick start

Normalize the default runtime configuration:

{:ok, config} = LeanLsp.runtime_config()

%LeanLsp.Runtime.Config{
  runtime: LeanLsp.Runtime.Docker,
  docker_image: "leanprovercommunity/lean4:latest",
  container_workspace_root: "/workspace"
} = config

Start the Docker runtime and run a Lean command:

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

try do
  {:ok, result} = LeanLsp.Runtime.Docker.exec(runtime, ["lean", "--version"], [])
  IO.puts(result.stdout)
after
  LeanLsp.Runtime.Docker.stop(runtime)
end

The second example requires Docker. If Docker is not installed, unavailable, or not permitted for the current user, runtime startup returns an error.

Release status

v0.1.0 is a foundation/runtime-preview release. It is suitable for trying the package metadata, runtime configuration, and Docker-backed runtime boundary. It is intentionally not a complete language-server client.

Included in v0.1.0

The documented runtime defaults are:

Not included yet

The following features are roadmap work and should not be treated as available in v0.1.0:

• A production-ready Lean LSP client.
• Stable application-level APIs for Lean LSP requests.
• LeanLsp.Session, LeanLsp.Transport, and LeanLsp.Protocol as usable public modules.
• Lean document open/change/close lifecycle management.
• Diagnostics, hover, completion, go-to-definition, or other editor-style query helpers.
• Lean fixture projects and integration-test coverage for complete LSP workflows.
• Compatibility guarantees for Docker command internals, generated container names, runtime process state, or implementation-specific error detail shapes.

0.x compatibility policy

LeanLsp is experimental while its version is below 1.0.0.

Patch releases in the same 0.x minor line should avoid breaking the documented public preview contract unless a correction is required for safety, correctness, or package-publication issues.

Minor 0.x releases may change, rename, or remove preview APIs when the runtime and LSP client design evolves. Undocumented modules, private helpers, internal process state, Docker command construction, and implementation-specific error details may change without deprecation during 0.x.

Roadmap

Architecture

LeanLsp separates runtime execution from the LSP client layer. Docker-specific code belongs in LeanLsp.Runtime.Docker; future Session, Transport, and Protocol code should use the runtime abstraction instead of calling Docker directly.

Application code
      |
      v
+----------------+
| LeanLsp        | public API and option validation
+----------------+
      |
      v
+-----------------+       builds and parses       +------------------+
| LeanLsp.Session | <---------------------------> | LeanLsp.Protocol |
| LSP state       |                               | LSP/JSON-RPC     |
+-----------------+                               +------------------+
      |
      | framed messages
      v
+-------------------+
| LeanLsp.Transport | Content-Length framing and IO
+-------------------+
      |
      | process-like IO
      v
+-----------------+
| LeanLsp.Runtime | runtime contract
+-----------------+
      |
      v
+------------------------+
| LeanLsp.Runtime.Docker | Docker implementation
+------------------------+
      |
      v
Lean language server

Module responsibilities

For detailed boundary rules, see Module responsibilities.

Runtime configuration

Runtime configuration is explicit and normalized through LeanLsp.Runtime.Config.

{:ok, runtime} =
  LeanLsp.start_runtime(
    docker_image: "leanprovercommunity/lean4:latest",
    container_workspace_root: "/workspace"
  )

LeanLsp.Runtime.Docker.stop(runtime)

Additional documentation

• Release scope and stability
• Hex package metadata
• Runtime dependency and Docker policy
• Module responsibilities
• Changelog

Development setup

Install dependencies

mix local.hex --force
mix local.rebar --force
mix deps.get

Run the quality gate

mix check

Run mix check before opening a pull request. It is the repository quality gate used by CI.

Run local pre-commit checks

mix precommit

mix precommit is intended for local use when you want formatting fixes and the full local validation path.

License

Copyright (c) 2026 University of Kitakyushu

Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at http://www.apache.org/licenses/LICENSE-2.0.

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.