setting up leantool in roo-code

Stream: Machine Learning for Theorem Proving

[Jared green]

is there a way to set up LeanTool in roo-code?

[Jared green]

where do i set the api key in the last step, and how do i get the base url to provide to roo-code?

[GasStationManager]

After installing and opening roo-code, there's a page "welcome to roo-code...", then "Express setup throgh a router"; scroll further down, look under "Bring your own API key", then in the list of providers select "OpenAI Compatible", then it will let you input the base url and your API key.

[Jared green]

i already installed roo-code. how do i get to that page?

[GasStationManager]

Click on the kangaroo on the left pane to open the roo pane. If that page doesn't appear, try the settings icon on the top of the roo pane.

[Jared green]

i got an api key from anthropic. what do i put in the other fields? my copy of LeanTool is at
C:\\Users\\jared\\AppData\\Roaming\\Roo-Code\\MCP\\LeanTool

[GasStationManager]

For roo code, LeanTool can be deployed two ways, as API proxy server or as MCP. If going with the proxy server route, the easiest would be to first try the demo server by following https://github.com/GasStationManager/LeanTool?tab=readme-ov-file#api-server-demo

[Jared green]

what do i do to run it as mcp? the site doesnt tell me.

[GasStationManager]

First set up your LLM normally in roo code; e.g. anthropic with your API key.
Then, set up leantool MCP server. For a quick start, you can use the demo/testing server at http://www.codeproofarena.com:8008/sse
(so no set up required at this step).
Then, set up roo code's connection to the MCP server. See https://docs.roocode.com/features/mcp/using-mcp-in-roo under "SSE". Basically fill in the server address in the config file provided, e.g.

{
  "mcpServers": {
    "remote-server": {
      "url": "http://www.codeproofarena.com:8008/sse"
    }
  }
}

[Jared green]

what about a local mcp server connecting to a remote model

[GasStationManager]

Local MCP server: First install and set up LeanTool by following the steps at https://github.com/GasStationManager/LeanTool?tab=readme-ov-file#installation
(except the last step; you'll set up the LLM in roo code)
Then, to deploy the MCP server in SSE mode, run in the command line poetry run python leanmcp.py --sse --port 8008 and then put the URL http://localhost:8008/sse in roo code's mcp configuration, e.g.

{
  "mcpServers": {
    "remote-server": {
      "url": "http://localhost:8008/sse"
    }
  }
}

[Jared green]

what would that line be if poetry was installed via pip?

[Jared green]

and do i have to do that every time i turn on my computer?

[GasStationManager]

Jared green said:

what would that line be if poetry was installed via pip?

I'm not too familiar with that myself. Going by the poetry documentation at https://python-poetry.org/docs/#installing-manually
if you installed poetry via pip into a venv as the doc suggested, then you can invoke poetry by $VENV_PATH/bin/poetry where $VENV_PATH is where you put the venv at.

[Jared green]

apparently just cd <path-to-leantool>; python -m poetry run python leanmcp.py --sse --port 8008
however im getting
PS C:\Users\jared\AppData\Roaming\Roo-Code\MCP\LeanTool> python -m poetry run python leanmcp.py --sse --port 8008
Traceback (most recent call last):
File "C:\Users\jared\AppData\Roaming\Roo-Code\MCP\LeanTool\leanmcp.py", line 1, in <module>
from mcp.server.fastmcp import FastMCP
ModuleNotFoundError: No module named 'mcp'

[GasStationManager]

poetry is the package manager that LeanTool uses to install its python dependencies. So in the LeanTool installation instructions https://github.com/GasStationManager/LeanTool?tab=readme-ov-file#installation
one of the steps is to do poetry install in the LeanTool directory. (This would read the config file pyproject.toml which tells poetry to install the mcp library among others.)
Did you go through those installation steps?

[Jared green]

yes

[Jared green]

the list of things it installed does not have mcp

[Jared green]

is the fact it didnt install mcp a windows only thing? i tried installing it separately but that didnt work.(i dont know the line for getting it in the same environment)