Skip to main content

oak_lean/mcp/
mod.rs

1#![doc = include_str!("readme.md")]
2use crate::lsp::LeanLanguageService;
3use oak_vfs::MemoryVfs;
4
5/// Start an MCP server for Lean semantics (Stdio).
6pub async fn serve_lean_mcp(_vfs: MemoryVfs) {
7    let service = LeanLanguageService::new(crate::language::LeanLanguage::default());
8    let server = oak_mcp::McpServer::new(service);
9
10    let reader = tokio::io::BufReader::new(tokio::io::stdin());
11    let writer = tokio::io::BufWriter::new(tokio::io::stdout());
12    server.run(reader, writer).await.unwrap()
13}