From f0c9043ae8db13012d6f0031579e02baea748e5c Mon Sep 17 00:00:00 2001 From: Canitas Date: Thu, 29 Oct 2026 19:44:25 -0700 Subject: [PATCH 1/2] fix: keep an unreadable version from failing a logged run --- DESIGN_RUN_LOG.md | 2 +- tools/src/lsc.ts | 2 +- tools/src/run-log.ts | 7 ++++--- tools/tests/run-log.test.ts | 32 +++++++++++++++++++++++--------- 4 files changed, 29 insertions(+), 14 deletions(-) diff --git a/DESIGN_RUN_LOG.md b/DESIGN_RUN_LOG.md index 06aea77..46145ca 100644 --- a/DESIGN_RUN_LOG.md +++ b/DESIGN_RUN_LOG.md @@ -71,7 +71,7 @@ The helper that detects how the run ended appends one record: `dafnyCheckDiff` f - **`stage`** tells where the run stopped. `diff` means the additions-only check failed, so Dafny never ran. `resolve` means Dafny wrote no member results (a parse or resolution error, or `lsc` refused the proof before running Dafny). If Dafny is not installed, nothing was verified and the run is not recorded. `conflict` means a `regen` merge conflicted. `verify` means Dafny ran and reported failures. `ok` means everything that ran passed. - **`failed` / `passed`** are member names. A member that fails either check appears once, in `failed`. - **`partial`** is `true` when the run did not report on every member: Dafny never ran or wrote no results, `regen --no-verify`, or a `--filter-symbol` / `--filter-position` flag. Only a non-partial run can make a member disappear (ยง4). -- **`exit`** is the exit code `lsc` ends with. **`v`** is the record schema version; **`id`** is a random UUID; `lsc` (the version) gives context; fields such as the git commit or whether the run came from CI can be added in a later schema version if records leave the machine. +- **`exit`** is the exit code `lsc` ends with. **`v`** is the record schema version; **`id`** is a random UUID; `lsc` (the version, or `null` when it can't be read) gives context; fields such as the git commit or whether the run came from CI can be added in a later schema version if records leave the machine. - **`tsHash` / `dfyHash`** are the first 12 hex characters of the SHA-256 of the source `.ts` and of the proof `.dfy`. The `.ts` is hashed when the run starts. The `.dfy` is hashed when the run ends, because `check` may create it and `regen` may merge into it. **Snapshots.** On every run, `lsc` copies the `.ts` to `.lemmascript/blobs/.ts` unless that file already exists. Most runs during proof work leave the `.ts` unchanged, so they add nothing. The `.dfy` is not snapshotted, because labeling only needs to see what changed in the program and its spec. diff --git a/tools/src/lsc.ts b/tools/src/lsc.ts index db73c74..a9ab363 100755 --- a/tools/src/lsc.ts +++ b/tools/src/lsc.ts @@ -436,7 +436,7 @@ function runFile( // so an aborted run leaves no snapshot; each helper records the stage it detects. const logCmd = cmd === "check" || cmd === "regen" ? cmd : null; const log = logCmd && runLogOn - ? new RunLog({ logDir: resolveLogDir(absPath, configFile), cmd: logCmd, sourcePath: absPath, extraFlags, lscVersion: lscVersion() }) + ? new RunLog({ logDir: resolveLogDir(absPath, configFile), cmd: logCmd, sourcePath: absPath, extraFlags, lscVersion }) : undefined; if (cmd === "gen") { dafnyGen(genPath, dfyPath, text); return; } diff --git a/tools/src/run-log.ts b/tools/src/run-log.ts index c8bd842..232c3a7 100644 --- a/tools/src/run-log.ts +++ b/tools/src/run-log.ts @@ -42,7 +42,7 @@ export interface VerifyRecord { passed: string[]; tsHash: string | null; dfyHash: string | null; - lsc: string; + lsc: string | null; } export interface RunLogInit { @@ -50,7 +50,8 @@ export interface RunLogInit { cmd: "check" | "regen"; sourcePath: string; extraFlags?: string; - lscVersion: string; + /** Read when the record is written, so a version that can't be read never fails the run. */ + lscVersion: () => string; } /** @@ -212,7 +213,7 @@ export class RunLog { passed: results?.passed ?? [], tsHash: this.tsHash, dfyHash: safely(() => hashText(readFileSync(outcome.dfyPath, "utf8"))), - lsc: this.init.lscVersion, + lsc: safely(this.init.lscVersion), }; appendFileSync(path.join(dir, "runs.jsonl"), JSON.stringify(record) + "\n"); }); diff --git a/tools/tests/run-log.test.ts b/tools/tests/run-log.test.ts index 96ebed2..8def6cd 100644 --- a/tools/tests/run-log.test.ts +++ b/tools/tests/run-log.test.ts @@ -94,7 +94,7 @@ function verifyWithLog(root: string, opts: { extraFlags?: string; proof?: string const dfy = join(root, "a.dfy"); writeFileSync(source, "export const a = 1;\n"); writeFileSync(dfy, opts.proof ?? "lemma L() {}\n"); - const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, extraFlags: opts.extraFlags, lscVersion: "0" }); + const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, extraFlags: opts.extraFlags, lscVersion: () => "0" }); return dafnyVerify(dfy, root, undefined, opts.extraFlags, log); } @@ -105,7 +105,7 @@ function checkDiffWithLog(root: string, generated: string, proof: string): boole writeFileSync(source, ""); writeFileSync(gen, generated); writeFileSync(dfy, proof); - const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: "0" }); + const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: () => "0" }); return dafnyCheckDiff(gen, dfy, log); } @@ -123,7 +123,7 @@ function regenRecord(root: string, proof: string, next: string, opts: { base?: s writeFileSync(f.gen, generation(0)); writeFileSync(f.proof, proof); if (opts.base) writeFileSync(f.base, opts.base); - const log = new RunLog({ logDir: root, cmd: "regen", sourcePath: f.source, lscVersion: "0" }); + const log = new RunLog({ logDir: root, cmd: "regen", sourcePath: f.source, lscVersion: () => "0" }); const originalExit = process.exit; process.exit = ((code?: number) => { throw new ExitSignal(code); }) as typeof process.exit; try { @@ -267,7 +267,7 @@ test("finish appends one complete record and ignores later calls", () => { writeFileSync(source, "export const a = 1;\n"); const dfy = join(root, "src", "a.dfy"); writeFileSync(dfy, "lemma L() {}\n"); - const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: "9.9.9" }); + const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: () => "9.9.9" }); log.finish({ stage: "verify", exit: 1, dfyPath: dfy, results: { passed: ["a"], failed: ["L"] } }); log.finish({ stage: "ok", exit: 0, dfyPath: dfy }); const [r, ...rest] = records(root); @@ -299,9 +299,9 @@ test("a run without member results, or with a filter, is partial", () => { try { const source = join(root, "a.ts"); writeFileSync(source, ""); - new RunLog({ logDir: root, cmd: "regen", sourcePath: source, lscVersion: "0" }) + new RunLog({ logDir: root, cmd: "regen", sourcePath: source, lscVersion: () => "0" }) .finish({ stage: "diff", exit: 1, dfyPath: join(root, "missing.dfy") }); - new RunLog({ logDir: root, cmd: "check", sourcePath: source, extraFlags: "--filter-symbol=a", lscVersion: "0" }) + new RunLog({ logDir: root, cmd: "check", sourcePath: source, extraFlags: "--filter-symbol=a", lscVersion: () => "0" }) .finish({ stage: "ok", exit: 0, dfyPath: join(root, "missing.dfy"), results: { passed: ["a"], failed: [] } }); const [diff, filtered] = records(root); assert.equal(diff.partial, true); @@ -320,7 +320,7 @@ test("an unwritable log directory never throws", () => { writeFileSync(blocker, "a file, so nothing can be created beneath it"); const source = join(root, "a.ts"); writeFileSync(source, ""); - const log = new RunLog({ logDir: join(blocker, "sub"), cmd: "check", sourcePath: source, lscVersion: "0" }); + const log = new RunLog({ logDir: join(blocker, "sub"), cmd: "check", sourcePath: source, lscVersion: () => "0" }); assert.doesNotThrow(() => log.dafnyArgs()); assert.doesNotThrow(() => log.finish({ stage: "ok", exit: 0, dfyPath: source })); } finally { @@ -328,12 +328,26 @@ test("an unwritable log directory never throws", () => { } }); +test("a version that can't be read is recorded as null and never throws", () => { + const root = tempDir(); + try { + const source = join(root, "a.ts"); + writeFileSync(source, ""); + const unreadable = () => { throw new Error("ENOENT: no such file or directory, open 'package.json'"); }; + const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: unreadable }); + assert.doesNotThrow(() => log.finish({ stage: "ok", exit: 0, dfyPath: source })); + assert.equal(records(root)[0].lsc, null); + } finally { + rmSync(root, { recursive: true, force: true }); + } +}); + test("dafnyArgs points Dafny at a temporary text log that readResults parses", () => { const root = tempDir(); try { const source = join(root, "a.ts"); writeFileSync(source, ""); - const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: "0" }); + const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: () => "0" }); assert.equal(log.readResults(), null); const args = log.dafnyArgs(); assert.equal(args[0], "--log-format"); @@ -353,7 +367,7 @@ test("discard ends a run without a record and removes Dafny's temporary results try { const source = join(root, "a.ts"); writeFileSync(source, ""); - const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: "0" }); + const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: () => "0" }); const file = log.dafnyArgs()[1].replace(/^text;LogFileName=/, ""); const folder = join(file, ".."); assert.ok(existsSync(folder)); From a8edd5562913311732f14d5bde42eef1cc291b80 Mon Sep 17 00:00:00 2001 From: Canitas Date: Thu, 29 Oct 2026 20:33:31 -0700 Subject: [PATCH 2/2] refactor: read the version eagerly through safely --- tools/src/lsc.ts | 4 ++-- tools/src/run-log.ts | 7 +++---- tools/tests/run-log.test.ts | 27 +++++++++++++-------------- 3 files changed, 18 insertions(+), 20 deletions(-) diff --git a/tools/src/lsc.ts b/tools/src/lsc.ts index a9ab363..d387eea 100755 --- a/tools/src/lsc.ts +++ b/tools/src/lsc.ts @@ -21,7 +21,7 @@ import { emitDafnyFile, emittedNameMap } from "./dafny-emit.js"; import { dafnyGen, dafnyCheckDiff, dafnyVerify, dafnyRegen } from "./dafny-commands.js"; import { leanGen, leanCheck } from "./lean-commands.js"; import { runInfo, runTypedInfo, type TypedInfoDafny } from "./info-command.js"; -import { RunLog, resolveLogDir, runLogEnabled } from "./run-log.js"; +import { RunLog, resolveLogDir, runLogEnabled, safely } from "./run-log.js"; import { runRuns } from "./runs-command.js"; import { findUp, @@ -436,7 +436,7 @@ function runFile( // so an aborted run leaves no snapshot; each helper records the stage it detects. const logCmd = cmd === "check" || cmd === "regen" ? cmd : null; const log = logCmd && runLogOn - ? new RunLog({ logDir: resolveLogDir(absPath, configFile), cmd: logCmd, sourcePath: absPath, extraFlags, lscVersion }) + ? new RunLog({ logDir: resolveLogDir(absPath, configFile), cmd: logCmd, sourcePath: absPath, extraFlags, lscVersion: safely(lscVersion) }) : undefined; if (cmd === "gen") { dafnyGen(genPath, dfyPath, text); return; } diff --git a/tools/src/run-log.ts b/tools/src/run-log.ts index 232c3a7..488f3f1 100644 --- a/tools/src/run-log.ts +++ b/tools/src/run-log.ts @@ -50,8 +50,7 @@ export interface RunLogInit { cmd: "check" | "regen"; sourcePath: string; extraFlags?: string; - /** Read when the record is written, so a version that can't be read never fails the run. */ - lscVersion: () => string; + lscVersion: string | null; } /** @@ -116,7 +115,7 @@ export function hashText(text: string): string { return createHash("sha256").update(text).digest("hex").slice(0, 12); } -function safely(fn: () => T): T | null { +export function safely(fn: () => T): T | null { try { return fn(); } catch { @@ -213,7 +212,7 @@ export class RunLog { passed: results?.passed ?? [], tsHash: this.tsHash, dfyHash: safely(() => hashText(readFileSync(outcome.dfyPath, "utf8"))), - lsc: safely(this.init.lscVersion), + lsc: this.init.lscVersion, }; appendFileSync(path.join(dir, "runs.jsonl"), JSON.stringify(record) + "\n"); }); diff --git a/tools/tests/run-log.test.ts b/tools/tests/run-log.test.ts index 8def6cd..e30277b 100644 --- a/tools/tests/run-log.test.ts +++ b/tools/tests/run-log.test.ts @@ -8,7 +8,7 @@ import { tmpdir } from "node:os"; import { delimiter, join } from "node:path"; import { dafnyCheckDiff, dafnyRegen, dafnyVerify } from "../src/dafny-commands.ts"; import { - RunLog, ensureLogDir, hashText, isPartialRun, parseTextLog, readRecords, resolveLogDir, runLogEnabled, snapshotSource, + RunLog, ensureLogDir, hashText, isPartialRun, parseTextLog, readRecords, resolveLogDir, runLogEnabled, safely, snapshotSource, } from "../src/run-log.ts"; const posixOnly = { skip: process.platform === "win32" }; @@ -94,7 +94,7 @@ function verifyWithLog(root: string, opts: { extraFlags?: string; proof?: string const dfy = join(root, "a.dfy"); writeFileSync(source, "export const a = 1;\n"); writeFileSync(dfy, opts.proof ?? "lemma L() {}\n"); - const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, extraFlags: opts.extraFlags, lscVersion: () => "0" }); + const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, extraFlags: opts.extraFlags, lscVersion: "0" }); return dafnyVerify(dfy, root, undefined, opts.extraFlags, log); } @@ -105,7 +105,7 @@ function checkDiffWithLog(root: string, generated: string, proof: string): boole writeFileSync(source, ""); writeFileSync(gen, generated); writeFileSync(dfy, proof); - const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: () => "0" }); + const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: "0" }); return dafnyCheckDiff(gen, dfy, log); } @@ -123,7 +123,7 @@ function regenRecord(root: string, proof: string, next: string, opts: { base?: s writeFileSync(f.gen, generation(0)); writeFileSync(f.proof, proof); if (opts.base) writeFileSync(f.base, opts.base); - const log = new RunLog({ logDir: root, cmd: "regen", sourcePath: f.source, lscVersion: () => "0" }); + const log = new RunLog({ logDir: root, cmd: "regen", sourcePath: f.source, lscVersion: "0" }); const originalExit = process.exit; process.exit = ((code?: number) => { throw new ExitSignal(code); }) as typeof process.exit; try { @@ -267,7 +267,7 @@ test("finish appends one complete record and ignores later calls", () => { writeFileSync(source, "export const a = 1;\n"); const dfy = join(root, "src", "a.dfy"); writeFileSync(dfy, "lemma L() {}\n"); - const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: () => "9.9.9" }); + const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: "9.9.9" }); log.finish({ stage: "verify", exit: 1, dfyPath: dfy, results: { passed: ["a"], failed: ["L"] } }); log.finish({ stage: "ok", exit: 0, dfyPath: dfy }); const [r, ...rest] = records(root); @@ -299,9 +299,9 @@ test("a run without member results, or with a filter, is partial", () => { try { const source = join(root, "a.ts"); writeFileSync(source, ""); - new RunLog({ logDir: root, cmd: "regen", sourcePath: source, lscVersion: () => "0" }) + new RunLog({ logDir: root, cmd: "regen", sourcePath: source, lscVersion: "0" }) .finish({ stage: "diff", exit: 1, dfyPath: join(root, "missing.dfy") }); - new RunLog({ logDir: root, cmd: "check", sourcePath: source, extraFlags: "--filter-symbol=a", lscVersion: () => "0" }) + new RunLog({ logDir: root, cmd: "check", sourcePath: source, extraFlags: "--filter-symbol=a", lscVersion: "0" }) .finish({ stage: "ok", exit: 0, dfyPath: join(root, "missing.dfy"), results: { passed: ["a"], failed: [] } }); const [diff, filtered] = records(root); assert.equal(diff.partial, true); @@ -320,7 +320,7 @@ test("an unwritable log directory never throws", () => { writeFileSync(blocker, "a file, so nothing can be created beneath it"); const source = join(root, "a.ts"); writeFileSync(source, ""); - const log = new RunLog({ logDir: join(blocker, "sub"), cmd: "check", sourcePath: source, lscVersion: () => "0" }); + const log = new RunLog({ logDir: join(blocker, "sub"), cmd: "check", sourcePath: source, lscVersion: "0" }); assert.doesNotThrow(() => log.dafnyArgs()); assert.doesNotThrow(() => log.finish({ stage: "ok", exit: 0, dfyPath: source })); } finally { @@ -328,14 +328,13 @@ test("an unwritable log directory never throws", () => { } }); -test("a version that can't be read is recorded as null and never throws", () => { +test("a version that can't be read is recorded as null", () => { const root = tempDir(); try { const source = join(root, "a.ts"); writeFileSync(source, ""); - const unreadable = () => { throw new Error("ENOENT: no such file or directory, open 'package.json'"); }; - const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: unreadable }); - assert.doesNotThrow(() => log.finish({ stage: "ok", exit: 0, dfyPath: source })); + const lscVersion = safely((): string => { throw new Error("ENOENT: no such file or directory, open 'package.json'"); }); + new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion }).finish({ stage: "ok", exit: 0, dfyPath: source }); assert.equal(records(root)[0].lsc, null); } finally { rmSync(root, { recursive: true, force: true }); @@ -347,7 +346,7 @@ test("dafnyArgs points Dafny at a temporary text log that readResults parses", ( try { const source = join(root, "a.ts"); writeFileSync(source, ""); - const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: () => "0" }); + const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: "0" }); assert.equal(log.readResults(), null); const args = log.dafnyArgs(); assert.equal(args[0], "--log-format"); @@ -367,7 +366,7 @@ test("discard ends a run without a record and removes Dafny's temporary results try { const source = join(root, "a.ts"); writeFileSync(source, ""); - const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: () => "0" }); + const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: "0" }); const file = log.dafnyArgs()[1].replace(/^text;LogFileName=/, ""); const folder = join(file, ".."); assert.ok(existsSync(folder));