.env.template

# Docker/launch args
# ==================

# self-explanatory
BLV_VERSION=0.3.3
LEAN_VERSION=v4.24.0

# Path to Lean project on your machine (optional). Useful if you're processing
# theorems with additional dependencies other than just mathlib.
# **IMPORTANT:** If you set a PROJECT_PATH, make sure you also uncomment
#                BLV_PROJECT_PATH, and mount $PROJECT_PATH:$BLV_PROJECT_PATH in
#                the compose.yaml file 

# PROJECT_PATH=
# BLV_PROJECT_PATH=/project

# Number of REPL instances to have at once. More is faster, but
# will also consume more memory if you're loading big libraries like Mathlib.
N_WORKERS=10
            

# Which Redis DB to launch workers on. 0 is default, but if you use Redis for
# something else and you don't want the data from that DB to be flushed, you
# can set this to something else. You should also then set `redis_db=...` in
# `blv.verify_theorems` when you use it.
REDIS_DB=0


# You can customize the default imports for the workers, comma separated.
BLV_IMPORTS="import Mathlib,import Aesop"