diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 4853400..b0a7616 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -30,7 +30,7 @@ milestones = [ { name = "Content-hash invalidation of proven (file-level + transitive-import closure via [proven] include_root)", completion = 100 }, { name = "Operator config (.arghda/config.toml + --headline-pattern + --config)", completion = 100 }, { name = "RSR / standards alignment (.machine_readable, README.adoc, EXPLAINME, LICENSE, .well-known)", completion = 100 }, - { name = "Groove service manifest (/.well-known/groove) for PanLL discovery", completion = 0 }, + { name = "Groove service manifest (/.well-known/groove) for PanLL discovery", completion = 100 }, ] # "Flying Logic for provers/solvers" epic (v0.2+): generalise the Agda-only @@ -51,7 +51,7 @@ milestones = [ { name = "M8: Coq/Rocq adapter (--heavy provisioning; Section-aware postulate classifier)", completion = 0 }, { name = "M9: Isabelle adapter (--heavy; dogfood tropical-resource-typing .thy)", completion = 0 }, { name = "M10: Mizar adapter (detect-only first; highest uncertainty)", completion = 0 }, - { name = "M11: studio JSON freeze (reason/0.1) + Groove manifest", completion = 0 }, + { name = "M11: studio JSON freeze (reason/0.1) + Groove manifest", completion = 100 }, ] # M0 provisioning verified in-container 2026-07-01: agda 2.6.3 (+stdlib v2.3 # +cubical lib), zig 0.15.2, z3 4.8.12, cvc5 1.2.0, lean 4.13.0 all report @@ -60,6 +60,22 @@ milestones = [ # Remaining M0: `arghda doctor` Rust subcommand (interim: `just doctor` shells # the script's --verify-only table). # +# M11 landed 2026-07-01: studio JSON freeze (reason/0.1) + Groove manifest — +# closes the ONE open v0.1 milestone (Groove service manifest, was 0%). Two +# deliverables. (1) Studio JSON freeze: a reason/0.1 JSON CONTRACT test in +# src/reason/mod.rs pins the top-level (version/dag/nodes/edges/crt_roots) + +# per-node (id/self_verdict/effective/verdict_evidence/soundness/wired) + +# per-edge (from/to/junct/kind) keys — a rename now breaks a test (bump the +# version, don't silently edit). (2) Groove: src/groove.rs `GrooveManifest` +# (groove 0.1; service/description; capabilities = live backend probes + +# commands + frozen schemas dag/0.1+reason/0.1). `arghda groove [--output +# ]` emits it (stdout, or writes a `/.well-known/groove` file, creating +# parent dirs). arghda-core is a CLI so it EMITS the manifest; serving it over +# HTTP is the host's (PanLL's) job — honest. Backends probed live so the +# manifest reflects this machine. 121 tests (88 lib + 33 integration; +1 groove +# unit +1 reason-contract-freeze unit). Dogfooded: `arghda groove` → all 6 +# backends runnable, schemas 0.1; `--output` wrote /.well-known/groove. +# # M6 landed 2026-07-01 (85%): the Lean4 backend — sixth backend. src/prover/ # lean.rs: `lean ` elaboration. The honesty subtlety Lean forces: a green # exit does NOT mean proven (sorry is only a warning; exit 0). So the verdict is @@ -184,10 +200,9 @@ milestones = [ [critical-next-actions] actions = [ - "M0-M6 DONE. SIX backends (agda, agda-cubical, idris2, lean4 Assistant; z3, cvc5 Solver) + reasoning graph + doctor. Engine spine essentially complete. Next:", - "Flying-Logic epic M11: studio JSON freeze (reason/0.1) + Groove /.well-known/groove manifest (the one open v0.1 milestone; `arghda doctor` output feeds the manifest).", - "Flying-Logic epic M7: Echidna dispatch seam (feature-gated client, same Outcome).", - "M6 follow-on (15%): lake-env/LEAN_PATH multi-file resolution; per-decl #print axioms audit to promote Unknown→Proven.", + "M0-M6 + M11 DONE. The v0.1 spec is now CLOSED (Groove manifest was the last open milestone). Engine-spine deliverable (M0-M7 + M11) is complete bar M7. Six backends + reasoning graph + doctor + groove. Remaining:", + "Flying-Logic epic M7: Echidna dispatch seam (feature-gated client, same Outcome) — completes the engine-spine deliverable.", + "M6 follow-on: lake-env/LEAN_PATH multi-file resolution; per-decl #print axioms audit to promote Unknown→Proven.", "M4 follow-on: .ipkg-declared roots; totality-hole (?name) + per-def `partial` lint.", "M3 follow-on: feed real verdicts into `reason` from a workspace `proven/` state + wire staleness from the content-hash closure (proven.rs).", "M8-M10 heavy tail (Coq/Rocq, Isabelle, Mizar) — gated on --heavy provisioning.", @@ -199,10 +214,11 @@ last-result = "pass" # unknown | pass | warn | fail open-warnings = 0 open-failures = 0 # `just check` (fmt-check + clippy -D warnings + build + test + SPDX) green -# post-M6: 86 lib + 33 integration = 119 tests pass. `arghda doctor` dogfooded: -# 6/6 backends runnable. All six dogfooded via real CLI: agda + agda-cubical + -# idris2 + lean4 (Assistant), z3 + cvc5 (Solver). Dogfooded historically against -# echo-types + agda-unused. +# post-M11: 88 lib + 33 integration = 121 tests pass. `arghda doctor`/`groove` +# dogfooded: 6/6 backends runnable; manifest emits + writes /.well-known/groove. +# All six backends dogfooded via real CLI: agda + agda-cubical + idris2 + lean4 +# (Assistant), z3 + cvc5 (Solver). Dogfooded historically vs echo-types + +# agda-unused. [ecosystem] part-of = ["arghda"] diff --git a/src/groove.rs b/src/groove.rs new file mode 100644 index 0000000..902753d --- /dev/null +++ b/src/groove.rs @@ -0,0 +1,98 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! Groove service-discovery manifest. +//! +//! Groove is the estate's HTTP-based service-discovery protocol: a capability +//! provider publishes a manifest at `/.well-known/groove` so consumers (e.g. +//! PanLL) can auto-detect it and wire it in without manual configuration. +//! +//! arghda-core is a CLI, not a server, so it *emits* the manifest (`arghda +//! groove`) as JSON; serving it over HTTP at `/.well-known/groove` is the +//! host's job (a web server, or the PanLL shell). Backend availability is +//! probed live, so the manifest reflects what this machine can actually run — +//! honest discovery, not a static advertisement. +//! +//! This is arghda's v0.1 manifest shape (`groove: "0.1"`); it announces the +//! two frozen JSON schemas the visual layer consumes (`dag/0.1`, +//! `reason/0.1`), the CLI commands, and the probed backends. + +use crate::prover::Probe; +use serde::Serialize; + +/// The JSON-contract schema versions the visual layer (arghda-studio) and +/// PanLL consume. Frozen — bump only on a breaking change. +#[derive(Clone, Debug, Serialize)] +pub struct Schemas { + pub dag: &'static str, + pub reason: &'static str, +} + +/// What arghda announces it can do. +#[derive(Clone, Debug, Serialize)] +pub struct Capabilities { + /// Live probe of each known backend (id, kind, runnable, detail). + pub backends: Vec, + /// The CLI verbs a consumer can drive. + pub commands: Vec<&'static str>, + /// The frozen output-schema versions. + pub schemas: Schemas, +} + +/// The `/.well-known/groove` manifest for arghda. +#[derive(Clone, Debug, Serialize)] +pub struct GrooveManifest { + /// Groove manifest-schema version. + pub groove: &'static str, + pub service: &'static str, + pub description: &'static str, + pub capabilities: Capabilities, +} + +/// Build the manifest from live backend probes. +pub fn manifest(backends: Vec) -> GrooveManifest { + GrooveManifest { + groove: "0.1", + service: "arghda", + description: "proof-workspace manager for provers and solvers", + capabilities: Capabilities { + backends, + commands: vec!["scan", "check", "dag", "reason", "doctor", "groove"], + schemas: Schemas { + dag: "0.1", + reason: "0.1", + }, + }, + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::prover::BackendKind; + + fn probe(name: &str) -> Probe { + Probe { + backend: name.to_string(), + kind: BackendKind::Assistant, + runnable: true, + detail: "v1".to_string(), + } + } + + #[test] + fn manifest_announces_frozen_schemas_and_backends() { + let m = manifest(vec![probe("agda"), probe("lean4")]); + assert_eq!(m.groove, "0.1"); + assert_eq!(m.service, "arghda"); + assert_eq!(m.capabilities.schemas.dag, "0.1"); + assert_eq!(m.capabilities.schemas.reason, "0.1"); + assert_eq!(m.capabilities.backends.len(), 2); + assert!(m.capabilities.commands.contains(&"reason")); + // It serialises to the expected discovery shape. + let v = serde_json::to_value(&m).unwrap(); + assert_eq!(v["groove"], "0.1"); + assert_eq!(v["capabilities"]["schemas"]["reason"], "0.1"); + assert_eq!(v["capabilities"]["backends"][0]["backend"], "agda"); + } +} diff --git a/src/lib.rs b/src/lib.rs index 7d103bf..55285b0 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -15,6 +15,7 @@ pub mod dag; pub mod diagnostic; pub mod event; pub mod graph; +pub mod groove; pub mod hash; pub mod lint; pub mod proven; @@ -29,6 +30,7 @@ pub use dag::{build as build_dag, DagDocument}; pub use diagnostic::{Diagnostic, LintReport, Severity}; pub use event::{Event, EventKind}; pub use graph::{build as build_graph, ImportGraph}; +pub use groove::{manifest as groove_manifest, GrooveManifest}; pub use lint::{default_rules, rules_with_config, run_lints, LintRule, RuleConfig}; pub use prover::{ default_backend, Agda, AgdaCubical, Backend, BackendKind, Idris2, Lean, Outcome, Probe, Smt, diff --git a/src/main.rs b/src/main.rs index daa8d44..6ef03ad 100644 --- a/src/main.rs +++ b/src/main.rs @@ -4,8 +4,9 @@ use anyhow::{Context, Result}; use arghda_core::lint::LintContext; use arghda_core::{ - build_dag, build_reason, event, run_lints, unused, watcher, Agda, AgdaCubical, Backend, - BackendKind, Idris2, Lean, LintRule, RuleConfig, Smt, State, Verdict, Workspace, + build_dag, build_reason, event, groove_manifest, run_lints, unused, watcher, Agda, AgdaCubical, + Backend, BackendKind, Idris2, Lean, LintRule, Probe, RuleConfig, Smt, State, Verdict, + Workspace, }; use clap::{Parser, Subcommand}; use std::path::{Path, PathBuf}; @@ -170,6 +171,15 @@ enum Cmd { #[arg(long)] json: bool, }, + /// Emit the Groove service-discovery manifest (`/.well-known/groove`). + /// Announces arghda's capabilities (probed backends, CLI commands, and + /// the frozen `dag/0.1` + `reason/0.1` schemas) for PanLL discovery. + Groove { + /// Write the manifest to a file instead of stdout (e.g. + /// `/.well-known/groove`). + #[arg(long)] + output: Option, + }, } fn main() -> Result<()> { @@ -252,16 +262,41 @@ fn main() -> Result<()> { } => stale(&workspace, invalidate)?, Cmd::Watch { workspace } => watch(&workspace)?, Cmd::Doctor { json } => doctor(json)?, + Cmd::Groove { output } => groove(output.as_deref())?, } Ok(()) } -/// Probe every known backend and report which are actually runnable. -fn doctor(json: bool) -> Result<()> { - let probes = KNOWN_BACKENDS +/// Probe every known backend for runnability (shared by `doctor`/`groove`). +fn probe_all() -> Result> { + KNOWN_BACKENDS .iter() .map(|name| backend_for(name).map(|b| b.probe())) - .collect::>>()?; + .collect() +} + +/// Emit the Groove service-discovery manifest (stdout, or `--output` file). +fn groove(output: Option<&Path>) -> Result<()> { + let manifest = groove_manifest(probe_all()?); + let json = serde_json::to_string_pretty(&manifest)?; + match output { + Some(path) => { + if let Some(parent) = path.parent() { + std::fs::create_dir_all(parent) + .with_context(|| format!("creating {}", parent.display()))?; + } + std::fs::write(path, format!("{json}\n")) + .with_context(|| format!("writing {}", path.display()))?; + println!("wrote Groove manifest to {}", path.display()); + } + None => println!("{json}"), + } + Ok(()) +} + +/// Probe every known backend and report which are actually runnable. +fn doctor(json: bool) -> Result<()> { + let probes = probe_all()?; if json { let payload = serde_json::json!({ "version": "0.1", "backends": probes }); diff --git a/src/reason/mod.rs b/src/reason/mod.rs index d1fd71f..3ce724e 100644 --- a/src/reason/mod.rs +++ b/src/reason/mod.rs @@ -531,4 +531,65 @@ mod tests { assert!(wired.contains("Deep")); assert!(!wired.contains("Orphan")); } + + // ── reason/0.1 JSON contract freeze (M11) ──────────────────────────── + // The visual layer (arghda-studio) + Groove consumers depend on this + // shape. A rename here is a BREAKING change — bump the version, don't + // silently edit. This test pins the schema so that can't happen by + // accident. + #[test] + fn reason_json_contract_is_frozen_at_0_1() { + use crate::dag::{DagDocument, DagNode, LintSummary}; + use crate::graph::Edge; + use crate::prover::Agda; + use std::path::PathBuf; + + let dag = DagDocument { + version: "0.1", + include_root: PathBuf::from("/r"), + entry_modules: vec![PathBuf::from("/r/All.agda")], + generated_at: "t".to_string(), + nodes: vec![ + DagNode { + id: "All".to_string(), + file: PathBuf::from("All.agda"), + status: "clean", + lint: LintSummary::default(), + headlines: vec![], + }, + DagNode { + id: "Util".to_string(), + file: PathBuf::from("Util.agda"), + status: "clean", + lint: LintSummary::default(), + headlines: vec![], + }, + ], + edges: vec![Edge { + from: "All".to_string(), + to: "Util".to_string(), + kind: "imports", + }], + blocked: vec![], + }; + let doc = build(dag, &Agda, &BTreeMap::new(), &BTreeSet::new()); + let v = serde_json::to_value(&doc).unwrap(); + + assert_eq!(v["version"], "0.1"); + assert!(v["dag"].is_object(), "the DAG is embedded verbatim"); + assert!(v["crt_roots"].is_array()); + for k in [ + "id", + "self_verdict", + "effective", + "verdict_evidence", + "soundness", + "wired", + ] { + assert!(v["nodes"][0].get(k).is_some(), "reason node missing `{k}`"); + } + for k in ["from", "to", "junct", "kind"] { + assert!(v["edges"][0].get(k).is_some(), "reason edge missing `{k}`"); + } + } }