Skip to content

Conversation

@oOo0oOo
Copy link

@oOo0oOo oOo0oOo commented Apr 4, 2025

Description

This PR adds the lean-lsp-mcp server to the list in the README.md. This MCP server allows interaction with the Lean theorem prover via the Language Server Protocol.

Types of changes

  • Bug fix (non-breaking change which fixes an issue)
  • New feature (non-breaking change which adds functionality)
  • Breaking change (fix or feature that would cause existing functionality to change)
  • Documentation update

Checklist

  • I have read the MCP Protocol Documentation
  • My changes follows MCP security best practices
  • I have updated the server's README accordingly
  • I have tested this with an LLM client
  • My code follows the repository's style guidelines
  • New and existing tests pass locally
  • I have added appropriate error handling
  • I have documented all environment variables and configuration options

Copy link
Member

@olaservo olaservo left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hi, could you resolve the conflicts? Thanks!

@olaservo olaservo added the waiting for submitter Waiting for the submitter to provide more info label May 29, 2025
@olaservo
Copy link
Member

olaservo commented Jun 9, 2025

Thanks for your contribution to the servers list. This has been merged in this combined PR: #2007

This is a new process we're trying out, so if you see any issues feel free to re-open the PR and tag me.

@olaservo olaservo closed this Jun 9, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

waiting for submitter Waiting for the submitter to provide more info

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants