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.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 processes to use
- lean_dojo.constants.REMOTE_CACHE_URL = 'https://dl.fbaipublicfiles.com/lean-dojo'
URL of the remote cache (see Caching).
- lean_dojo.constants.TACTIC_CPU_LIMIT = 1
Number of CPUs for executing tactics when interacting with Lean.
- lean_dojo.constants.TACTIC_MEMORY_LIMIT = '32g'
Maximum memory when interacting with Lean.
- lean_dojo.constants.TMP_DIR = None
Temporary directory used by LeanDojo for storing intermediate files