Lean LSP MCP -palvelin

Mitä “Lean LSP MCP” -palvelin tekee?

Lean LSP MCP on Model Context Protocol (MCP) -palvelin, joka yhdistää tekoälyassistentit Lean Theorem Prover -projekteihin Language Server Protocolin (LSP) kautta käyttämällä leanclientia. Se mahdollistaa agenttien ja LLM-mallien vuorovaikutuksen Lean-projektien kanssa tarjoten pääsyn diagnostiikkaan, tavoitetiloihin, termitietoon, hover-dokumentaatioon ja paljon muuhun. Tämä integraatio sujuvoittaa Lean-käyttäjien kehitystyötä tarjoamalla rikkaan, agenteille suunnatun työkalupakin, johon sisältyvät lausekkeiden haku, koodin täydennys ja projektin rakennustoiminnot. Palvelimen tavoitteena on parantaa kehittäjien, tutkijoiden ja tekoälyagenttien kokemusta Leanin parissa tekemällä Leanin työkalut helposti saavutettaviksi sekä automaattisissa että interaktiivisissa yhteyksissä.

Lista syötemalleista

Tietoa syötemallipohjista ei löytynyt arkistosta.

Lista resursseista

Tietoa julkaistuista MCP-resursseista ei löytynyt arkistosta.

Lista työkaluista

• Lean-lausekkeiden haku: Mahdollistaa agenttien lausekkeiden hakemisen leansearch.net-integraation avulla.
• Koodin täydennys: Tarjoaa koodin täydennysehdotuksia Lean-tiedostoille.
• Projektin rakennus: Mahdollistaa projektin rakentamisen Lean-rakennusjärjestelmän avulla.
• Diagnostiikka: Tarjoaa pääsyn diagnostisiin tietoihin Lean-projekteissa.
• Tavoitetilat & termitiedot: Näyttää tavoitetilan ja termitiedon syvällisempää projektianalyysia varten.
• Hover-dokumentaatio: Palauttaa dokumentaation, kun osoitat Lean-koodin osia.

Tämän MCP-palvelimen käyttötapaukset

• Lean-projektien diagnostiikka: Selaa ja näytä diagnostiikkaa koodin oikeellisuuden ja virheiden löytämiseksi Lean-projekteissa.
• Tavoitetilojen tutkiminen: Hae ja esitä ajankohtaiset tavoitetilat todistustyössä ja strategian suunnittelussa.
• Lausekkeiden haku: Hae relevantteja lausekkeita leansearch.netistä todistuksen rakentamisen tueksi.
• Koodin täydennys Leanille: Tarjoa älykkäitä koodin täydennyksiä ja ehdotuksia Lean-kielelle, parantaen tuottavuutta.
• Automaattiset projektin rakennukset: Käynnistä ja seuraa Lean-projektin rakennuksia osana automaattisia työnkulkuja tai agenttien koodikatselmointia.

Näin otat palvelimen käyttöön

Windsurf

1. Varmista, että uv on asennettu.
2. Rakenna Lean-projektisi suorittamalla lake build projektisi juuressa.
3. Etsi Windsurfin asetustiedosto.
4. Lisää Lean LSP MCP -palvelin seuraavalla JSON-pätkällä:

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

5. Tallenna ja käynnistä Windsurf uudelleen ja varmista, että MCP-palvelin toimii.

Claude

1. Asenna uv ja suorita lake build Lean-projektissasi.
2. Avaa Clauden asetustiedosto.
3. Lisää MCP-palvelimen konfiguraatio:

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

4. Tallenna ja käynnistä Claude uudelleen, ja varmista että palvelin on käytettävissä.

Cursor

1. Asenna uv ja suorita lake build.
2. Avaa Cursorin asetustiedosto.
3. Lisää Lean LSP MCP -palvelin:

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

4. Tallenna muutokset ja käynnistä Cursor uudelleen.

Cline

1. Varmista, että uv on asennettu ja suorita lake build.
2. Etsi ja muokkaa Clinen asetustiedostoa.
3. Lisää palvelin:

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

4. Tallenna ja käynnistä Cline uudelleen.

API-avainten suojaaminen

Jos ympäristössäsi vaaditaan API-avaimia, käytä ympäristömuuttujia niiden suojaamiseen. Esimerkki:

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

Näin käytät tätä MCP:tä flow’ssa

MCP:n käyttö FlowHuntissa

Jotta voit integroida MCP-palvelimet FlowHunt-työnkulkuusi, lisää ensin MCP-komponentti flow’hun ja yhdistä se tekoälyagenttiisi:

Klikkaa MCP-komponenttia avataksesi konfiguraatiopaneelin. Järjestelmän MCP-asetuksissa syötä MCP-palvelimesi tiedot seuraavassa JSON-muodossa:

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

Kun olet konfiguroinut asetukset, tekoälyagenttisi voi käyttää tätä MCP:tä työkaluna ja hyödyntää kaikkia sen toimintoja. Muista vaihtaa “lean-lsp-mcp” oman MCP-palvelimesi nimeen ja korvata URL omalla MCP-palvelimesi osoitteella.

Yhteenveto

Saatavilla olevan dokumentaation ja koodin perusteella Lean LSP MCP tarjoaa vahvan työkalutuen Lean-projekteille, mutta siltä puuttuu eksplisiittiset syötemallit ja MCP-resurssimääritykset. Näytteenottoa eikä juuritukea mainita. Kaiken kaikkiaan palvelin on käytännöllinen Lean-käyttäjille, mutta ei vielä tarjoa kaikkia edistyneitä MCP-ominaisuuksia.

MCP-pisteet