Changelog

v0.1.0

Release scope

LeanLsp v0.1.0 is the first Hex release candidate for the repository foundation and Docker-backed runtime layer. It is a preview release intended for users who want to evaluate runtime configuration and Docker execution boundaries before the higher-level Lean LSP client API is implemented.

Included

• Public runtime entry points:
  • LeanLsp.runtime_config/1
  • LeanLsp.start_runtime/1
• LeanLsp.Runtime behaviour for runtime implementations, including start_link/1, stop/1, and exec/3.
• LeanLsp.Runtime.Config for normalizing runtime options and applying defaults.
• LeanLsp.Runtime.Docker as the Docker-backed runtime implementation.
• Docker container startup, command execution through docker exec, and cleanup through docker stop.
• Runtime defaults:
  • Docker image: leanprovercommunity/lean4:latest
  • Container workspace root: /workspace

Requirements and limitations

• Docker must be installed and reachable from the environment running the package.
• v0.1.0 does not provide a production-ready Lean LSP client.
• High-level Lean query APIs are not available yet.
• Session, Transport, and Protocol functionality for JSON-RPC/LSP request lifecycle management is not implemented yet.
• Editor-style features such as diagnostics, hover, completion, go-to-definition, and document open/change/close lifecycle handling are out of scope for this release.
• Docker command internals, generated container names, runtime process state, and implementation-specific error details should be treated as preview internals.

Compatibility

The 0.1.x line should preserve the documented runtime preview contract where practical. Later 0.x minor releases may change preview APIs as the runtime and Lean LSP client design evolves.