Constants controlling LeanDojo’s behaviors. Many of them are configurable via Environment Variables.

lean_dojo.constants.CACHE_DIR = PosixPath('/home/docs/.cache/lean_dojo')

Cache directory for storing traced repos (see Caching).

lean_dojo.constants.CONTAINER = 'native'

Container to use for running LeanDojo. Default to native but also support docker. Using docker is recommended for Lean 3.

lean_dojo.constants.DISABLE_REMOTE_CACHE = False

Whether to disable remote caching (see Caching) and build all repos locally.

lean_dojo.constants.GITHUB_ACCESS_TOKEN = None

GiHub personal access token is optional. If provided, it can increase the rate limit for GitHub API calls.

lean_dojo.constants.LEAN3_PACKAGES_DIR = PosixPath('_target/deps')

The directory where Lean 3 dependencies are stored.

lean_dojo.constants.LEAN3_URL = 'https://github.com/leanprover-community/lean'

The URL of the Lean 3 repo.

lean_dojo.constants.LEAN4_NIGHTLY_REPO = Repository(full_name="leanprover/lean4-nightly")

The GitHub Repo for Lean 4 nightly releases.

lean_dojo.constants.LEAN4_PACKAGES_DIR = PosixPath('.lake/packages')

The directory where Lean 4 dependencies are stored (since v4.3.0-rc2).

lean_dojo.constants.LEAN4_PACKAGES_DIR_OLD = PosixPath('lake-packages')

The directory where Lean 4 dependencies are stored (before v4.3.0-rc2).

lean_dojo.constants.LEAN4_REPO = Repository(full_name="leanprover/lean4")

The GitHub Repo for Lean 4 itself.

lean_dojo.constants.LEAN4_URL = 'https://github.com/leanprover/lean4'

The URL of the Lean 4 repo.

lean_dojo.constants.LOAD_USED_PACKAGES_ONLY = False

Only load depdendency files that are actually used by the target repo.

lean_dojo.constants.MIN_LEAN3_VERSION = 'v3.42.1'

The minimum version of Lean 3 that LeanDojo supports.

lean_dojo.constants.NUM_PROCS = 2

Number of threads to use

lean_dojo.constants.REMOTE_CACHE_URL = 'https://lean-dojo.s3.amazonaws.com'

URL of the remote cache (see Caching).

lean_dojo.constants.TACTIC_CPU_LIMIT = 1

Number of CPUs for executing tactics when interacting with Lean (only useful when running within Docker).

lean_dojo.constants.TACTIC_MEMORY_LIMIT = '32g'

Maximum memory when interacting with Lean (only useful when running within Docker).

lean_dojo.constants.TACTIC_TIMEOUT = 5000

Maximum time (in milliseconds) before interrupting a tactic when interacting with Lean (only for Lean 3).

lean_dojo.constants.TMP_DIR = None

Temporary directory used by LeanDojo for storing intermediate files

lean_dojo.constants.check_git_version(min_version: Tuple[int, int, int]) Tuple[int, int, int][source]

Check the version of Git installed on the system.