Contributing to LeanInteract

Thank you for contributing to LeanInteract! This guide will help getting started, following best practices, and making contributions easy to review.

Pull Request Guidelines

• Describe changes clearly and concisely in the PR description.
• Link to relevant issues using # (e.g., #42).
• Include tests for new features or bug fixes.
• Update documentation if changes affect usage or APIs.
• Ensure all tests pass before requesting review.

Getting Started

1. Fork the repository on GitHub and clone the fork locally.

2. Install development dependencies: we recommend using uv.

uv pip install -e ".[dev]"

Code Style & Quality

• Type hints: All functions and methods should have type annotations.
• Docstrings: Write clear, descriptive docstrings for all public classes, functions, and modules.
• Tests: All new features and bug fixes must include unit tests.
• Documentation: Update or add documentation as needed.

Testing

• Run all tests:

uv run python -m unittest discover tests

• Run a specific test module:

uv run python -m unittest tests/test_server.py

• First-time setup is slow: Lean toolchain and dependencies may take several minutes to install/compile.
• Concurrency tests timeout: Use generous timeouts and check system resources.

Documentation & Versioning

LeanInteract uses mkdocs and mike for versioned documentation. Documentation is auto-deployed on main branch changes and version tags.

• Preview docs locally:

uv run mkdocs serve

Reporting Issues & Getting Help

Bugs/Feature requests:

1. Check GitHub issues first (open or closed).
2. If new, open an issue with a clear description and steps to reproduce.

Contact: For questions, contact the maintainer.

---

Thank you for contributing to LeanInteract!