Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions crates/supermath-mcp/src/cli/hive/mod.rs
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
//! `supermath-mcp hive-tools`: the toolkit as tinyhivemind executable tools.
//!
//! An `rsi-ralph` hive package declares the programs its seats may call in
//! the `tools` array of `hive.json` (tinyhivemind's
//! `docs/specs/executable-tools.md`). This module writes one declaration per
//! the `tools` array of its manifest, kept in `tools.json` in the loops
//! `loop new` writes (tinyhivemind's `docs/specs/executable-tools.md`). This module writes one declaration per
//! registered tool, straight from the tool's own name, description, schema,
//! and permission, so the package cannot drift from the code:
//!
Expand Down
38 changes: 25 additions & 13 deletions crates/supermath-mcp/src/cli/scaffold/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,19 @@
//! ```text
//! <loop>/rsi.json the subject, hive, scorer, models, budget
//! <loop>/brief.md the conjecture and the epoch's task
//! <loop>/hive/ lead, prover, refuter; the toolkit as tools
//! <loop>/hive/hive.json identity, context, policies, coordinator
//! <loop>/hive/agents.json roles and seats: lead, prover, refuter
//! <loop>/hive/desks.json the desk the seats share
//! <loop>/hive/tools.json the toolkit as tools and toolpacks
//! <loop>/subject/lean/Supermath/Statement.lean the conjecture, frozen
//! <loop>/subject/lean/Supermath/Prove.lean `theorem proof : Conjecture`
//! <loop>/subject/lean/Supermath/Refute.lean `theorem refute : ¬ Conjecture`
//! ```
//!
//! The statement file must declare `Supermath.Conjecture : Prop`; it is
//! copied in verbatim. `hive.json` gets one executable tool per toolkit tool
//! copied in verbatim. The hive's manifest is split the way tinyhivemind
//! allows, so no one file grows large. `tools.json` gets one executable tool
//! per toolkit tool
//! (see [`declarations`]), less the `file_*` tools,
//! whose work the seats' own file tools do in their checkout, and
//! `web_search`, whose name `OpenHuman`'s own search tool has; and one toolpack per
Expand All @@ -32,13 +37,21 @@ use super::hive::{Program, declarations};
use crate::error::{Error, Result};

