Skip to content

feat: add proof workspace package #170

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
tonyketcham merged 1 commit into from
May 8, 2026
Merged

feat: add proof workspace package #170

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
185 changes: 131 additions & 54 deletions .cursor/skills/dag-task-runner/scripts/canvas_writer.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -188,17 +188,15 @@ function renderCanvasSource(state: RunState): string {
return `${HEADER}\n\nconst STATE: RunState = ${stateLiteral};\n\n${BODY}\n`;
}

const HEADER = `/* AUTO-GENERATED by sdk/dag-task-runner. Do not edit by hand — the runner overwrites this file. */
const HEADER = `/* AUTO-GENERATED by @flatbread/proof. Do not edit by hand — the runner overwrites this file. */
import {
Card,
CardBody,
CardHeader,
Divider,
Grid,
H1,
H2,
Pill,
Row,
Stack,
Stat,
Text,
Expand Down Expand Up @@ -252,12 +250,12 @@ interface RunState {
tasks: TaskState[];
}`;

const BODY = String.raw`const NODE_W = 200;
const NODE_H = 64;
const SCROLL_STORAGE_KEY = 'dag-task-runner:scroll-y';
const BODY = String.raw`const NODE_H = 64;
const SCROLL_STORAGE_KEY = '@flatbread/proof:scroll-y';
const COMPLETED_DOT_COLOR = '#22c55e';
const AWAITING_DOT_COLOR = '#f59e0b';
const BUDGET_DOT_COLOR = '#ef4444';
const COMPACT_BREAKPOINT_PX = 720;

function effectiveKind(t: TaskState): TaskKind {
return t.kind ?? 'task';
Expand Down Expand Up @@ -320,6 +318,20 @@ function taskElementId(taskId: string): string {
return 'task-card-' + taskId;
}

function useViewportWidth(): number {
const [width, setWidth] = useState(1024);

useEffect(() => {
if (typeof window === 'undefined') return;
const update = (): void => setWidth(window.innerWidth);
update();
window.addEventListener('resize', update);
return () => window.removeEventListener('resize', update);
}, []);

return width;
}

function getScrollY(): number {
if (typeof window === 'undefined') return 0;
return Math.max(window.scrollY ?? 0, 0);
Expand Down Expand Up @@ -378,17 +390,24 @@ function DAGGraph({
onNodeClick?: (taskId: string) => void;
}): JSX.Element {
const theme = useHostTheme();
const viewportWidth = useViewportWidth();
const isCompact = viewportWidth < COMPACT_BREAKPOINT_PX;
const nodeWidth = isCompact ? 168 : 200;
const nodeGap = isCompact ? 24 : 40;
const rankGap = isCompact ? 60 : 72;
const layoutPadding = isCompact ? 12 : 24;
const titleLimit = Math.max(12, Math.floor((nodeWidth - 44) / 7));
const layout = computeDAGLayout({
nodes: state.tasks.map((t) => ({ id: t.id })),
edges: state.tasks.flatMap((t) =>
t.depends_on.map((d) => ({ from: d, to: t.id })),
),
direction: 'vertical',
nodeWidth: NODE_W,
nodeWidth,
nodeHeight: NODE_H,
rankGap: 72,
nodeGap: 40,
padding: 24,
rankGap,
nodeGap,
padding: layoutPadding,
});

const byId = new Map(state.tasks.map((t) => [t.id, t]));
Expand Down Expand Up @@ -462,10 +481,24 @@ function DAGGraph({
}

return (
<div
style={{
width: '100%',
maxWidth: '100%',
overflowX: 'auto',
overflowY: 'hidden',
WebkitOverflowScrolling: 'touch',
paddingBottom: 4,
}}
>
<svg
width={layout.width}
height={layout.height}
style={{ display: 'block', maxWidth: '100%' }}
style={{
display: 'block',
minWidth: Math.min(layout.width, nodeWidth + layoutPadding * 2),
maxWidth: layout.width <= viewportWidth ? '100%' : undefined,
}}
>
<defs>
<marker
Expand Down Expand Up @@ -504,7 +537,7 @@ function DAGGraph({
style={{ cursor: onNodeClick ? 'pointer' : 'default' }}
>
<rect
width={NODE_W}
width={nodeWidth}
height={NODE_H}
rx={8}
ry={8}
Expand All @@ -528,7 +561,7 @@ function DAGGraph({
fontWeight={600}
fill={theme.text.primary}
>
{t.id.length > 22 ? t.id.slice(0, 21) + '…' : t.id}
{t.id.length > titleLimit ? t.id.slice(0, titleLimit - 1) + '…' : t.id}
</text>
<text
x={12}
Expand Down Expand Up @@ -565,6 +598,38 @@ function DAGGraph({
);
})}
</svg>
</div>
);
}

function SummaryStats({
counts,
}: {
counts: {
total: number;
pending: number;
running: number;
finished: number;
error: number;
awaiting: number;
};
}): JSX.Element {
return (
<div
style={{
display: 'grid',
gridTemplateColumns: 'repeat(auto-fit, minmax(112px, 1fr))',
gap: 12,
width: '100%',
}}
>
<Stat value={String(counts.total)} label="Total" />
<Stat value={String(counts.pending)} label="Pending" />
<Stat value={String(counts.running)} label="Running" tone={counts.running > 0 ? 'info' : undefined} />
<Stat value={String(counts.awaiting)} label="Awaiting" tone={counts.awaiting > 0 ? 'warning' : undefined} />
<Stat value={String(counts.finished)} label="Finished" tone={counts.finished > 0 ? 'success' : undefined} />
<Stat value={String(counts.error)} label="Errored" tone={counts.error > 0 ? 'danger' : undefined} />
</div>
);
}

Expand All @@ -580,14 +645,21 @@ function TaskList({
<Stack gap={10}>
{state.tasks.map((t) => {
const trailing = (
<Row gap={6} align="center">
<div
style={{
display: 'flex',
flexWrap: 'wrap',
justifyContent: 'flex-end',
gap: 6,
}}
>
<Pill tone={complexityTone(t.complexity)} size="sm">
{t.complexity}
</Pill>
<Pill tone={pillToneFor(t.status)} active={t.status !== 'PENDING'} size="sm">
{t.status}
</Pill>
</Row>
</div>
);
return (
<div key={t.id} id={taskElementId(t.id)}>
Expand Down Expand Up @@ -761,7 +833,7 @@ export default function DagRun(): JSX.Element {
break;
case 'BUDGET-EXCEEDED':
// Surfaced via the per-task pill / glyph; bucketed under errored
// here so the 6-column summary grid stays stable.
// here so the summary counts stay stable.
acc.error += 1;
break;
}
Expand Down Expand Up @@ -795,49 +867,54 @@ export default function DagRun(): JSX.Element {
: 'info';

return (
<Stack gap={20}>
<Stack gap={6}>
<H1>{STATE.title}</H1>
<Row gap={10} align="center">
<Pill tone={statusTone} active size="sm">
{statusLabel}
</Pill>
<Text tone="secondary" size="small">
{counts.total} tasks · elapsed {formatDuration(elapsed(STATE))}
{tokens.input + tokens.output > 0
? ' · ' + tokens.input + ' in / ' + tokens.output + ' out tokens'
: ''}
</Text>
</Row>
{STATE.runMessage ? (
<Text tone="secondary" size="small">
{STATE.runMessage}
</Text>
) : null}
</Stack>
<main style={{ overflowX: 'hidden', width: '100%', maxWidth: '100%' }}>
<Stack gap={20}>
<Stack gap={6}>
<div style={{ minWidth: 0 }}>
<H1>{STATE.title}</H1>
</div>
<div
style={{
display: 'flex',
flexWrap: 'wrap',
alignItems: 'center',
gap: 10,
minWidth: 0,
}}
>
<Pill tone={statusTone} active size="sm">
{statusLabel}
</Pill>
<Text tone="secondary" size="small">
{counts.total} tasks · elapsed {formatDuration(elapsed(STATE))}
{tokens.input + tokens.output > 0
? ' · ' + tokens.input + ' in / ' + tokens.output + ' out tokens'
: ''}
</Text>
</div>
{STATE.runMessage ? (
<Text tone="secondary" size="small">
{STATE.runMessage}
</Text>
) : null}
</Stack>

<Grid columns={6} gap={12}>
<Stat value={String(counts.total)} label="Total" />
<Stat value={String(counts.pending)} label="Pending" />
<Stat value={String(counts.running)} label="Running" tone={counts.running > 0 ? 'info' : undefined} />
<Stat value={String(counts.awaiting)} label="Awaiting" tone={counts.awaiting > 0 ? 'warning' : undefined} />
<Stat value={String(counts.finished)} label="Finished" tone={counts.finished > 0 ? 'success' : undefined} />
<Stat value={String(counts.error)} label="Errored" tone={counts.error > 0 ? 'danger' : undefined} />
</Grid>
<SummaryStats counts={counts} />

<Divider />
<Divider />

<Stack gap={12}>
<H2>Graph</H2>
<DAGGraph state={STATE} onNodeClick={handleNodeClick} />
</Stack>
<Stack gap={12}>
<H2>Graph</H2>
<DAGGraph state={STATE} onNodeClick={handleNodeClick} />
</Stack>

<Divider />
<Divider />

<Stack gap={12}>
<H2>Tasks</H2>
<TaskList state={STATE} forcedOpenVersionByTaskId={forcedOpenVersionByTaskId} />
<Stack gap={12}>
<H2>Tasks</H2>
<TaskList state={STATE} forcedOpenVersionByTaskId={forcedOpenVersionByTaskId} />
</Stack>
</Stack>
</Stack>
</main>
);
}`;
4 changes: 2 additions & 2 deletions .cursor/skills/dag-task-runner/scripts/oracle_task.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,7 @@ export async function runOracleTask(
deps.writer.schedule(deps.cloneState(deps.state));

console.log(
`[dag-runner] oracle ${task.id} → exec \`${command}\` (expect /${expectSrc}/)`
`[proof] oracle ${task.id} → exec \`${command}\` (expect /${expectSrc}/)`
);

const outcome = await execShell(command, options);
Expand Down Expand Up @@ -142,7 +142,7 @@ export async function runOracleTask(
deps.writer.schedule(deps.cloneState(deps.state));

console.log(
`[dag-runner] oracle ${task.id} → ${pass ? 'PASS' : 'FAIL'} (exit ${
`[proof] oracle ${task.id} → ${pass ? 'PASS' : 'FAIL'} (exit ${
outcome.exitCode ?? 'null'
}, ${ts.durationMs}ms${outcome.timedOut ? ', TIMED OUT' : ''})`
);
Expand Down
4 changes: 2 additions & 2 deletions .cursor/skills/dag-task-runner/scripts/pause_task.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ export async function runPauseTask(
deps.writer.schedule(deps.cloneState(deps.state));

console.log(
`[dag-runner] pause ${task.id} → AWAITING_APPROVAL; delete ${sentinelPath} to release the gate`
`[proof] pause ${task.id} → AWAITING_APPROVAL; delete ${sentinelPath} to release the gate`
);

const deadline = Date.now() + options.taskTimeoutMs;
Expand Down Expand Up @@ -92,7 +92,7 @@ export async function runPauseTask(
ts.resultText = renderApprovedResultText(sentinelPath, ts.finishedAt);
deps.writer.schedule(deps.cloneState(deps.state));
console.log(
`[dag-runner] pause ${task.id} → FINISHED (sentinel removed, ${ts.durationMs}ms gated)`
`[proof] pause ${task.id} → FINISHED (sentinel removed, ${ts.durationMs}ms gated)`
);
return;
}
Expand Down
Loading
Loading