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]"
.
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 :ref:`code-formatting`).
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.
This documentation is generated by Sphinx. You can build it by:
cd docs && make clean && make html && cd ..
You probably won't need it, but this is how to build the LeanDojo package and upload it to PyPI:
hatch build
hatch publish
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.
LeanDojo's code is formatted by Black. We use Github Actions to ensure all modifications are formatted.