/// The template, as (path in the loop folder, text) pairs.
const TEMPLATE: [(&str, &str); 17] = [
const TEMPLATE: [(&str, &str); 19] = [
("rsi.json", include_str!("../../../template/rsi.json")),
("brief.md", include_str!("../../../template/brief.md")),
(
"hive/hive.json",
include_str!("../../../template/hive/hive.json"),
),
(
"hive/agents.json",
include_str!("../../../template/hive/agents.json"),
),
(
"hive/desks.json",
include_str!("../../../template/hive/desks.json"),
),
(
"hive/constitution.json",
include_str!("../../../template/hive/constitution.json"),
Expand Down Expand Up @@ -97,6 +110,10 @@ const TEMPLATE: [(&str, &str); 17] = [
),
];

/// Where the hive's tools and toolpacks go in the loop folder: written from
/// the toolkit, not the template.
const TOOLS_PATH: &str = "hive/tools.json";

/// Where the conjecture goes in the loop folder.
pub const STATEMENT_PATH: &str = "subject/lean/Supermath/Statement.lean";

Expand Down Expand Up @@ -157,13 +174,9 @@ pub fn create(
.replace("{{statement}}", statement.trim_end())
};
for (path, text) in TEMPLATE {
let text = if path == "hive/hive.json" {
hive_manifest(&render(text), program, registry)?
} else {
render(text)
};
write(&dir.join(path), &text)?;
write(&dir.join(path), &render(text))?;
}
write(&dir.join(TOOLS_PATH), &tool_manifest(program, registry)?)?;
write(&dir.join(STATEMENT_PATH), statement)
}

Expand All @@ -175,10 +188,9 @@ fn declares_conjecture(statement: &str) -> bool {
.any(|line| line.trim_start().starts_with("def Conjecture"))
}

/// The template's `hive.json` with the toolkit's tools and toolpacks added.
fn hive_manifest(text: &str, program: &Program, registry: &ToolRegistry) -> Result<String> {
let mut manifest: Map<String, Value> =
serde_json::from_str(text).map_err(|error| Error::Template(error.to_string()))?;
/// The hive's `tools.json`: the toolkit's tools and its domain toolpacks.
fn tool_manifest(program: &Program, registry: &ToolRegistry) -> Result<String> {
let mut manifest = Map::new();
let tools: Vec<Value> = match declarations(registry, program) {
Value::Array(tools) => tools
.into_iter()
Expand Down
34 changes: 32 additions & 2 deletions crates/supermath-mcp/src/cli/scaffold/test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -79,10 +79,40 @@ fn the_manifest_runs_this_binary_as_its_scorer_and_freezes_the_statement() {
}

#[test]
fn the_hive_holds_the_toolkit_less_the_file_tools_in_domain_toolpacks() {
fn the_hive_manifest_is_split_into_agents_desks_and_tools() {
let (_root, dir) = scaffold();
let section = |file: &str| -> Vec<String> {
let mut keys: Vec<String> = json(&dir, file)
.as_object()
.unwrap()
.keys()
.cloned()
.collect();
keys.sort();
keys
};
let hive = json(&dir, "hive/hive.json");
assert_eq!(hive["id"], "demo");
for moved in ["roles", "seats", "desks", "tools", "toolpacks"] {
assert!(hive.get(moved).is_none(), "hive.json still holds {moved}");
}
assert_eq!(section("hive/agents.json"), ["roles", "seats"]);
assert_eq!(section("hive/desks.json"), ["desks"]);
assert_eq!(section("hive/tools.json"), ["toolpacks", "tools"]);
let seats = json(&dir, "hive/agents.json")["seats"].clone();
let ids: Vec<&str> = seats
.as_array()
.unwrap()
.iter()
.map(|seat| seat["id"].as_str().unwrap())
.collect();
assert_eq!(ids, ["lead", "prover", "refuter"]);
}

#[test]
fn the_hive_holds_the_toolkit_less_the_file_tools_in_domain_toolpacks() {
let (_root, dir) = scaffold();
let hive = json(&dir, "hive/tools.json");
let ids: Vec<&str> = hive["tools"]
.as_array()
.unwrap()
Expand Down Expand Up @@ -110,7 +140,7 @@ fn the_hive_holds_the_toolkit_less_the_file_tools_in_domain_toolpacks() {
assert!(pack("ledger").contains(&"recall_memory".to_owned()));
assert_eq!(pack("ledger-read"), ["ledger_claims", "recall_memory"]);
// Every toolpack a seat names exists.
for seat in hive["seats"].as_array().unwrap() {
for seat in json(&dir, "hive/agents.json")["seats"].as_array().unwrap() {
for name in seat["toolpacks"].as_array().unwrap() {
pack(name.as_str().unwrap());
}
Expand Down
123 changes: 123 additions & 0 deletions crates/supermath-mcp/template/hive/agents.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,123 @@
{
"roles": [
{
"id": "lead",
"charter": "roles/lead.md"
},
{
"id": "prover",
"charter": "roles/prover.md"
},
{
"id": "refuter",
"charter": "roles/refuter.md"
}
],
"seats": [
{
"id": "lead",
"role": "lead",
"prompt": "seats/lead.md",
"template": "openhuman",
"config": {
"action_dir": "{incumbent}",
"max_iterations": 30
},
"tools": {
"allow": [
"file_read",
"grep",
"glob",
"list",
"read_diff"
],
"deny": [
"wait",
"wait_loop",
"spawn_subagent",
"spawn_async_subagent",
"spawn_parallel_agents",
"web_fetch",
"shell"
]
},
"toolpacks": [
"literature",
"ledger-read"
]
},
{
"id": "prover",
"role": "prover",
"prompt": "seats/prover.md",
"template": "openhuman",
"config": {
"action_dir": "{candidate}",
"max_iterations": 60
},
"tools": {
"allow": [
"file_read",
"grep",
"glob",
"list",
"read_diff",
"file_write",
"edit",
"apply_patch"
],
"deny": [
"wait",
"wait_loop",
"spawn_subagent",
"spawn_async_subagent",
"spawn_parallel_agents",
"web_fetch",
"shell"
]
},
"toolpacks": [
"lean",
"literature",
"ledger"
]
},
{
"id": "refuter",
"role": "refuter",
"prompt": "seats/refuter.md",
"template": "openhuman",
"config": {
"action_dir": "{candidate}",
"max_iterations": 60
},
"tools": {
"allow": [
"file_read",
"grep",
"glob",
"list",
"read_diff",
"file_write",
"edit",
"apply_patch"
],
"deny": [
"wait",
"wait_loop",
"spawn_subagent",
"spawn_async_subagent",
"spawn_parallel_agents",
"web_fetch",
"shell"
]
},
"toolpacks": [
"lean",
"python",
"literature",
"ledger"
]
}
]
}
15 changes: 15 additions & 0 deletions crates/supermath-mcp/template/hive/desks.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
{
"desks": [
{
"id": "lab",
"name": "Settling lab",
"description": "settle one pinned conjecture in Lean",
"members": [
"lead",
"prover",
"refuter"
],
"responder_mode": "auto"
}
]
}
Loading
Loading