CLI and engine
| Variable | Default | Meaning |
|---|---|---|
THEFORMALERA_TOKEN | stored token | Spec Hub API token; takes precedence over theformalera login |
THEFORMALERA_HUB | [project] hub | Hub URL; file://<dir> uses a local mirror |
THEFORMALERA_CACHE | ~/.cache/theformalera | Spec package cache (specs/<digest>) and compiled lemma packs |
THEFORMALERA_MATHLIB | — | A Lake workspace with Mathlib built; spec workspaces reuse its .lake/packages |
THEFORMALERA_SPECS | — | Use this Lean workspace for proof checks instead of the locked package’s; also the spec library used by theformalera-conformance (default specs/) |
THEFORMALERA_ENGINE_URL | — | The on-prem engine endpoint (runner = "on-prem") |
THEFORMALERA_ORG | local-org | Organisation name, for file:// mirrors |
THEFORMALERA_PLAN | enterprise | Plan reported by a file:// mirror |
THEFORMALERA_SIGNING_KEY | .theformalera/signing-key.pem | Release signing key for signoff |
THEFORMALERA_SIGNER_PUBKEY | — | Public key for cert verify |
THEFORMALERA_GUARDS | 1 | Set to 0 to disable the generated runtime guards |
THEFORMALERA_KEEP_CERTS | — | Directory where the engine keeps every generated certificate, including rejected ones (debugging) |
XDG_CONFIG_HOME | ~/.config | Location of theformalera/credentials.json |
Hub API
| Variable | Default | Meaning |
|---|---|---|
THEFORMALERA_HUB_STORE | hub-data | Object store: a directory or s3://bucket/prefix |
THEFORMALERA_HUB_JOBS | jobs in the store directory | DynamoDB table of jobs |
THEFORMALERA_HUB_TOKENS | tokens.json in the store | DynamoDB table of API tokens |
THEFORMALERA_HUB_QUEUE | in-store queue file | SQS queue URL for verification jobs |
THEFORMALERA_HUB_PUBLIC_URL | — | Public URL, for redirects to the website |
Conformance
| Variable | Default | Meaning |
|---|---|---|
THEFORMALERA_SPECS | specs/ of the repository | The Lean spec library and its theformalera-spec executable |
HF_HOME / HF_HUB_CACHE | Hugging Face defaults | Where config.json files and checkpoints are cached |