Commit 6feec89
ci(server): server boot gate — convert 'compiles' into 'boots' (#258)
## Summary
- Adds `.github/workflows/server-boot-gate.yml`: builds the binary,
starts `echidna server`, curls `/api/health`, `/api/provers`, and a
session `{id}` route on every push/PR to `main`.
The axum 0.8 route-panic shipped because nothing in CI started the
server. This gate permanently closes that gap.
## What's NOT in this PR (blockers)
Three additional fixes from the close-out work order are **ready but
blocked** by pre-existing SPDX header drift on the affected source
files. The pre-commit hook checks every staged `.rs` / `.adoc` file for
`Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>` and rejects files that
have:
| File | Current header (wrong) | Needed |
|------|------------------------|--------|
| `src/rust/server.rs` | `2025 ECHIDNA Project Team` | `2025 Jonathan
D.A. Jewell <j.d.a.jewell@open.ac.uk>` |
| `src/interfaces/rest/main.rs` | (no SPDX-FileCopyrightText at all) |
add one |
| `QUICKSTART-USER.adoc` | `Copyright (c) 2026 Jonathan D.A. Jewell
(hyperpolymath) <j.d.a.jewell@open.ac.uk>` | remove `(hyperpolymath)`
from between name and `<` |
Once you fix those three headers manually, the following changes are
ready to commit (diffs saved to
`~/dev-notes/echidna-closeout-patches/`):
1. **QUICKSTART demo fix** (task 1c): replace `(assert (> x 0))`
(satisfiable, always returns `success:false`) with `(assert (and (> x 0)
(< x 0)))` → unsat → `success:true`.
2. **VeriSim wiring** (task 3): attach
`with_verisim_writer(VERISIM_URL)` to the dispatcher at startup; route
`prove_handler` through `dispatcher.verify_proof()` when compiled
`--features verisim`.
## Note on Task 1a (route syntax)
The axum 0.8 `{id}` route syntax is **already correct** in `origin/main`
— the routes were `{id}`-style before the bump landed. The boot-gate
will now permanently verify this on every PR.
## Test plan
- [ ] Merge this PR; verify `Server Boot Gate` CI job passes
- [ ] Apply the SPDX header fixes to the three files above (manual)
- [ ] Apply the QUICKSTART demo patch
- [ ] Apply the VeriSim wiring patch and open `feat/verisim-prove-path`
PR
Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>1 parent 147d6b4 commit 6feec89
1 file changed
Lines changed: 72 additions & 0 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
| 11 | + | |
| 12 | + | |
| 13 | + | |
| 14 | + | |
| 15 | + | |
| 16 | + | |
| 17 | + | |
| 18 | + | |
| 19 | + | |
| 20 | + | |
| 21 | + | |
| 22 | + | |
| 23 | + | |
| 24 | + | |
| 25 | + | |
| 26 | + | |
| 27 | + | |
| 28 | + | |
| 29 | + | |
| 30 | + | |
| 31 | + | |
| 32 | + | |
| 33 | + | |
| 34 | + | |
| 35 | + | |
| 36 | + | |
| 37 | + | |
| 38 | + | |
| 39 | + | |
| 40 | + | |
| 41 | + | |
| 42 | + | |
| 43 | + | |
| 44 | + | |
| 45 | + | |
| 46 | + | |
| 47 | + | |
| 48 | + | |
| 49 | + | |
| 50 | + | |
| 51 | + | |
| 52 | + | |
| 53 | + | |
| 54 | + | |
| 55 | + | |
| 56 | + | |
| 57 | + | |
| 58 | + | |
| 59 | + | |
| 60 | + | |
| 61 | + | |
| 62 | + | |
| 63 | + | |
| 64 | + | |
| 65 | + | |
| 66 | + | |
| 67 | + | |
| 68 | + | |
| 69 | + | |
| 70 | + | |
| 71 | + | |
| 72 | + | |
0 commit comments