diff --git a/agents/blueprint-absorber/README.md b/agents/blueprint-absorber/README.md new file mode 100644 index 0000000..5803cac --- /dev/null +++ b/agents/blueprint-absorber/README.md @@ -0,0 +1,54 @@ +# Blueprint Absorber Agent + +将 `draft-hint/` 里的数学家提示文件吸收进 `blueprint/src/chapters/*.tex`。 + +## 前置条件 + +```bash +pip install -e tools/plastexdepgraph +pip install -e tools/leanblueprint +``` + +## 本地运行 + +```bash +# 处理单个文件 +./agents/blueprint-absorber/run.sh draft-hint/foo.md + +# 处理所有待吸收文件 +./agents/blueprint-absorber/run.sh + +# 指定模型 +./agents/blueprint-absorber/run.sh --model opus draft-hint/foo.md + +# 试运行（只显示会处理哪些文件，不实际调用 claude） +./agents/blueprint-absorber/run.sh --dry-run +``` + +运行日志保存在 `agents/blueprint-absorber/logs/run-/absorber.jsonl`。 + +## 远程监控（多机协作） + +如果需要在本机跑 agent、同时让部署在服务器上的 dashboard 实时看到运行进度， +设置以下两个环境变量即可： + +```bash +export KIP_INGEST_URL=https://kip.opensii.ai/dashboard/api/ingest +export KIP_INGEST_TOKEN= # 与服务器 KIP_INGEST_TOKEN 一致，未配置 token 时可不设 +``` + +设置后正常跑 agent，每条日志 event 会自动上报到服务器，在 dashboard 的 +**Logs** tab 实时可见。未设置 `KIP_INGEST_URL` 时行为与纯本地模式完全一致。 + +### 验证网络是否通 + +```bash +curl -s -w "\nHTTP %{http_code}" -X POST "$KIP_INGEST_URL" -H "Content-Type: application/json" -d '{"agent":"blueprint-absorber","runId":"run-test","hintFile":"test","row":{"ts":"2026-01-01T00:00:00Z","event":"text","content":"ping"}}' +``` + +返回 `HTTP 204` 即表示连接正常。 + +## 状态追踪 + +`agents/blueprint-absorber/STATUS.md` 记录哪些 hint 文件已吸收（Absorbed）、哪些待处理（Pending）。 +成功吸收后 agent 自动更新此文件。 diff --git a/agents/blueprint-absorber/run.sh b/agents/blueprint-absorber/run.sh index 710e1f8..833ad54 100755 --- a/agents/blueprint-absorber/run.sh +++ b/agents/blueprint-absorber/run.sh @@ -124,16 +124,35 @@ Instructions: - If the file was listed under '## Pending', remove it from there. 8. Report what changed and whether validation passed." \ 2>>"$stderr_dest" | python3 -u -c " -import sys, json, datetime +import sys, json, datetime, urllib.request, os VERBOSE = '$VERBOSE_LOGS' == 'true' RAW = open('$RAW_FILE', 'a') if VERBOSE else None JSONL = open('$JSONL_FILE', 'a') +_INGEST_URL = os.getenv('KIP_INGEST_URL', '') +_INGEST_TOKEN = os.getenv('KIP_INGEST_TOKEN', '') +_AGENT = 'blueprint-absorber' +_RUN_ID = 'run-$RUN_TS' +_HINT_FILE = '$HINT_FILE' + +def ingest(row): + if not _INGEST_URL: + return + payload = json.dumps({'agent': _AGENT, 'runId': _RUN_ID, 'hintFile': _HINT_FILE, 'row': row}).encode() + req = urllib.request.Request(_INGEST_URL, data=payload, + headers={'Content-Type': 'application/json', 'Authorization': 'Bearer ' + _INGEST_TOKEN}, + method='POST') + try: + urllib.request.urlopen(req, timeout=3) + except Exception: + pass + def emit(event_type, **fields): row = {'ts': datetime.datetime.now(datetime.timezone.utc).isoformat().replace('+00:00', 'Z'), 'event': event_type, **fields} JSONL.write(json.dumps(row) + '\n') JSONL.flush() + ingest(row) last_result = '' diff --git a/homepage/index.html b/homepage/index.html new file mode 100644 index 0000000..559a5bf --- /dev/null +++ b/homepage/index.html @@ -0,0 +1,157 @@ + + + + + + On the Last Kervaire Invariant Problem + + + +

