|
| 1 | +<!-- SPDX-License-Identifier: MPL-2.0 --> |
| 2 | +<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> --> |
| 3 | + |
| 4 | +# ECHIDNA Environment Variables |
| 5 | + |
| 6 | +**Status**: canonical reference. Last revised: 2026-05-26. |
| 7 | + |
| 8 | +Every environment variable the system reads, with type, default, and the |
| 9 | +files that consume it. If you add a new env var, update this table in the |
| 10 | +same PR. |
| 11 | + |
| 12 | +## Core runtime |
| 13 | + |
| 14 | +| Variable | Type | Default | Used by | Purpose | |
| 15 | +|---|---|---|---|---| |
| 16 | +| `ECHIDNA_ML_API_URL` | URL | `http://127.0.0.1:8090` | `src/rust/server.rs:71` | Julia ML sidecar HTTP endpoint (GNN, suggest, training/update) | |
| 17 | +| `VERISIM_URL` | URL | `http://localhost:8080` | `src/rust/dispatch.rs`, `src/rust/learning/daemon.rs`, `src/julia/retrain_from_verisim.jl` | VeriSimDB REST endpoint for proof-attempt writes and history reads. **Canonical name** — older surfaces using `VERISIMDB_URL` are stale and being migrated. | |
| 18 | +| `ECHIDNA_GNN_URL` | URL | falls back to `ECHIDNA_ML_API_URL` | (planned C5 — see Stage 3c fix list) | Specifically the GNN endpoint; separate from the ML server only when the GNN runs on a different host. | |
| 19 | + |
| 20 | +## Training & evaluation (Julia) |
| 21 | + |
| 22 | +| Variable | Type | Default | Used by | Purpose | |
| 23 | +|---|---|---|---|---| |
| 24 | +| `ECHIDNA_MAX_PROOF_STATES` | int | 0 (all) | `src/julia/run_training.jl`, `run_training_cpu.jl` | Cap corpus size for fast smoke runs. `just train-cpu` sets this to 2000. | |
| 25 | +| `ECHIDNA_NUM_EPOCHS` | int | implementation default | same | Number of training epochs. `just train-cpu` sets this to 2. | |
| 26 | +| `ECHIDNA_NUM_NEGATIVES` | int | 20 | same | Negative-sample count per training step. | |
| 27 | +| `ECHIDNA_MODELS_DIR` | path | `models/` | `src/julia/api/server.jl`, `src/julia/eval_held_out.jl` | Where trained Flux model artefacts live. | |
| 28 | + |
| 29 | +## CI & supply-chain |
| 30 | + |
| 31 | +| Variable | Type | Default | Used by | Purpose | |
| 32 | +|---|---|---|---|---| |
| 33 | +| `FARM_DISPATCH_TOKEN` | secret | unset | `.github/workflows/instant-sync.yml` | Push notifications to dependent forks. | |
| 34 | +| `VERISIMDB_PAT` | secret | unset | `.github/workflows/security-scan.yml` | Reusable panic-attack workflow auth. Note: name is `VERISIMDB_PAT` not `VERISIM_PAT` — secret-name compatibility with upstream. | |
| 35 | + |
| 36 | +## Build flags (not env vars but related) |
| 37 | + |
| 38 | +| Cargo feature | Default? | Enables | |
| 39 | +|---|---|---| |
| 40 | +| `verisim` | no (target: yes after Stage 3c C4 lands) | VeriSimDB writer + advisor + entity-type emission | |
| 41 | +| `chapel` | no | Chapel parallel-search bridge via Zig FFI shim | |
| 42 | + |
| 43 | +## Container & secrets |
| 44 | + |
| 45 | +In `.containerization/Containerfile.full`, the following are expected to be |
| 46 | +mounted or built into the image rather than passed as env: |
| 47 | + |
| 48 | +- Solver binaries — paths in `config/solver-manifest.toml` (with SHAKE3-512 hashes) |
| 49 | +- Guix manifest — `manifests/live-provers.scm` |
| 50 | +- TLS material — none in default container; HTTPS terminated by reverse proxy |
| 51 | + |
| 52 | +## Deprecated / soon-removed |
| 53 | + |
| 54 | +| Variable | Note | |
| 55 | +|---|---| |
| 56 | +| `VERISIMDB_URL` | Old name for `VERISIM_URL`. Still read by `tests/live_prover_suite.rs:118` and enforced by `k9iser.toml:47`. Migration tracked in Stage 3c fix C3. | |
| 57 | + |
| 58 | +## Reading order for new contributors |
| 59 | + |
| 60 | +1. Set `ECHIDNA_ML_API_URL` and `VERISIM_URL` for any local dev session that |
| 61 | + touches dispatch or ML paths. |
| 62 | +2. Set the `ECHIDNA_*` training caps only when running `just train-cpu` or |
| 63 | + `just eval` on a constrained host. |
| 64 | +3. CI secrets (`FARM_DISPATCH_TOKEN`, `VERISIMDB_PAT`) are repository-level — |
| 65 | + no local action needed. |
0 commit comments