lean_dojo.constants

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.LEAN4_PACKAGES_DIR = PosixPath('.lake/packages')

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

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.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.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]

Check the version of Git installed on the system.