Lean LSP MCP Sunucusu

“Lean LSP MCP” Sunucusu Ne İşe Yarar?

Lean LSP MCP, Lean Teorem İspatlayıcı projelerini Yapay Zeka asistanlarıyla Dil Sunucu Protokolü (LSP) üzerinden leanclient kullanarak buluşturan bir Model Context Protocol (MCP) sunucusudur. Ajanların ve büyük dil modellerinin Lean projeleriyle etkileşim kurmasına olanak tanır; teşhis, hedef durumu, terim bilgisi, üzerine gelme dokümantasyonu ve daha fazlasına erişim sağlar. Bu entegrasyon, Lean kullanıcılarının geliştirme iş akışlarını, teorem arama, kod tamamlama ve proje derleme gibi zengin, ajana odaklı araç seti sunarak kolaylaştırır. Sunucu, geliştiriciler, araştırmacılar ve Yapay Zeka ajanları için Lean’in araçlarını otomatik ve etkileşimli ortamlarda erişilebilir kılarak kullanıcı deneyimini geliştirmeyi hedefler.

Komut Şablonları Listesi

Depoda komut şablonları hakkında herhangi bir bilgi bulunamadı.

Kaynaklar Listesi

Depoda sunulan MCP kaynakları hakkında herhangi bir bilgi bulunamadı.

Araçlar Listesi

• Lean Teorem Arama: leansearch.net entegrasyonu ile ajanların teorem aramasına olanak tanır.
• Kod Tamamlama: Lean dosyaları için kod tamamlama önerileri sunar.
• Proje Derleme: Lean derleme sistemi aracılığıyla proje derlemelerini kolaylaştırır.
• Teşhis: Lean projelerinde teşhislere erişim sağlar.
• Hedef Durumları & Terim Bilgisi: Daha derin proje analizi için hedef durumu ve terim bilgisini sunar.
• Üzerine Gelme Dökümantasyonu: Lean kod ögelerinin üzerine gelindiğinde dökümantasyon döndürür.

Bu MCP Sunucusunun Kullanım Alanları

• Lean Proje Teşhisi: Lean projelerinde kod doğruluğu ve hata ayıklama için teşhisleri anında alın ve gösterin.
• Hedef Durumu Keşfi: İspat geliştirme ve strateji planlaması için mevcut hedef durumları alın ve görüntüleyin.
• Teorem Arama: leansearch.net üzerinden ilgili teoremleri arayarak ispat sürecine yardımcı olun.
• Lean için Kod Tamamlama: Lean için akıllı kod tamamlama ve öneriler sunarak üretkenliği artırın.
• Otomatik Proje Derlemeleri: Otomatik iş akışları veya ajana dayalı kod incelemesinin bir parçası olarak Lean proje derlemelerini tetikleyin ve izleyin.

Kurulum Nasıl Yapılır

Windsurf

1. uv yüklü olduğundan emin olun.
2. Proje kök dizininizde lake build komutunu çalıştırarak Lean projenizi derleyin.
3. Windsurf yapılandırma dosyasını bulun.
4. Aşağıdaki JSON kesitini kullanarak Lean LSP MCP sunucusunu ekleyin:

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

5. Kaydedin ve Windsurf’u yeniden başlatın, ardından MCP sunucusunun çalıştığını doğrulayın.

Claude

1. uv’yi yükleyin ve Lean projenizde lake build komutunu çalıştırın.
2. Claude’un yapılandırma dosyasını açın.
3. MCP sunucu yapılandırmasını ekleyin:

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

4. Kaydedin ve Claude’u yeniden başlatın; ardından sunucunun hazır olduğunu doğrulayın.

Cursor

1. uv yükleyin ve lake build komutunu çalıştırın.
2. Cursor’un yapılandırma dosyasını açın.
3. Lean LSP MCP sunucusunu ekleyin:

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

4. Değişiklikleri kaydedin ve Cursor’u yeniden başlatın.

Cline

1. uv’nin yüklü olduğundan emin olun ve lake build komutunu çalıştırın.
2. Cline yapılandırma dosyasını bulun ve düzenleyin.
3. Sunucuyu ekleyin:

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

4. Kaydedin ve Cline’ı yeniden başlatın.

API Anahtarlarını Güvenceye Alma

Kurulumunuzda API anahtarları gerekiyorsa, bunları güvenli tutmak için ortam değişkenlerini kullanın. Örnek:

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

Flow’larda Bu MCP Nasıl Kullanılır

FlowHunt’ta MCP Kullanımı

MCP sunucularını FlowHunt iş akışınıza entegre etmek için, öncelikle MCP bileşenini akışınıza ekleyin ve AI ajanınıza bağlayın:

MCP bileşenine tıklayarak yapılandırma panelini açın. Sistem MCP yapılandırma bölümüne aşağıdaki JSON formatında MCP sunucu bilgilerinizi girin:

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

Yapılandırma tamamlandığında, AI ajanınız bu MCP’nin tüm işlev ve yeteneklerine sahip bir araç olarak kullanabilir. “lean-lsp-mcp” adını kendi MCP sunucunuzun ismine, URL kısmını ise kendi MCP sunucunuzun adresine göre değiştirmeniz gerektiğini unutmayın.

Genel Bakış

Mevcut dokümantasyon ve koda göre, Lean LSP MCP Lean projeleri için güçlü araç desteği sunar, ancak açık komut şablonları veya MCP kaynak tanımı içermez. Örnekleme ve kök desteğinden bahsedilmemiştir. Genel olarak, sunucu Lean kullanıcıları için pratik olsa da henüz tüm gelişmiş MCP özelliklerini sunmamaktadır.

MCP Puanı