Leanllm 0.2.0

leanllm v0.2.0 — model version constructors now use underscore decimal separators, matching how Lean identifiers represent dotted version numbers.

Consumers should update constructor names when bumping from v0.1.0. Wire IDs and OpenRouter slugs are unchanged.

Breaking: underscore version constructors

Family	v0.1.0	v0.2.0
Claude	.opus55, .sonnet55, .haiku55, .fable51, .opus45, .sonnet45, .haiku45	.opus5_5, .sonnet5_5, .haiku5_5, .fable5_1, .opus4_5, .sonnet4_5, .haiku4_5
OpenAI	.gpt56Sol, .gpt56Terra, .gpt56Luna, .gpt55, .gpt54	.gpt5_6Sol, .gpt5_6Terra, .gpt5_6Luna, .gpt5_5, .gpt5_4
Gemini	.flash38, .flash35, .pro25, .flash25	.flash3_8, .flash3_5, .pro2_5, .flash2_5
DeepSeek	.v41Flash, .v32	.v4_1Flash, .v3_2
Kimi	.k27Code, .k26, .k25	.k2_7Code, .k2_6, .k2_5
GLM	.glm53Prime, .glm53, .glm53Flash, .glm52, .glm51, .glm47, .glm47Flash	.glm5_3Prime, .glm5_3, .glm5_3Flash, .glm5_2, .glm5_1, .glm4_7, .glm4_7Flash
Qwen	.qwen38Max, .qwen38Flash, .qwen37Max, .qwen37Plus, .qwen35Plus	.qwen3_8Max, .qwen3_8Flash, .qwen3_7Max, .qwen3_7Plus, .qwen3_5Plus
MiniMax	.m27, .m25	.m2_7, .m2_5
Grok	.grok47, .grok46, .grok45, .grok43, .grokBuild01	.grok4_7, .grok4_6, .grok4_5, .grok4_3, .grokBuild0_1
Mistral	.medium35	.medium3_5

Unchanged constructors (no decimal in the version): .opus5, .sonnet5, .gpt6Astra, .gpt4o, .gpt4oMini, .o3, .o4Mini, .argon4, .v4Pro, .v4Flash, .chat, .reasoner, .k3, .k2Thinking, .forCoding, .glm5, .coderNext, .coderPlus, .m3, .m2, .codeFast1, .large4, .small2603, .devstral, and all .custom id variants.

Other

• Install libcurl development headers in CI so Lake/LeanHttp builds have the native dependency.

Install:

[[require]]
name = "leanllm"
git = "https://github.com/theoriclabs/leanllm"
rev = "v0.2.0"

Leanllm 0.1.0

Initial release of leanllm (v0.1.0), a unified LLM client library for Lean 4 built on LeanHttp (v0.6.0).

Highlights

• Four Orthogonal Axes (Model × Provider × WireApi × AuthMode):
  • 10 Model Families: ClaudeModel, OpenAIModel, GeminiModel, DeepSeekModel, KimiModel, GlmModel, QwenModel, MiniMaxModel, GrokModel, and MistralModel.
  • Providers: .direct, .openRouter, .bedrock, .azure, .vertex, .copilot, .antigravity, .grokBuild, .kimiCode, .zaiCoding, .alibabaCoding, .opencodeZen, .opencodeGo, .groq, .cerebras, .together, .fireworks, .deepinfra, .novita, .baseten, .nebius, .nvidiaNim, .ollama, .lmstudio, and .custom.
  • 6 Wire Dialects: .anthropicMessages, .openaiChat, .openaiResponses, .geminiGenerate, .bedrockConverse, and .bedrockInvoke.
• Subscription OAuth & Cross-Tool Credential Reuse (Leanllm.Auth):
  • Reuses and proactively refreshes local subscription OAuth sessions from Claude Code (~/.claude/.credentials.json, macOS Keychain, $CLAUDE_CODE_OAUTH_TOKEN), OpenAI Codex (~/.codex/auth.json), Gemini CLI (~/.gemini/oauth_creds.json), Antigravity, GitHub Copilot (~/.config/github-copilot/hosts.json), Grok CLI (~/.grok/auth.json), jcode (~/.jcode/), OpenCode, Pi, OpenClaw, and Hermes.
  • Pure Lean Base64URL + JWT claim decoding (exp, client_id, aud, azp, chatgpt_account_id) with zero hardcoded OAuth client IDs.
• Monadic Interface (LLMM) & SSE Streaming:
  • ReaderT LLMContext (ExceptT LLMError IO) with automatic LeanHttp.Session reuse and scoped combinators (LLMM.withProvider, LLMM.withWireApi, LLMM.withModel, LLMM.withAuth).
  • Synchronous (call, completion, ask) and incremental Server-Sent Events streaming (callStream, completionStream, askStream) with multimodal images, tool calling, and reasoning/thinking blocks.