Lean LSP MCP Server

Máy chủ “Lean LSP MCP” dùng để làm gì?

Lean LSP MCP là một máy chủ Model Context Protocol (MCP) kết nối trợ lý AI với các dự án Lean Theorem Prover thông qua Language Server Protocol (LSP) sử dụng leanclient. Nó cho phép các tác nhân và LLM tương tác với dự án Lean, cung cấp quyền truy cập chẩn đoán, trạng thái mục tiêu, thông tin về thuật ngữ, tài liệu hover và nhiều hơn nữa. Sự tích hợp này đơn giản hóa quy trình phát triển cho người dùng Lean bằng cách cung cấp bộ công cụ tập trung vào tác nhân, bao gồm tìm kiếm định lý, tự động hoàn thành mã và chức năng xây dựng dự án. Máy chủ này nhằm nâng cao trải nghiệm cho nhà phát triển, nhà nghiên cứu và tác nhân AI làm việc với Lean bằng cách làm cho công cụ Lean trở nên dễ tiếp cận trong các bối cảnh tự động hóa và tương tác.

Danh sách Prompt

Không tìm thấy thông tin về các mẫu prompt trong kho lưu trữ.

Danh sách tài nguyên

Không tìm thấy thông tin về tài nguyên MCP được cung cấp trong kho lưu trữ.

Danh sách Công cụ

• Tìm kiếm Định lý Lean: Cho phép tác nhân tìm kiếm các định lý thông qua tích hợp leansearch.net.
• Tự động hoàn thành mã: Đưa ra gợi ý tự động hoàn thành mã cho tệp Lean.
• Xây dựng dự án: Hỗ trợ xây dựng dự án thông qua hệ thống build của Lean.
• Chẩn đoán: Cung cấp quyền truy cập chẩn đoán trong dự án Lean.
• Trạng thái mục tiêu & Thông tin thuật ngữ: Cung cấp thông tin trạng thái mục tiêu và thuật ngữ để phân tích sâu hơn dự án.
• Tài liệu Hover: Trả về tài liệu khi di chuột qua các phần tử mã Lean.

Các trường hợp sử dụng của máy chủ MCP này

• Chẩn đoán dự án Lean: Truy cập và hiển thị nhanh các chẩn đoán về tính đúng đắn và gỡ lỗi mã trong dự án Lean.
• Khám phá trạng thái mục tiêu: Lấy và hiển thị trạng thái mục tiêu hiện tại cho phát triển chứng minh và lên kế hoạch chiến lược.
• Tìm kiếm định lý: Tìm kiếm định lý liên quan từ leansearch.net để hỗ trợ xây dựng chứng minh.
• Tự động hoàn thành mã cho Lean: Đưa ra các gợi ý tự động hoàn thành và đề xuất thông minh cho Lean, nâng cao năng suất.
• Tự động hóa xây dựng dự án: Kích hoạt và giám sát quá trình xây dựng dự án Lean như một phần của quy trình tự động hoặc đánh giá mã do tác nhân thực hiện.

Cách thiết lập

Windsurf

1. Đảm bảo đã cài đặt uv.
2. Xây dựng dự án Lean của bạn bằng cách chạy lake build tại thư mục gốc của dự án.
3. Tìm tệp cấu hình Windsurf.
4. Thêm máy chủ Lean LSP MCP bằng đoạn JSON sau:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

5. Lưu và khởi động lại Windsurf, sau đó kiểm tra máy chủ MCP đã chạy.

Claude

1. Cài đặt uv và chạy lake build trong dự án Lean của bạn.
2. Mở tệp cấu hình của Claude.
3. Thêm cấu hình máy chủ MCP:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

4. Lưu và khởi động lại Claude, xác nhận máy chủ đã sẵn sàng.

Cursor

1. Cài đặt uv và chạy lake build.
2. Mở tệp cấu hình của Cursor.
3. Thêm máy chủ Lean LSP MCP:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

4. Lưu thay đổi và khởi động lại Cursor.

Cline

1. Đảm bảo đã cài đặt uv và chạy lake build.
2. Tìm và chỉnh sửa tệp cấu hình Cline.
3. Thêm máy chủ:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

4. Lưu và khởi động lại Cline.

Bảo mật API Key

Nếu thiết lập của bạn yêu cầu API key, hãy dùng biến môi trường để bảo mật. Ví dụ:

{
  "mcpServers": {
    "lean-lsp-mcp": {
      "command": "lean-lsp-mcp",
      "args": [],
      "env": {
        "API_KEY": "${env:LEAN_LSP_MCP_API_KEY}"
      },
      "inputs": {
        "api_key": "${env:LEAN_LSP_MCP_API_KEY}"
      }
    }
  }
}

Cách sử dụng MCP này trong flows

Sử dụng MCP trong FlowHunt

Để tích hợp máy chủ MCP vào quy trình FlowHunt của bạn, hãy bắt đầu bằng cách thêm thành phần MCP vào flow và kết nối nó với tác nhân AI của bạn:

Nhấp vào thành phần MCP để mở bảng cấu hình. Trong phần cấu hình hệ thống MCP, chèn thông tin máy chủ MCP của bạn bằng định dạng JSON sau:

{
  "lean-lsp-mcp": {
    "transport": "streamable_http",
    "url": "https://yourmcpserver.example/pathtothemcp/url"
  }
}

Khi đã cấu hình xong, tác nhân AI sẽ có thể sử dụng MCP này như một công cụ với đầy đủ chức năng và khả năng. Lưu ý thay “lean-lsp-mcp” bằng tên thực tế của máy chủ MCP của bạn và thay đổi URL thành URL máy chủ MCP của bạn.

Tổng quan

Dựa trên tài liệu và mã nguồn hiện có, Lean LSP MCP cung cấp hỗ trợ công cụ mạnh mẽ cho dự án Lean nhưng chưa có mẫu prompt hoặc định nghĩa tài nguyên MCP rõ ràng. Hỗ trợ sampling và roots chưa được đề cập. Tổng thể, máy chủ này thực tế cho người dùng Lean nhưng chưa cung cấp đầy đủ các tính năng MCP nâng cao.

MCP Score