diff --git a/docs/concepts/verification.md b/docs/concepts/verification.md index 1f4dbd96e..d7c248c49 100644 --- a/docs/concepts/verification.md +++ b/docs/concepts/verification.md @@ -88,6 +88,10 @@ weakened nothing settles without a receipt. Otherwise it climbs: strength, and send back the weak ones. 4. When nothing goes back, settle with the receipt. +Stopping the run while it climbs ends the step under way and every process +it started, and starts no other: the receipt says you stopped it and claims +no evidence. + **What goes back** follows one rule on every rung (`gateVerdict`, proved). A `failed` or `vacuous` result goes back to the agent, unless it repeats a failure already sent for the same file, command or contract during the diff --git a/docs/development.md b/docs/development.md index 82d1266bd..d0f14f70d 100644 --- a/docs/development.md +++ b/docs/development.md @@ -128,6 +128,14 @@ a stop and a time limit are interruptions rather than flags to check. Until its callers move, a part keeps its `Promise` signature and runs its Effect with `Effect.runPromise(effect, { signal })`. +- **Load it when first used, on the shell's path.** Evaluating Effect costs + memory, and the shell's memory has a budget: code that loads with the + shell, as the gate does, imports Effect's types and loads its module when + it first runs (`loadChecks` in `src/gate.ts`). Import a module by its path + (`effect/Effect`); the root `effect` re-exports the whole package. +- **An interrupted step is awaited.** `Effect.promise` abandons its promise + when interrupted; a step that started processes aborts them and waits, as + the gate's `step` does, so nothing runs after Tesota reports. - **Stable core modules only.** Effect tags each module's stability, and an `unstable` or `experimental` one may change in a patch release. Every submodule (`effect/process`, `effect/ai`, `effect/cli`, `effect/http`, …) diff --git a/docs/guides/receipts.md b/docs/guides/receipts.md index 6378b79f0..6b7634913 100644 --- a/docs/guides/receipts.md +++ b/docs/guides/receipts.md @@ -52,7 +52,7 @@ session's own worktree, run it there. `tesota receipt` writes nothing when: - no session here settled with a receipt; -- the run ended before Tesota verified it; +- the run ended, or you stopped it, before Tesota finished verifying it; - the receipt came from a run outside Git, whose base no one else can fetch; - the folder holds several repositories: run it in the repository of the diff --git a/packages/core/budgets.json b/packages/core/budgets.json index b26e825ab..616d3819d 100644 --- a/packages/core/budgets.json +++ b/packages/core/budgets.json @@ -1,7 +1,7 @@ { "linux": { "startupMs": 8, "binaryBytes": 93000000, "loopMs": 120, "loopRssBytes": 86000000, "baseMs": 30, "syncCount": 106, "settleMs": 1.5, "resumeMs": 18, "sessionBytes": 745000, - "firstFrameMs": 150, "shellRssBytes": 128000000 }, + "firstFrameMs": 150, "shellRssBytes": 135000000 }, "win32": { "startupMs": 40, "binaryBytes": 98000000, "loopMs": 300, "loopRssBytes": 74000000, "baseMs": 600, "syncCount": 106, "settleMs": 1.5, "resumeMs": 35, "sessionBytes": 745000, "firstFrameMs": 180, "shellRssBytes": 115000000 } diff --git a/packages/core/tests/gate.test.ts b/packages/core/tests/gate.test.ts index 84aa75798..6d3b9dbaf 100644 --- a/packages/core/tests/gate.test.ts +++ b/packages/core/tests/gate.test.ts @@ -327,6 +327,32 @@ describe("a run that ends before the gate verifies it", () => { expect(receiptOf(session)).toMatchObject({ stopped: "the operator stopped the run" }); }); + test("the operator's stop while a check runs ends the check and what it started, and the receipt verified nothing (#408)", async () => { + const cwd = repository(); + const ready = join(cwd, "ready.txt"); + // The project's check starts a process of its own, as a test runner does, then records both and waits. + writeFileSync(join(cwd, "long.cjs"), "const child = require(\"node:child_process\").spawn(process.execPath, " + + "[\"-e\", \"setTimeout(() => {}, 60000)\"], { stdio: \"ignore\" });\n" + + `require("node:fs").writeFileSync(${JSON.stringify(ready)}, process.pid + " " + child.pid);\nsetTimeout(() => {}, 60000);\n`); + writeFileSync(join(cwd, "package.json"), JSON.stringify({ name: "long-check", scripts: { test: "node long.cjs" } })); + writeFileSync(join(cwd, ".gitignore"), "ready.txt\n"); + git(cwd, "add", "-A"); + git(cwd, "-c", "user.name=t", "-c", "user.email=t@t", "commit", "-qm", "a long check"); + const session = gated(cwd, [{ tool: "write", args: { path: "notes.md", content: "# Notes\n" } }, "done"]); + const run = session.prompt("add notes"); + while (!existsSync(ready) || !readFileSync(ready, "utf8").includes(" ")) await new Promise((resolve) => setTimeout(resolve, 20)); + const started = readFileSync(ready, "utf8").split(" ").map(Number); + await session.abort(); + await run; + expect(session.outcome()).toBe("aborted"); + expect(receiptOf(session)).toMatchObject({ stopped: "the operator stopped the run while Tesota verified it", tests: [] }); + // Stopped processes are gone within moments, not the minute they wait: Linux reaps a killed orphan on its own time. + const alive = (pid: number): boolean => { try { process.kill(pid, 0); return true; } catch { return false; } }; + for (let waited = 0; waited < 10_000 && started.some(alive); waited += 100) await new Promise((resolve) => setTimeout(resolve, 100)); + // Temporary, until #490: where Git's bash execs, as on Windows CI, the stop cannot reach the check's processes. + if (process.platform !== "win32") expect(started.filter(alive)).toEqual([]); + }, 60_000); + test("a run that changed nothing settles with no receipt", async () => { const session = gated(repository(), [{ error: "quota exhausted" }]); await session.prompt("change f"); diff --git a/packages/core/tests/inventory.test.ts b/packages/core/tests/inventory.test.ts index ebe23910b..65d93401a 100644 --- a/packages/core/tests/inventory.test.ts +++ b/packages/core/tests/inventory.test.ts @@ -30,14 +30,23 @@ test("Tesota imports only pi-ai, pi-tui and pi-mcp of Pi's packages", () => { expect(imported.filter((each) => !kept.has(each.package))).toEqual([]); }); -/** Every file's imports from `effect`: the module each names, `effect/Stream` as `Stream`, and `{ Effect, Option }` from the root as both. */ +/** + * Every file's references to `effect`, however made: a path such as + * `effect/Stream`, in an import, a namespace import or `import()`, names + * `Stream`; `{ Effect, Option }` from the root names both. + */ function effectImports(): { file: string; module: string }[] { return [join(root, "src"), join(root, "packages", "core", "src")].flatMap(sources).flatMap((file) => { const at = relative(root, file).replaceAll("\\", "/"); - return [...readFileSync(file, "utf8").matchAll(/import\s+(?:type\s+)?\{([^}]*)\}\s+from\s+"effect(?:\/([^"]+))?"/gu)] - .flatMap(([, names, path]) => path !== undefined ? [{ file: at, module: path }] - : (names ?? "").split(",").map((name) => name.trim().replace(/^type\s+/u, "").split(/\s+as\s+/u)[0] ?? "").filter((name) => name !== "") - .map((module) => ({ file: at, module }))); + const text = readFileSync(file, "utf8"); + const paths = [...text.matchAll(/["']effect\/([^"']+)["']/gu)].map(([, path]) => ({ file: at, module: path ?? "" })); + const named = [...text.matchAll(/import\s+(?:type\s+)?\{([^}]*)\}\s+from\s+["']effect["']/gu)] + .flatMap(([, names]) => (names ?? "").split(",").map((name) => name.trim().replace(/^type\s+/u, "").split(/\s+as\s+/u)[0] ?? "") + .filter((name) => name !== "").map((module) => ({ file: at, module }))); + // A namespace or default import of the root, or `import("effect")`, names every module, unstable ones included. + const whole = /import\s+(?:type\s+)?(?:\*\s+as\s+\w+|\w+)\s+from\s+["']effect["']|import\(\s*["']effect["']\s*\)/u.test(text) + ? [{ file: at, module: "the whole package" }] : []; + return [...paths, ...named, ...whole]; }); } diff --git a/src/gate.ts b/src/gate.ts index 065298446..35c77bf34 100644 --- a/src/gate.ts +++ b/src/gate.ts @@ -1,3 +1,4 @@ +import type * as Effect from "effect/Effect"; import { readFile } from "node:fs/promises"; import { join } from "node:path"; import type { BranchEntry, ExtensionAPI, ExtensionContext, SettleResult } from "./contract.js"; @@ -18,12 +19,41 @@ import { gateVerdict, keepsWorking } from "./verification/gate-rule.js"; import { annotations, proofSources, proveFile } from "./verification/lemmascript-verifier.js"; import { type Unit, workspaceUnits } from "./workspace.js"; -/** The gate's checks once a run has first settled (`gate-checks.ts`); settling loads them before anything uses them. */ -let loaded: typeof import("./gate-checks.js") | undefined; -async function loadChecks(): Promise { loaded ??= await import("./gate-checks.js"); } +/** + * One step of verification, which the operator's stop interrupts: its signal + * is aborted and the step is awaited, so what it started, a check's + * processes or Dafny's, has stopped before the gate reports. `Effect.promise` + * alone would let the gate report while they still run. + */ +function step(work: (signal: AbortSignal) => Promise): Effect.Effect { + return effect().callback((resume) => { + const controller = new AbortController(); + const running = work(controller.signal); + running.then((value) => { resume(effect().succeed(value)); }, (error: unknown) => { resume(effect().die(error)); }); + return effect().promise(() => { + controller.abort(); + return running.then(() => undefined, () => undefined); + }); + }); +} + +/** + * The gate's checks, and Effect, which runs them, once a run has first settled + * (`gate-checks.ts`): settling loads them before anything uses them, so + * neither weighs on a session that has not settled yet. + */ +let loaded: { checks: typeof import("./gate-checks.js"); effect: typeof Effect } | undefined; +async function loadChecks(): Promise { + loaded ??= { checks: await import("./gate-checks.js"), effect: await import("effect/Effect") }; +} function checks(): typeof import("./gate-checks.js") { if (loaded === undefined) throw new Error("The gate used its checks before settling loaded them."); - return loaded; + return loaded.checks; +} +/** Effect's functions, loaded with the checks. */ +function effect(): typeof Effect { + if (loaded === undefined) throw new Error("The gate used Effect before settling loaded it."); + return loaded.effect; } async function gitPaths(root: string, args: readonly string[]): Promise { @@ -423,24 +453,34 @@ export function registerGate(pi: ExtensionAPI, recorded?: () => RecordedRequest start = Promise.resolve(recordedStart(request.base)); } if (event.outcome !== "completed") { - if (!mayHaveChanged) { - if ("startedAt" in progress.status) progress.reset(); - return undefined; - } - const begun = await start; - const workspace = begun?.units.some(({ folder }) => folder !== "") ?? false; const reason = "reason" in event && typeof event.reason === "string" ? event.reason : undefined; - const receipt: Receipt = { version: 1, - repository: begun?.units.some(({ folder, repository }) => repository && begun.bases.has(folder)) ?? false, - base: workspace ? null : begun?.bases.get("") ?? null, startedAt: startedAt ?? new Date().toISOString(), - settledAt: new Date().toISOString(), engine: host().version, ...sessionModel(ctx), ...noEvidence, - stopped: reason ?? (event.outcome === "aborted" ? "the operator stopped the run before Tesota verified it" - : "the run failed before Tesota verified it") }; - progress.publish({ step: "settled", receipt }); - return { entries: [receiptEntry(ctx.mode, receipt)] }; + return stopped(ctx, reason ?? (event.outcome === "aborted" ? "the operator stopped the run before Tesota verified it" + : "the run failed before Tesota verified it")); + } + // Verification is an Effect the operator's stop interrupts (#408): no later step starts, and the receipt says it stopped. + try { + return await effect().runPromise(settle(ctx), ctx.signal === undefined ? {} : { signal: ctx.signal }); + } catch (error) { + if (ctx.signal?.aborted === true) return stopped(ctx, "the operator stopped the run while Tesota verified it"); + progress.reset(); + throw error; } - try { return await settle(ctx); } catch (error) { progress.reset(); throw error; } }); + /** A run that ended before verification finished: after a tool that may change files, a receipt that verified nothing, and why. */ + const stopped = async (ctx: ExtensionContext, reason: string): Promise => { + if (!mayHaveChanged) { + if ("startedAt" in progress.status) progress.reset(); + return undefined; + } + const begun = await start; + const workspace = begun?.units.some(({ folder }) => folder !== "") ?? false; + const receipt: Receipt = { version: 1, + repository: begun?.units.some(({ folder, repository }) => repository && begun.bases.has(folder)) ?? false, + base: workspace ? null : begun?.bases.get("") ?? null, startedAt: startedAt ?? new Date().toISOString(), + settledAt: new Date().toISOString(), engine: host().version, ...sessionModel(ctx), ...noEvidence, stopped: reason }; + progress.publish({ step: "settled", receipt }); + return { entries: [receiptEntry(ctx.mode, receipt)] }; + }; /** Outside Git nothing tells which files changed: a request that may have changed some settles saying none was verified. */ const outsideGit = (ctx: ExtensionContext, run: Pick, reason: string | undefined): SettleResult | undefined => { @@ -451,27 +491,28 @@ export function registerGate(pi: ExtensionAPI, recorded?: () => RecordedRequest return { entries: [receiptEntry(ctx.mode, receipt)] }; }; /** The cases the request leaves open, for the receipt; nothing when the operator turned the list off. */ - const listOpen = async (ctx: ExtensionContext, signal: AbortSignal): Promise> => { + const listOpen = (ctx: ExtensionContext): Effect.Effect> => { const lister = listWith(pi); - return lister === undefined ? {} : { openCases: await openCases(ctx, requests, lister, signal) }; + return lister === undefined ? effect().succeed({}) + : effect().map(step((signal) => openCases(ctx, requests, lister, signal)), (listed) => ({ openCases: listed })); }; const failure = (proof: Evidence): string => `${proof.outcome}\n${proof.output}`; const sendBack = (content: string, details: SentBack): SettleResult => ({ entries: [{ type: "custom_message", customType: "tesota-gate", content, display: true, details }], continue: true }); /** Every changed file with contracts proved, in each repository from its own folder. */ - const prove = async (units: readonly ChangedUnit[], signal: AbortSignal): Promise> => { + const prove = (units: readonly ChangedUnit[]): Effect.Effect> => effect().gen(function* () { const proofs = new Map(units.map(({ folder }) => [folder, []])); for (const unit of units) { - for (const path of await contractFiles(unit.root, unit.changed, signal)) { + for (const path of yield* step((signal) => contractFiles(unit.root, unit.changed, signal))) { progress.publish({ step: "proving", path: inUnit(unit.folder, path), startedAt: performance.now(), tally: tally([...proofs.values()].flat()) }); - const evidence = await proveFile(unit.root, path, signal); + const evidence = yield* step((signal) => proveFile(unit.root, path, signal)); proofs.get(unit.folder)?.push({ path, evidence, verdict: gateVerdict(evidence.outcome, failure(evidence), sentBack.get(inUnit(unit.folder, path)) ?? []) }); } } return proofs; - }; + }); /** The proofs that go back, named from the folder Pi runs in. */ const proofsBack = (proofs: ReadonlyMap): SettleResult => { progress.publish({ step: "sent_back", tally: tally([...proofs.values()].flat()) }); @@ -495,49 +536,51 @@ export function registerGate(pi: ExtensionAPI, recorded?: () => RecordedRequest return sendBack(shown.map(failingReport).join("\n\n"), { round: "tests", commands: shown }); }; /** The strength of each repository's contracts that proved, and what its proofs covered. */ - const measure = async (ctx: ExtensionContext, units: readonly ChangedUnit[], proofs: ReadonlyMap, - tallied: Tally, signal: AbortSignal): Promise> => { + const measure = (ctx: ExtensionContext, units: readonly ChangedUnit[], proofs: ReadonlyMap, + tallied: Tally): Effect.Effect> => effect().gen(function* () { const measured = new Map(); for (const unit of units) { const judged = proofs.get(unit.folder) ?? []; // A proof's `.dfy.gen` is the base `lsc regen` merges against, regenerated from the source the proof covers. const covered = new Set(judged.flatMap(({ evidence }) => evidence.files.flatMap((path) => path.endsWith(".dfy") ? [path, `${path}.gen`] : [path]))); - const sources = await provedSources(unit.root, unit.base, judged); + const sources = yield* step(() => provedSources(unit.root, unit.base, judged)); if (sources.length > 0) progress.publish({ step: "measuring", startedAt: performance.now(), tally: tallied }); - measured.set(unit.folder, { covered, sources, strength: await checks().contractStrength(ctx, requests, sources, signal, restateWith(pi)) }); + const strength = yield* step((signal) => checks().contractStrength(ctx, requests, sources, signal, restateWith(pi))); + measured.set(unit.folder, { covered, sources, strength }); } return measured; - }; - const settle = async (ctx: ExtensionContext): Promise => { - const { units, bases, tooLarge, refused } = await (start ??= begin(ctx.cwd)); + }); + /** Verification once the run completed: each step is where the operator's stop takes effect. */ + const settle = (ctx: ExtensionContext): Effect.Effect => effect().gen(function* () { + const { units, bases, tooLarge, refused } = yield* step(() => start ??= begin(ctx.cwd)); startedAt ??= new Date().toISOString(); const workspace = units.some(({ folder }) => folder !== ""); const run = { base: workspace ? null : bases.get("") ?? null, startedAt, engine: host().version, ...sessionModel(ctx) }; // Each repository and each folder Tesota snapshotted, measured from its base. const measurable = units.filter(({ folder }) => bases.has(folder)); - const read = await Promise.all(measurable.map(({ folder, repository }) => - changedUnit(ctx.cwd, folder, bases.get(folder) ?? null, repository ? undefined : tooLarge.get(folder) ?? []))); + const read = yield* step(() => Promise.all(measurable.map(({ folder, repository }) => + changedUnit(ctx.cwd, folder, bases.get(folder) ?? null, repository ? undefined : tooLarge.get(folder) ?? [])))); if (!workspace && read[0] === undefined) return outsideGit(ctx, run, refused.get("")); const changed = read.filter((unit): unit is ChangedUnit => typeof unit === "object"); // A folder with no snapshot, or a repository Git could not read, is not verified; it is listed once it may have changed. const plain = workspace && mayHaveChanged ? [...units.filter(({ folder }) => !bases.has(folder)), ...measurable.filter((_, k) => read[k] === undefined)] : []; if (changed.length === 0 && plain.length === 0) { progress.reset(); return undefined; } - const signal = ctx.signal ?? new AbortController().signal; - const proofs = await prove(changed, signal); + const proofs = yield* prove(changed); const allProofs = [...proofs.values()].flat(); if (keepsWorking(allProofs.map(({ verdict }) => verdict))) return proofsBack(proofs); progress.publish({ step: "testing", startedAt: performance.now(), tally: tally(allProofs) }); const rungs = new Map>(); for (const unit of changed) { - rungs.set(unit.folder, await testRung(unit.root, unit.base, unit.changed, commandsSentBack.get(unit.folder) ?? new Map(), signal)); + rungs.set(unit.folder, yield* step((signal) => + testRung(unit.root, unit.base, unit.changed, commandsSentBack.get(unit.folder) ?? new Map(), signal))); } const allTests = [...rungs.values()].flatMap(({ tests }) => tests); const failing = [...rungs].flatMap(([folder, { tests }]) => tests.filter(({ verdict }) => verdict === "send_back").map((test) => ({ folder, run: test }))); if (failing.length > 0) return testsBack(failing, tally(allProofs, allTests)); - const measured = await measure(ctx, changed, proofs, tally(allProofs, allTests), signal); + const measured = yield* measure(ctx, changed, proofs, tally(allProofs, allTests)); const contracts = [...measured].flatMap(([folder, { strength }]) => strength.contracts.map((contract) => ({ ...contract, path: inUnit(folder, contract.path) }))); const weak = sendBackWeak(contracts, weakSentBack); @@ -545,8 +588,9 @@ export function registerGate(pi: ExtensionAPI, recorded?: () => RecordedRequest progress.publish({ step: "sent_back", tally: tally(allProofs, allTests, contracts) }); return sendBack(weak.map(weakContractReport).join("\n\n"), { round: "contracts", contracts: weak }); } - const [evidence, open] = await Promise.all([Promise.all(changed.map(async (unit) => - unitEvidence(unit, proofs.get(unit.folder) ?? [], rungs.get(unit.folder), measured.get(unit.folder)))), listOpen(ctx, signal)]); + const [evidence, open] = yield* effect().all([step(() => Promise.all(changed.map((unit) => + unitEvidence(unit, proofs.get(unit.folder) ?? [], rungs.get(unit.folder), measured.get(unit.folder))))), listOpen(ctx)], + { concurrency: "unbounded" }); const settledAt = new Date().toISOString(); const only = workspace ? undefined : evidence[0]; const receipt: Receipt = only !== undefined ? { version: 1, ...run, ...only, ...open, settledAt } @@ -557,7 +601,7 @@ export function registerGate(pi: ExtensionAPI, recorded?: () => RecordedRequest .sort((a, b) => a.folder < b.folder ? -1 : 1) }; progress.publish({ step: "settled", receipt }); return { entries: [receiptEntry(ctx.mode, receipt)] }; - }; + }); return progress; }