|
1 | | -;; SPDX-License-Identifier: PMPL-1.0-or-later |
2 | | -;; STATE.scm - Project state for echidnabot |
3 | | -;; Media-Type: application/vnd.state+scm |
4 | | - |
5 | | -(state |
6 | | - (metadata |
7 | | - (version "0.0.1") |
8 | | - (schema-version "1.0") |
9 | | - (created "2026-01-03") |
10 | | - (updated "2026-01-03") |
11 | | - (project "echidnabot") |
12 | | - (repo "github.com/hyperpolymath/echidnabot")) |
13 | | - |
14 | | - (project-context |
15 | | - (name "echidnabot") |
16 | | - (tagline "") |
17 | | - (tech-stack ())) |
18 | | - |
19 | | - (current-position |
20 | | - (phase "initial") |
21 | | - (overall-completion 0) |
22 | | - (components ()) |
23 | | - (working-features ())) |
24 | | - |
25 | | - (route-to-mvp |
26 | | - (milestones ())) |
27 | | - |
28 | | - (blockers-and-issues |
29 | | - (critical) |
30 | | - (high) |
31 | | - (medium) |
32 | | - (low)) |
33 | | - |
34 | | - (critical-next-actions |
35 | | - (immediate) |
36 | | - (this-week) |
37 | | - (this-month)) |
38 | | - |
39 | | - (session-history ())) |
| 1 | +# SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | +# |
| 4 | +# STATE.a2ml — Echidnabot project state |
| 5 | + |
| 6 | +[metadata] |
| 7 | +project = "echidnabot" |
| 8 | +version = "0.1.0" |
| 9 | +last-updated = "2026-04-11" |
| 10 | +status = "active" |
| 11 | +session = "VeriSimDB coupling + dogfood run — 2026-04-11" |
| 12 | + |
| 13 | +[project-context] |
| 14 | +name = "Echidnabot" |
| 15 | +purpose = """ |
| 16 | +Proof-aware CI bot for theorem prover repositories. Calls ECHIDNA Core |
| 17 | +to verify proof files, records every attempt (success + failure) to |
| 18 | +VeriSimDB via the VeriSimWriter adapter, and feeds the Hypatia learning |
| 19 | +loop through the proof_attempts ClickHouse table. |
| 20 | +""" |
| 21 | +completion-percentage = 72 |
| 22 | + |
| 23 | +[position] |
| 24 | +phase = "implementation" # design | implementation | testing | maintenance | archived |
| 25 | +maturity = "alpha" # experimental | alpha | beta | production | lts |
| 26 | + |
| 27 | +[route-to-mvp] |
| 28 | +milestones = [ |
| 29 | + { id = "M1", title = "Core prover dispatch (48 provers)", status = "done" }, |
| 30 | + { id = "M2", title = "VeriSimWriter — proof_attempts recording", status = "done" }, |
| 31 | + { id = "M3", title = "check --slug for ad-hoc dogfood runs", status = "done" }, |
| 32 | + { id = "M4", title = "Webhook server + scheduler", status = "done" }, |
| 33 | + { id = "M5", title = "Register/check/status CLI commands", status = "done" }, |
| 34 | + { id = "M6", title = "GitHub / GitLab / Bitbucket adapters", status = "in-progress" }, |
| 35 | + { id = "M7", title = "Production hardening (retry, backoff, circuit-break)", status = "planned" }, |
| 36 | + { id = "M8", title = "Prover availability detection (not just status)", status = "planned" }, |
| 37 | +] |
| 38 | + |
| 39 | +[blockers-and-issues] |
| 40 | +issues = [ |
| 41 | + { id = "B1", description = "Agda/Coq/Isabelle provers report status=unavailable when not installed locally; proof attempts write failure rows correctly but classification could be improved", severity = "low" }, |
| 42 | + { id = "B2", description = "GitHub adapter not yet wired with real webhook signing validation", severity = "medium" }, |
| 43 | +] |
| 44 | + |
| 45 | +[critical-next-actions] |
| 46 | +actions = [ |
| 47 | + "Wire GitHub PAT for production webhook dispatch", |
| 48 | + "Add prover-not-installed vs proof-failed distinction in outcome classification", |
| 49 | + "Test process_job path end-to-end with a real GitHub webhook", |
| 50 | +] |
| 51 | + |
| 52 | +[session-history] |
| 53 | +# 2026-04-11: VeriSimDB coupling complete. VeriSimWriter records every verify_proof |
| 54 | +# result to POST /api/v1/proof_attempts (ClickHouse via verisim-api). |
| 55 | +# Fixed timestamp format to DateTime64(3) without Z suffix. |
| 56 | +# Added --slug flag to check command so ad-hoc file checks also populate |
| 57 | +# proof_attempts. Dogfood run: 4 echidna proof files verified, all rows |
| 58 | +# landed in ClickHouse (lean=success, agda/coq=failure, correct timestamps). |
| 59 | +# 2026-04-05: V4 coupling: VeriSimWriter stub present but not wired into process_job. |
| 60 | +# echidnabot compiles, 0 clippy warnings. |
| 61 | + |
| 62 | +[maintenance-status] |
| 63 | +last-run-utc = "2026-04-11T17:11:17Z" |
| 64 | +last-result = "pass" |
0 commit comments