Developer Guide

This page includes information that are hidden from most users but useful if you want to contribute to LeanDojo. It requires additional dependencies installed via pip install "lean-dojo[all]".

Contribution Guideline

We welcome and appreciate contributions from the community. For bug fixes and relatively minor changes (comments, typos, etc.), feel free to submit a pull request directly. For anything more substantial, please first reach out to us before implementing. All contributions should conform to our code formatting standards (see Code Formatting).

Testing

We use pytest for testing. You can run tests by:

VERBOSE=1 CACHE_DIR=~/.cache/lean_dojo_testing DISABLE_REMOTE_CACHE=1 pytest -s tests
rm -rf ~/.cache/lean_dojo_testing

The environment variable CACHE_DIR makes sure the testing uses a temporary cache directory that does not interfere with the deployed code. The temporary cache directory is deleted after the testing completes. DISABLE_REMOTE_CACHE=1 instructs repos to be built locally. Note that running all tests can take almost 1 day on 32 CPUs.

Building the Documentation

This documentation is generated by Sphinx. You can build it by:

cd docs && make clean && make html && cd ..

Building the Package and Uploading to PyPI

You probably won’t need it, but this is how to build the LeanDojo package and upload it to PyPI:

hatch build
hatch publish

Static Type Checking

The source code of LeanDojo uses Python type annotations extensively. You can perform static type checking using mypy by

mypy src/lean_dojo

Currently there are still many type errors. Contributions to fix them are welcome.

Code Formatting

LeanDojo’s code is formatted by Black. We use Github Actions to ensure all modifications are formatted.