خادم Lean LSP MCP

ماذا يفعل خادم “Lean LSP MCP”؟

Lean LSP MCP هو خادم بروتوكول سياق النماذج (MCP) يصل المساعدات الذكية بمشاريع Lean Theorem Prover عبر بروتوكول خادم اللغة (LSP) باستخدام leanclient. يمكّن الوكلاء ونماذج اللغة الكبيرة من التفاعل مع مشاريع Lean، ويوفر الوصول إلى التشخيصات، حالات الأهداف، معلومات المصطلحات، توثيق التلميحات، والمزيد. يبسّط هذا التكامل سير العمل التطويري لمستخدمي Lean من خلال إتاحة مجموعة أدوات غنية موجهة للوكلاء، بما في ذلك البحث عن النظريات، إكمال الشيفرة، وميزات بناء المشروع. يهدف الخادم إلى تحسين تجربة المطورين والباحثين والوكلاء الذكاء الاصطناعي العاملين مع Lean عبر إتاحة أدوات Lean في السياقات المؤتمتة والتفاعلية.

قائمة القوالب

لم يتم العثور على معلومات حول قوالب المطالبات في المستودع.

قائمة الموارد

لم يتم العثور على معلومات حول الموارد المكشوفة في المستودع.

قائمة الأدوات

• البحث عن نظريات Lean: يتيح للوكلاء البحث عن النظريات عبر تكامل leansearch.net.
• إكمال الشيفرة: يوفر اقتراحات لإكمال الشيفرة لملفات Lean.
• بناء المشروع: يسهل عمليات بناء المشروع من خلال نظام بناء Lean.
• التشخيصات: يقدم وصولًا إلى التشخيصات داخل مشاريع Lean.
• معلومات حالة الأهداف والمصطلحات: يكشف معلومات حالات الأهداف والمصطلحات لتحليل أعمق للمشروع.
• توثيق التلميحات: يعرض التوثيق عند تمرير المؤشر فوق عناصر الشيفرة في Lean.

حالات الاستخدام لهذا الخادم MCP

• تشخيصات مشاريع Lean: الوصول الفوري وعرض التشخيصات لصحة الشيفرة وتصحيح الأخطاء ضمن مشاريع Lean.
• استكشاف حالات الأهداف: استرجاع وعرض حالات الأهداف الحالية لتطوير البراهين وتخطيط الاستراتيجية.
• البحث عن النظريات: البحث عن نظريات ذات صلة من leansearch.net لدعم بناء البراهين.
• إكمال الشيفرة لـ Lean: توفير إكمال ذكي واقتراحات للشيفرة في Lean لتعزيز الإنتاجية.
• بناء المشاريع المؤتمت: تشغيل ومراقبة بناء مشاريع Lean ضمن سير العمل المؤتمت أو مراجعة الشيفرة بواسطة الوكلاء.

كيفية الإعداد

Windsurf

1. تأكد من تثبيت uv.
2. ابنِ مشروع Lean الخاص بك بتشغيل lake build في مجلد المشروع الجذري.
3. حدد موقع ملف إعدادات Windsurf.
4. أضف خادم Lean LSP MCP باستخدام المقطع JSON التالي:

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

5. احفظ وأعد تشغيل Windsurf ثم تحقق من تشغيل خادم MCP.

Claude

1. قم بتثبيت uv وشغّل lake build في مشروع Lean الخاص بك.
2. افتح ملف إعدادات Claude.
3. أدرج إعدادات خادم MCP:

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

4. احفظ وأعد تشغيل Claude ثم تأكد من توفر الخادم.

Cursor

1. قم بتثبيت uv وشغّل lake build.
2. افتح ملف إعدادات Cursor.
3. أضف خادم Lean LSP MCP:

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

4. احفظ التغييرات وأعد تشغيل Cursor.

Cline

1. تأكد من تثبيت uv وشغل lake build.
2. ابحث عن ملف إعدادات Cline وقم بتحريره.
3. أضف الخادم:

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

4. احفظ وأعد تشغيل Cline.

تأمين مفاتيح API

إذا كان إعدادك يتطلب مفاتيح API، استخدم متغيرات البيئة للحفاظ على أمانها. مثال:

{
  "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}"
      }
    }
  }
}

كيفية استخدام هذا الخادم MCP ضمن التدفقات

استخدام MCP في FlowHunt

لدمج خوادم MCP ضمن سير عمل FlowHunt الخاص بك، ابدأ بإضافة مكون MCP إلى تدفقك وربطه بوكيل الذكاء الاصطناعي لديك:

اضغط على مكون MCP لفتح لوحة الإعدادات. في قسم إعداد النظام MCP، أدخل تفاصيل الخادم باستخدام هذا التنسيق لـ JSON:

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

بعد الإعداد، سيتمكن وكيل الذكاء الاصطناعي من استخدام هذا الخادم MCP كأداة مع الوصول إلى جميع وظائفه. تذكّر تغيير “lean-lsp-mcp” إلى اسم خادم MCP الفعلي واستبدال الرابط الإلكتروني بعنوان خادم MCP الخاص بك.

نظرة عامة

استنادًا إلى الوثائق والشيفرة المتوفرة، يوفر Lean LSP MCP دعمًا قويًا لأدوات مشاريع Lean لكنه يفتقر لقوالب المطالبات الصريحة أو تعريفات موارد MCP. لم يتم ذكر دعم أخذ العينات والجذور. بشكل عام، الخادم عملي لمستخدمي Lean لكنه لا يوفر حتى الآن جميع ميزات MCP المتقدمة.

تقييم MCP