On the Last Kervaire Invariant Problem

+

by Weinan Lin, Guozhen Wang, and Zhouli Xu

+

+ A Lean 4 formalization of the paper On the Last Kervaire Invariant Problem, + which proves that framed manifolds of Kervaire invariant one exist in dimension 126. +

+ +
+
Formalization progress
+
+
+
+
+
+
+
+
+
+
+ Loading… +
+
+ + + + + + diff --git a/ui/server/src/index.ts b/ui/server/src/index.ts index 47e248e..767d3b3 100644 --- a/ui/server/src/index.ts +++ b/ui/server/src/index.ts @@ -11,6 +11,7 @@ import { register as registerAgents } from './routes/agents.js'; import { register as registerLogs } from './routes/logs.js'; import { register as registerSummary } from './routes/summary.js'; import { register as registerNodes } from './routes/nodes.js'; +import { register as registerIngest } from './routes/ingest.js'; export interface ProjectPaths { projectPath: string; @@ -64,6 +65,7 @@ export async function createServer(options: { projectPath: string; port: number registerLogs(fastify, paths); registerSummary(fastify, paths); registerNodes(fastify, paths); + registerIngest(fastify, paths); await fastify.listen({ port, host: '0.0.0.0' }); return fastify; diff --git a/ui/server/src/routes/ingest.ts b/ui/server/src/routes/ingest.ts new file mode 100644 index 0000000..3188bdb --- /dev/null +++ b/ui/server/src/routes/ingest.ts @@ -0,0 +1,75 @@ +import fs from 'fs'; +import path from 'path'; +import type { FastifyInstance } from 'fastify'; +import type { ProjectPaths } from '../index.js'; + +const TOKEN = process.env.KIP_INGEST_TOKEN ?? ''; + +// agent name and runId must be safe path segments +function safeSeg(s: unknown): s is string { + return typeof s === 'string' && /^[\w.\-:]+$/.test(s) && !s.includes('..'); +} + +export function register(fastify: FastifyInstance, paths: ProjectPaths) { + fastify.post('/api/ingest', async (req, reply) => { + if (TOKEN) { + const auth = (req.headers.authorization ?? '') as string; + if (auth !== `Bearer ${TOKEN}`) { + return reply.code(401).send({ error: 'unauthorized' }); + } + } + + const body = req.body as Record | undefined; + if (!body) return reply.code(400).send({ error: 'missing JSON body' }); + + const { agent, runId, hintFile, row } = body; + + if (!safeSeg(agent) || !safeSeg(runId)) { + return reply.code(400).send({ error: 'invalid agent or runId' }); + } + + const runDir = path.resolve(paths.agentsPath, agent, 'logs', runId); + if (!runDir.startsWith(paths.agentsPath + path.sep)) { + return reply.code(400).send({ error: 'path outside agents directory' }); + } + + fs.mkdirSync(runDir, { recursive: true }); + + const metaFile = path.join(runDir, 'meta.json'); + const jsonlFile = path.join(runDir, 'absorber.jsonl'); + + // Write meta.json on the first event for this run + if (!fs.existsSync(metaFile)) { + const meta = { + agent, + hint_file: typeof hintFile === 'string' ? hintFile : null, + startedAt: (row as Record)?.ts ?? new Date().toISOString(), + completedAt: null, + status: 'running', + model: null, + }; + fs.writeFileSync(metaFile, JSON.stringify(meta, null, 2)); + } + + // Update meta on session_end + if ((row as Record)?.event === 'session_end') { + try { + const meta = JSON.parse(fs.readFileSync(metaFile, 'utf-8')); + meta.completedAt = (row as Record).ts ?? new Date().toISOString(); + meta.status = 'done'; + const usage = (row as Record).model_usage as Record | undefined; + if (usage) { + const first = Object.keys(usage)[0]; + if (first) meta.model = first; + } + fs.writeFileSync(metaFile, JSON.stringify(meta, null, 2)); + } catch { /* ignore */ } + } + + // Append event row to JSONL — fs.watch in logs.ts picks this up automatically + // and broadcasts to any connected WebSocket clients watching this file + fs.appendFileSync(jsonlFile, JSON.stringify(row) + '\n'); + + return reply.code(204).send(); + }); +}