From 033499b1e63479b0dc2e6683dd64ec036724d56f Mon Sep 17 00:00:00 2001 From: Annie Vella Date: Thu, 1 Oct 2026 18:01:25 +1300 Subject: [PATCH 01/12] Add run-log design proposal --- DESIGN_RUN_LOG.md | 237 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 237 insertions(+) create mode 100644 DESIGN_RUN_LOG.md diff --git a/DESIGN_RUN_LOG.md b/DESIGN_RUN_LOG.md new file mode 100644 index 0000000..d8dc01c --- /dev/null +++ b/DESIGN_RUN_LOG.md @@ -0,0 +1,237 @@ +# DESIGN_RUN_LOG — Counting what verification caught + +**Status:** proposal; nothing is implemented in `lsc`. A stopgap wrapper on the `lemmascript-catch-log` branch of lemmascript-skills confirmed the Dafny CSV approach in §2 against `lsc` 0.6.1, passing the flag through `--extra-flags`. +**Date:** September 2026 + +## Goal + +When an agent writes LemmaScript code and proofs, the prover and claimcheck reject things along the way. Some rejections are real bugs in the TypeScript, some are specs that said the wrong thing, and many are ordinary proof work. We want honest counts of each, reported periodically over the life of a project. + +Asking the agent to keep a tally at the end of a session does not give honest counts. The agent's memory of the session is incomplete, and it tends to call every failed proof attempt a "bug caught". This design has `lsc` record every verification run itself, together with a snapshot of the source. A catch is then a fact derived from the record: something failed, and a later run passed. + +Labeling a catch as a code bug or a spec bug happens afterward, at report time. A reporting skill reads the log, looks at what changed in the source between the failing and the passing run, and labels each catch from that diff. The agent doing the work has no extra duties while it works. + +## Requirements + +1. **Mechanical first.** A catch exists only if the log shows a failure followed by a pass. +2. **Always on.** Every `lsc check`, `lsc regen`, and `lsc claimcheck` on a file is recorded, whoever runs it: an agent, a person, or CI. No wrapper, skill rule, or hook is needed for logging. +3. **No change to what the user sees.** Logging does not alter `lsc` output, exit codes, or generated files. Dafny's output still streams to the terminal while it runs. +4. **Invisible to git.** The log directory ignores itself, so it never shows up in `git status` and needs no `.gitignore` edit. +5. **Code and proof are kept apart.** The record shows whether the fix touched the `.ts` (the program or its spec) or only the `.dfy` (the proof). The two are reported separately. +6. **Labels are made after the fact, from evidence.** The log keeps enough to label a catch later without the working agent's memory: the source before and after the fix, and the error that preceded it. +7. **Claimcheck is counted the same way, and is not modified.** `lsc` reads the report file that claimcheck already writes. + +## 1. Where the log lives + +Logging is on by default. A project turns it off with a config-only entry in the registry (see DESIGN_CONFIG.md §2): + +```json +{ + "run-log": false +} +``` + +`LSC_RUN_LOG=0` turns it off for a single run. + +The log lives in `.lemmascript/` in the directory that holds the selected `lemmascript.json`. Without a config file, it goes in the git repository root, or in the current working directory outside a repository. When `lsc` creates the directory, it writes `.lemmascript/.gitignore` containing `*`, so git ignores the whole directory without any change to the project's own `.gitignore`. + +``` +.lemmascript/ + .gitignore contains "*" + runs.jsonl one record per run, plus label and report records + blobs/.ts source snapshots, one file per distinct version + reports/ dated reports, one file per `lsc runs report` (§6) +``` + +## 2. What `lsc check` and `lsc regen` record + +`dafnyVerify` (`tools/src/dafny-commands.ts`) gains one extra Dafny argument when logging is on: + +``` +--log-format csv;LogFileName=/verify.csv +``` + +Dafny writes one row per verified member and still prints its normal output. Here is the real output for a two-lemma file, one lemma good and one bad, run with Dafny 4.11: + +``` +TestResult.DisplayName,TestResult.Outcome,TestResult.Duration,TestResult.ResourceCount,RandomSeed +bad (correctness),Failed,00:00:00.0356494,3134,0 +good (correctness),Passed,00:00:00.0256170,3017,0 +``` + +With this flag, Dafny also prints a `Results File: ` line, which `lsc` removes from the output it passes on. + +To keep the error text, `lsc` runs Dafny with its output piped rather than inherited and forwards each chunk to the terminal as it arrives. The output still streams, and `lsc` keeps a copy. After Dafny exits, `lsc` reads the CSV and appends one record: + +```json +{"type":"verify","id":"r_7f3a","ts":"2026-09-30T21:14:02Z", + "cmd":"check","file":"src/domain.ts","stage":"verify","exit":4, + "failed":["applyDiscount_ensures"],"passed":["clamp","clamp_ensures","applyDiscount"], + "tsHash":"9c1e04b2d7aa","dfyHash":"41d0f93be812", + "errors":["domain.dfy(41,2): Error: a postcondition could not be proved on this return path", "..."]} +``` + +- **`stage`** tells where the run stopped. `diff` means the additions-only check failed, so Dafny never ran. `resolve` means Dafny exited with a parse or resolution error and wrote no CSV rows. `conflict` means a `regen` merge conflicted. `verify` means Dafny ran and wrote rows. `ok` means everything passed. +- **`failed` / `passed`** are the member names with Dafny's ` (correctness)` / ` (well-formedness)` suffix removed. A member that fails on both counts appears once. +- **`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 after Dafny exits, because `check` may create it and `regen` may merge into it, and the post-run file is the one Dafny verified. +- **`errors`** holds Dafny's `Error:` lines and their related-location lines, capped at 40 lines. It is present only on failing runs. + +**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. + +## 3. What `lsc claimcheck` records + +Claimcheck already writes `.guarantees.json` next to the source, or under `--out`. Each entry in it has a function name, the contract text (`requirement`), the formal `spec`, a `status` of `confirmed`, `disputed`, or `unchecked`, and, for disputes, a `discrepancy` and a `backTranslation`. + +After claimcheck finishes, `lsc` reads that file, snapshots the `.ts`, and appends one record. In the single-file branch this happens after the dynamic `import` resolves; in the batch branch it happens after each `execFileSync`. `lsc` works out the report path from the same `--out` argument it forwards. + +```json +{"type":"claimcheck","id":"r_7f3b","ts":"2026-09-30T21:20:44Z", + "file":"src/domain.ts","tsHash":"9c1e04b2d7aa", + "results":[ + {"fn":"applyDiscount","status":"disputed","contractHash":"5b21","specHash":"e0c7", + "weakeningType":"missing-bound","discrepancy":"The spec bounds the result below but not above."} + ]} +``` + +`specHash` covers `requires` and `ensures` together, since a dispute can be resolved by changing either. Hashing the contract text and the spec separately lets the report tell, without any judgment, whether a dispute was resolved by changing the prose or by changing the spec. + +## 4. From runs to catches + +A new subcommand reads the log and derives the catches: + +```sh +npx lsc runs # everything not yet covered by a report +npx lsc runs --all # the whole log, ignoring past reports +npx lsc runs --json # machine-readable, with labeling evidence (combines with --all) +npx lsc runs report # write a dated report of everything not yet reported (§6) +``` + +There are no sessions. `lsc runs` always derives catches from the whole log, because a failure can be fixed days after it happened, and then shows only what falls after the most recent report. + +**A verify catch** is a member `M` in file `F` that appears in `failed` in some run, and in `passed` in the first later run of `F`. Its kind comes from comparing the hashes of the two runs: + +| `.ts` changed | `.dfy` changed | Kind | +|---|---|---| +| yes | either | `source-fix`: the program or its spec changed. It is labeled at report time. | +| no | yes | `proof`: proof work only. This is not counted as a bug. | +| no | no | `flaky`: the same inputs gave a different result, usually a timeout. | + +**A claimcheck catch** is a function that is `disputed` in some run and `confirmed` in the first later run: + +| contract changed | spec changed | Kind | +|---|---|---| +| yes | no | `contract-fixed`: the prose claimed something the spec did not say. | +| no | yes | `spec-fixed`: the spec was weaker than the claim. | +| yes | yes | `both-fixed` | +| no | no | `flaky`: claimcheck's LLM step changed its verdict on unchanged input. | + +A failure that has no later pass yet is **open**. If a member disappears from later runs because it was renamed or deleted, the failure is reported as **dropped**, never as a catch. + +Each catch has an ID, formed from the failing run and the member name, such as `r_7f3a:applyDiscount_ensures`. + +**Evidence for labeling.** In `--json` output, each `source-fix` catch carries the unified diff of the `.ts` between the two runs' snapshots, the failing run's `errors`, and a mechanical `change` hint: + +| `change` | Meaning | Likely label | +|---|---|---| +| `annotations-only` | Every changed line is a `//@` line. | `spec-bug` | +| `code-only` | No changed line is a `//@` line. | `impl-bug` | +| `mixed` | Both kinds of line changed. | Needs judgment. | + +The hint is a starting point, not a label. A `code-only` diff can still be an unrelated edit in the same file. + +## 5. Labels at report time + +Only `source-fix` catches need judgment, because a hash cannot tell a fixed bug from a tightened spec. That judgment is made when a report is requested, not while the work happens. + +A reporting skill, `lemmascript-catch-report`, does it. It is meant to run in a clean agent with no stake in the work, in the same way `lemmascript-proof-review` does. The skill: + +1. Runs `lsc runs --json` to get every catch not yet covered by a report. +2. For each unlabeled `source-fix` catch, reads the diff, the error that preceded it, and the `change` hint, and records a label: + + ```sh + npx lsc runs label r_7f3a:applyDiscount_ensures impl-bug "discount could exceed subtotal" + ``` + +3. Runs `lsc runs report` to write the dated report, then relays its counts and the `impl-bug` and `spec-bug` catches with their notes. + +The labels for a `source-fix` catch are `impl-bug` (the TypeScript computed the wrong thing), `spec-bug` (the `requires` or `ensures` was wrong), and `not-a-bug` (the `.ts` changed for another reason, such as an unrelated edit in the same file). When one change fixed both code and spec, the label is `impl-bug`. `lsc runs label` refuses an ID that is not in the log and a label that does not fit the catch. The label is appended as its own record, and a later label for the same catch replaces an earlier one: + +```json +{"type":"label","catch":"r_7f3a:applyDiscount_ensures","label":"impl-bug","note":"discount could exceed subtotal","ts":"..."} +``` + +Open claimcheck disputes are not labeled by the agent. A dispute is an intent question for the user, so the report lists open disputes with claimcheck's discrepancy text. If the user decides one is a false positive, it is recorded with the label `false-positive` and the user's reason. + +## 6. Dated reports + +`lsc runs report` writes `.lemmascript/reports/.md`, for example `reports/2026-09-30T2247.md`, and appends a marker to the log: + +```json +{"type":"report","id":"rep_2026-09-30T2247","ts":"2026-09-30T22:47:10Z","through":"r_9c2e","file":"reports/2026-09-30T2247.md"} +``` + +`through` is the last run the report covers. The next report covers the runs after it, so each run is reported exactly once. A run appended while a report is being written falls into the next report. + +A report's window decides what it counts: + +- **A catch** is counted in the report whose window contains its **passing** run. A failure from before the last report that is fixed now is counted now, and the report shows the date of the original failure. +- **Open failures** are listed in every report while they stay open, with the date each one first failed. They are a current state, not a count, so listing them again is not double counting. +- **Dropped failures** are counted in the report whose window contains the run where the member disappeared. + +A report is a snapshot. Labels added or changed later do not rewrite it, and they show up in the next report only if that report covers the catch. To relabel an already-reported catch, record the label and run `lsc runs --all`. + +`lsc runs` with no argument prints the same layout for the runs not yet reported, without writing a file or a marker. The mechanical counts come first and the labeled counts after them, so a reader can see which numbers depend on judgment: + +``` +report 2026-09-30 22:47 (runs 2026-09-28 14:02 → 2026-09-30 22:41, 31 runs, 3 files) +previous report 2026-09-28 13:55 + +verify: 14 fixed, 2 open (1 since 2026-09-26), 1 dropped + source-fix 5 (impl-bug 2, spec-bug 2, not-a-bug 0, unlabeled 1) + proof 8 + flaky 1 + diff-check 3 additions-only violations + +claimcheck: 5 resolved, 1 open (1 marked false-positive) + spec-fixed 2 + contract-fixed 2 + both-fixed 0 + flaky 1 + +impl-bug r_7f3a:applyDiscount_ensures src/domain.ts failed 2026-09-29 + discount could exceed subtotal +... +``` + +The report file ends with one line per catch: its kind, label, file, failure date, and note. The illustration above is a mock-up of the intended layout. Real numbers only come from a real log. + +## 7. Limits + +- **Only runs through `lsc` are recorded.** A bare `dafny verify --filter-symbol=...` is invisible to the log. The `lemmascript` skill already tells agents to finish with `lsc check`, so the passing run is recorded even when they iterate on a single lemma with bare Dafny. +- **Single-lemma iteration is compressed.** Ten attempts with bare Dafny followed by one `lsc check` show up as a single failure and a single pass. The log counts catches, not attempts. +- **The `.ts` hash covers the whole file.** If an unrelated function changed between the failing and passing runs, a proof-only fix is reported as `source-fix`. The diff shows this, and the labeler marks it `not-a-bug`. Hashing each function's extracted IR would remove the case, and could be added later. +- **The labeler sees evidence, not intent.** It has the diff and the error, but not the working agent's reasoning. For telling a code bug from a spec bug this is usually enough; the note records what the labeler concluded. +- **Claimcheck verdicts are not deterministic.** That is why `flaky` is a separate row and is never counted as a fix. +- **Reports live in the ignored log directory.** Deleting `.lemmascript/` deletes them too. A project that wants to keep reports copies them out or commits them deliberately. +- **Snapshots are never pruned automatically.** They are small text files, and identical versions are stored once. Deleting `.lemmascript/` resets the log. +- **The Lean backend is out of scope.** `lsc check --backend=lean` is not recorded in this version. + +## 8. Implementation + +| File | Change | +|---|---| +| `tools/src/config.ts` | Add a `run-log` registry entry (boolean, default `true`, config-only). | +| `tools/src/run-log.ts` (new) | Create `.lemmascript/` with its `.gitignore`, append records, hash and snapshot files, read the Dafny CSV, extract error lines, derive catches, compute diffs and `change` hints, write labels, write dated reports and their markers. | +| `tools/src/dafny-commands.ts` | `dafnyVerify` and `dafnyRegen` take an optional log context. When it is present, they add `--log-format`, pipe and forward Dafny's output instead of inheriting it, and append a record after Dafny exits. `dafnyCheckDiff` failures are recorded as `stage: "diff"`. | +| `tools/src/lsc.ts` | Pass the log context from resolved options. Record claimcheck results in both branches. Add the `runs`, `runs label`, and `runs report` subcommands. | +| `tools/fixtures/` | One fixture that goes fail → proof fix → pass, one that goes fail → code fix → pass (`code-only`), and one that goes fail → annotation fix → pass (`annotations-only`), checking the derived kinds and hints. | +| `lemmascript-catch-report` skill (new, in lemmascript-skills) | Label unlabeled `source-fix` catches from `lsc runs --json` evidence, list open claimcheck disputes for the user, and write the report. | + +The `lemmascript` skill needs no change for logging. The counting logic lives in `lsc`, where it has tests, and the skill only applies judgment on top of it. + +## Open questions + +1. Should `lsc runs` also read benchmark harness logs, so that benchmark write-ups can quote catch counts directly? +2. Is per-function IR hashing (§7, third limit) worth doing in the first version? It would also make the diff shown to the labeler smaller. +3. Should the `.dfy` be snapshotted too, so a report can show what proof work each `proof` catch took? +4. Should reports be written somewhere tracked by git by default, so they are kept and shared, instead of inside `.lemmascript/`? From 1152f3d8b39ac15503b065bce78b5bbd447a0220 Mon Sep 17 00:00:00 2001 From: Annie Vella Date: Mon, 5 Oct 2026 12:01:27 +1300 Subject: [PATCH 02/12] add run-log config option --- SPEC.md | 1 + tools/src/config.ts | 6 ++++++ tools/tests/config.test.ts | 9 ++++++++- 3 files changed, 15 insertions(+), 1 deletion(-) diff --git a/SPEC.md b/SPEC.md index 622a13f..753db23 100644 --- a/SPEC.md +++ b/SPEC.md @@ -1392,6 +1392,7 @@ it; absent means current behavior. Unknown keys and bad values are errors. | `proof-dir` | relative path | source directory | no (Dafny only) | | `string-semantics` | `unicode-scalar` \| `javascript-utf16` | `unicode-scalar` | yes (Dafny only) | | `dafny-library` | `stdlib` \| `local` | `stdlib` | yes (Dafny only) | +| `run-log` | boolean | `true` | no (Dafny only) | Eligible settings use `//@ option ` before the first source statement. File values override project values; duplicates are errors. diff --git a/tools/src/config.ts b/tools/src/config.ts index 0b8b402..c76da25 100644 --- a/tools/src/config.ts +++ b/tools/src/config.ts @@ -45,6 +45,12 @@ export const OPTION_SPECS = { fileOverride: true, description: "Use Dafny's standard library or generated local helpers for collection operations.", }, + "run-log": { + type: "boolean", + default: true, + fileOverride: false, + description: "Record lsc check and regen runs in .lemmascript/.", + }, } as const; type OptionSpecs = typeof OPTION_SPECS; diff --git a/tools/tests/config.test.ts b/tools/tests/config.test.ts index 58714e7..f99ca68 100644 --- a/tools/tests/config.test.ts +++ b/tools/tests/config.test.ts @@ -145,10 +145,11 @@ for (const [directive, message] of [ ["option", "expected //@ option "], ["option safe-slice", "expected //@ option "], ["option safe-slice true extra", "expected //@ option "], - ["option missing true", "unknown option 'missing' (known options: extern-default, safe-slice, proof-dir, string-semantics, dafny-library)"], + ["option missing true", "unknown option 'missing' (known options: extern-default, safe-slice, proof-dir, string-semantics, dafny-library, run-log)"], ["option safe-slice yes", "option 'safe-slice' must be true or false"], ["option extern-default invalid", "option 'extern-default' must be one of: pure, impure"], ["option proof-dir proofs", "option 'proof-dir' is config-only"], + ["option run-log false", "option 'run-log' is config-only"], ]) { test(`still rejects invalid directive: ${directive}`, () => { assert.throws( @@ -230,3 +231,9 @@ for (const [key, value] of [["string-semantics", "javascript-utf16"], ["dafny-li assert.throws(() => parseFileOptions("const value = 1;\n" + directive, "example.ts"), /before the first source statement/); }); } + +test("run-log defaults on and can be turned off in lemmascript.json", () => { + assert.equal(resolveOptions({}, "lemmascript.json")["run-log"], true); + const options = resolveOptions(validateOptions({ "run-log": false }, "lemmascript.json"), "lemmascript.json"); + assert.equal(options["run-log"], false); +}); From e377720bc8d66922d43c76158d3e05b3748670ec Mon Sep 17 00:00:00 2001 From: Annie Vella Date: Mon, 5 Oct 2026 12:20:28 +1300 Subject: [PATCH 03/12] parse Dafny text logs and resolve the run log location --- tools/src/run-log.ts | 61 ++++++++++++++++++++++++++++ tools/tests/run-log.test.ts | 81 +++++++++++++++++++++++++++++++++++++ 2 files changed, 142 insertions(+) create mode 100644 tools/src/run-log.ts create mode 100644 tools/tests/run-log.test.ts diff --git a/tools/src/run-log.ts b/tools/src/run-log.ts new file mode 100644 index 0000000..ef48212 --- /dev/null +++ b/tools/src/run-log.ts @@ -0,0 +1,61 @@ +/** + * Run log: record each Dafny `lsc check` / `lsc regen` run in + * `.lemmascript/runs.jsonl`, with a snapshot of the source (DESIGN_RUN_LOG.md). + * Logging must never change lsc's output or exit code, so every filesystem + * step is best-effort and swallows its own errors. + */ + +import { createHash } from "crypto"; +import path from "path"; +import { findUp } from "./config.js"; + +export interface MemberResults { + passed: string[]; + failed: string[]; +} + +/** + * Parse Dafny's `--log-format text` file. Each member gets one entry per + * check (`correctness`, `well-formedness`); it passes only if every check's + * outcome is `Correct`. + */ +export function parseTextLog(text: string): MemberResults { + const seen = new Set(); + const failed = new Set(); + for (const m of text.matchAll(/^Results for (.+?) \([a-z-]+\)\r?\n\s+Overall outcome: (\S+)/gm)) { + seen.add(m[1]); + if (m[2] !== "Correct") failed.add(m[1]); + } + return { + passed: [...seen].filter(name => !failed.has(name)).sort(), + failed: [...failed].sort(), + }; +} + +/** First 12 hex characters of the SHA-256 of `text`. */ +export function hashText(text: string): string { + return createHash("sha256").update(text).digest("hex").slice(0, 12); +} + +/** A filtered Dafny run verifies only some members, so absences mean nothing. */ +export function isPartialRun(extraFlags: string | undefined): boolean { + return /--filter-(symbol|position)\b/.test(extraFlags ?? ""); +} + +/** + * `LSC_RUN_LOG=false` turns logging off for one run; `true` or unset leaves it + * to the config. Like lemmascript.json, any other value is an error. + */ +export function runLogEnabled(option: boolean, env: NodeJS.ProcessEnv = process.env): boolean { + const value = env.LSC_RUN_LOG; + if (value === undefined || value === "" || value === "true") return option; + if (value === "false") return false; + throw new Error(`LSC_RUN_LOG must be true or false (got ${JSON.stringify(value)})`); +} + +/** The selected lemmascript.json's directory, else the source's git root, else cwd. */ +export function resolveLogDir(sourcePath: string, configFile: string | null): string { + if (configFile) return path.dirname(path.resolve(configFile)); + const git = findUp(".git", sourcePath); + return git ? path.dirname(git) : process.cwd(); +} diff --git a/tools/tests/run-log.test.ts b/tools/tests/run-log.test.ts new file mode 100644 index 0000000..507936d --- /dev/null +++ b/tools/tests/run-log.test.ts @@ -0,0 +1,81 @@ +import { test } from "node:test"; +import assert from "node:assert/strict"; +import { mkdirSync, mkdtempSync, realpathSync, rmSync, writeFileSync } from "node:fs"; +import { tmpdir } from "node:os"; +import { join } from "node:path"; +import { hashText, isPartialRun, parseTextLog, resolveLogDir, runLogEnabled } from "../src/run-log.ts"; + +function tempDir(): string { + return realpathSync(mkdtempSync(join(tmpdir(), "lsc-run-log-test-"))); +} + +// Trimmed from real Dafny 4.11 `--log-format text` output for a broken arraySum. +const TEXT_LOG = ` +Results for sumTo (well-formedness) + Overall outcome: Correct + Overall time: 00:00:00.0240667 + +Results for arraySum (well-formedness) + Overall outcome: Correct + +Results for arraySum (correctness) + Overall outcome: Errors +`; + +test("parseTextLog lists each member once, failed if any check failed", () => { + assert.deepEqual(parseTextLog(TEXT_LOG), { passed: ["sumTo"], failed: ["arraySum"] }); +}); + +test("parseTextLog treats any outcome other than Correct as a failure", () => { + const log = "Results for slow (correctness)\n Overall outcome: TimedOut\n"; + assert.deepEqual(parseTextLog(log), { passed: [], failed: ["slow"] }); +}); + +test("parseTextLog returns empty lists for a log with no results", () => { + assert.deepEqual(parseTextLog(""), { passed: [], failed: [] }); +}); + +test("hashText is a stable 12-character hex prefix", () => { + assert.equal(hashText("abc"), "ba7816bf8f01"); + assert.match(hashText("anything"), /^[0-9a-f]{12}$/); +}); + +test("filtered Dafny runs are partial", () => { + assert.equal(isPartialRun(undefined), false); + assert.equal(isPartialRun("--isolate-assertions"), false); + assert.equal(isPartialRun("--filter-symbol=foo"), true); + assert.equal(isPartialRun("--isolate-assertions --filter-position=x.dfy:3"), true); +}); + +test("LSC_RUN_LOG=false turns logging off for one run; true or unset defers to config", () => { + assert.equal(runLogEnabled(true, {}), true); + assert.equal(runLogEnabled(false, {}), false); + assert.equal(runLogEnabled(true, { LSC_RUN_LOG: "false" }), false); + assert.equal(runLogEnabled(true, { LSC_RUN_LOG: "true" }), true); + assert.equal(runLogEnabled(false, { LSC_RUN_LOG: "true" }), false); + assert.equal(runLogEnabled(true, { LSC_RUN_LOG: "" }), true); +}); + +test("LSC_RUN_LOG accepts only true or false, like lemmascript.json", () => { + for (const value of ["0", "1", "no", "FALSE"]) { + assert.throws(() => runLogEnabled(true, { LSC_RUN_LOG: value }), /LSC_RUN_LOG must be true or false/); + } +}); + +test("the log lives beside lemmascript.json, else at the git root, else in cwd", () => { + const root = tempDir(); + try { + mkdirSync(join(root, "repo", ".git"), { recursive: true }); + mkdirSync(join(root, "repo", "src"), { recursive: true }); + const source = join(root, "repo", "src", "a.ts"); + writeFileSync(source, ""); + const config = join(root, "repo", "src", "lemmascript.json"); + assert.equal(resolveLogDir(source, config), join(root, "repo", "src")); + assert.equal(resolveLogDir(source, null), join(root, "repo")); + const loose = join(root, "loose.ts"); + writeFileSync(loose, ""); + assert.equal(resolveLogDir(loose, null), process.cwd()); + } finally { + rmSync(root, { recursive: true, force: true }); + } +}); From cf3b2fa62c15f7b83bdedc0877e8061e2227be29 Mon Sep 17 00:00:00 2001 From: Annie Vella Date: Mon, 5 Oct 2026 13:09:51 +1300 Subject: [PATCH 04/12] write run log records and source snapshots --- tools/src/run-log.ts | 139 ++++++++++++++++++++++++++++++++++-- tools/tests/run-log.test.ts | 128 ++++++++++++++++++++++++++++++++- 2 files changed, 261 insertions(+), 6 deletions(-) diff --git a/tools/src/run-log.ts b/tools/src/run-log.ts index ef48212..c45431b 100644 --- a/tools/src/run-log.ts +++ b/tools/src/run-log.ts @@ -1,11 +1,14 @@ /** * Run log: record each Dafny `lsc check` / `lsc regen` run in - * `.lemmascript/runs.jsonl`, with a snapshot of the source (DESIGN_RUN_LOG.md). - * Logging must never change lsc's output or exit code, so every filesystem - * step is best-effort and swallows its own errors. + * `.lemmascript/runs.jsonl`, with a snapshot of the source, so that a later + * report can tell which failures were fixed and whether the fix changed the + * program or only the proof. Logging must never change lsc's output or exit + * code, so every filesystem step is best-effort and swallows its own errors. */ -import { createHash } from "crypto"; +import { createHash, randomUUID } from "crypto"; +import { appendFileSync, existsSync, mkdirSync, mkdtempSync, readFileSync, rmSync, writeFileSync } from "fs"; +import { tmpdir } from "os"; import path from "path"; import { findUp } from "./config.js"; @@ -59,3 +62,131 @@ export function resolveLogDir(sourcePath: string, configFile: string | null): st const git = findUp(".git", sourcePath); return git ? path.dirname(git) : process.cwd(); } + +export const RUN_LOG_SCHEMA_VERSION = 1; + +/** + * Where a run stopped: `diff` (additions-only check failed, Dafny never ran), + * `conflict` (regen merge conflict), `resolve` (Dafny produced no results), + * `verify` (Dafny reported failures), or `ok`. + */ +export type RunStage = "ok" | "verify" | "resolve" | "diff" | "conflict"; + +export interface VerifyRecord { + v: number; + type: "verify"; + id: string; + ts: string; + cmd: "check" | "regen"; + file: string; + stage: RunStage; + exit: number; + partial: boolean; + failed: string[]; + passed: string[]; + tsHash: string | null; + dfyHash: string | null; + lsc: string; + ci: boolean; +} + +export interface RunLogInit { + logDir: string; + cmd: "check" | "regen"; + sourcePath: string; + extraFlags?: string; + lscVersion: string; +} + +function safely(fn: () => T): T | null { + try { + return fn(); + } catch { + return null; + } +} + +/** Create `/.lemmascript/` with a `.gitignore` that ignores the whole directory. */ +export function ensureLogDir(logDir: string): string { + const dir = path.join(logDir, ".lemmascript"); + mkdirSync(path.join(dir, "blobs"), { recursive: true }); + const ignore = path.join(dir, ".gitignore"); + if (!existsSync(ignore)) writeFileSync(ignore, "*\n"); + return dir; +} + +/** Store the source as `blobs/.ts` unless that version is already there. */ +export function snapshotSource(dir: string, text: string): string { + const hash = hashText(text); + const blob = path.join(dir, "blobs", `${hash}.ts`); + if (!existsSync(blob)) writeFileSync(blob, text); + return hash; +} + +/** + * One verification run. `lsc.ts` creates it before generating; the code path + * where the run ends calls `finish` exactly once (later calls are ignored). + */ +export class RunLog { + private readonly dir: string | null; + private readonly tsHash: string | null; + private readonly startedAt = new Date().toISOString(); + private textLogDir: string | null = null; + private done = false; + + constructor(private readonly init: RunLogInit) { + this.dir = safely(() => ensureLogDir(init.logDir)); + this.tsHash = this.dir === null ? null + : safely(() => snapshotSource(this.dir!, readFileSync(init.sourcePath, "utf8"))); + } + + private textLogPath(): string { + return path.join(this.textLogDir!, "verify.txt"); + } + + /** Extra Dafny arguments that write member outcomes to a temporary text log. */ + dafnyArgs(): string[] { + this.textLogDir = safely(() => mkdtempSync(path.join(tmpdir(), "lsc-run-log-"))); + return this.textLogDir === null ? [] : ["--log-format", `text;LogFileName=${this.textLogPath()}`]; + } + + /** Member outcomes from Dafny's text log, or null when Dafny wrote none. */ + readResults(): MemberResults | null { + if (this.textLogDir === null) return null; + return safely(() => parseTextLog(readFileSync(this.textLogPath(), "utf8"))); + } + + /** Append this run's record. Never throws; only the first call writes. */ + finish(outcome: { stage: RunStage; exit: number; dfyPath: string; results?: MemberResults | null }): void { + if (this.done) return; + this.done = true; + const dir = this.dir; + if (dir !== null) { + safely(() => { + const results = outcome.results ?? null; + const record: VerifyRecord = { + v: RUN_LOG_SCHEMA_VERSION, + type: "verify", + id: randomUUID(), + ts: this.startedAt, + cmd: this.init.cmd, + file: path.relative(this.init.logDir, this.init.sourcePath).split(path.sep).join("/"), + stage: outcome.stage, + exit: outcome.exit, + partial: results === null || isPartialRun(this.init.extraFlags), + failed: results?.failed ?? [], + passed: results?.passed ?? [], + tsHash: this.tsHash, + dfyHash: safely(() => hashText(readFileSync(outcome.dfyPath, "utf8"))), + lsc: this.init.lscVersion, + ci: Boolean(process.env.CI), + }; + appendFileSync(path.join(dir, "runs.jsonl"), JSON.stringify(record) + "\n"); + }); + } + if (this.textLogDir !== null) { + const tmp = this.textLogDir; + safely(() => rmSync(tmp, { recursive: true, force: true })); + } + } +} diff --git a/tools/tests/run-log.test.ts b/tools/tests/run-log.test.ts index 507936d..e0d2d9f 100644 --- a/tools/tests/run-log.test.ts +++ b/tools/tests/run-log.test.ts @@ -1,9 +1,11 @@ import { test } from "node:test"; import assert from "node:assert/strict"; -import { mkdirSync, mkdtempSync, realpathSync, rmSync, writeFileSync } from "node:fs"; +import { existsSync, mkdirSync, mkdtempSync, readFileSync, realpathSync, rmSync, writeFileSync } from "node:fs"; import { tmpdir } from "node:os"; import { join } from "node:path"; -import { hashText, isPartialRun, parseTextLog, resolveLogDir, runLogEnabled } from "../src/run-log.ts"; +import { + RunLog, ensureLogDir, hashText, isPartialRun, parseTextLog, resolveLogDir, runLogEnabled, snapshotSource, +} from "../src/run-log.ts"; function tempDir(): string { return realpathSync(mkdtempSync(join(tmpdir(), "lsc-run-log-test-"))); @@ -79,3 +81,125 @@ test("the log lives beside lemmascript.json, else at the git root, else in cwd", rmSync(root, { recursive: true, force: true }); } }); + +function records(logDir: string): any[] { + return readFileSync(join(logDir, ".lemmascript", "runs.jsonl"), "utf8") + .trim().split("\n").map(line => JSON.parse(line)); +} + +test("ensureLogDir creates a self-ignoring directory and keeps an edited .gitignore", () => { + const root = tempDir(); + try { + const dir = ensureLogDir(root); + assert.equal(dir, join(root, ".lemmascript")); + assert.equal(readFileSync(join(dir, ".gitignore"), "utf8"), "*\n"); + writeFileSync(join(dir, ".gitignore"), "*\n# kept\n"); + ensureLogDir(root); + assert.equal(readFileSync(join(dir, ".gitignore"), "utf8"), "*\n# kept\n"); + } finally { + rmSync(root, { recursive: true, force: true }); + } +}); + +test("snapshotSource stores each distinct version once, named by its hash", () => { + const root = tempDir(); + try { + const dir = ensureLogDir(root); + const hash = snapshotSource(dir, "export const a = 1;\n"); + assert.equal(hash, hashText("export const a = 1;\n")); + assert.equal(readFileSync(join(dir, "blobs", `${hash}.ts`), "utf8"), "export const a = 1;\n"); + assert.equal(snapshotSource(dir, "export const a = 1;\n"), hash); + } finally { + rmSync(root, { recursive: true, force: true }); + } +}); + +test("finish appends one complete record and ignores later calls", () => { + const root = tempDir(); + try { + const source = join(root, "src", "a.ts"); + mkdirSync(join(root, "src")); + 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" }); + 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); + assert.equal(rest.length, 0); + assert.deepEqual(Object.keys(r).sort(), [ + "ci", "cmd", "dfyHash", "exit", "failed", "file", "id", "lsc", "partial", "passed", "stage", "ts", "tsHash", "type", "v", + ]); + assert.equal(r.v, 1); + assert.equal(r.type, "verify"); + assert.match(r.id, /^[0-9a-f-]{36}$/); + assert.equal(r.cmd, "check"); + assert.equal(r.file, "src/a.ts"); + assert.equal(r.stage, "verify"); + assert.equal(r.exit, 1); + assert.equal(r.partial, false); + assert.deepEqual(r.failed, ["L"]); + assert.deepEqual(r.passed, ["a"]); + assert.equal(r.tsHash, hashText("export const a = 1;\n")); + assert.equal(r.dfyHash, hashText("lemma L() {}\n")); + assert.equal(r.lsc, "9.9.9"); + assert.equal(typeof r.ci, "boolean"); + assert.ok(existsSync(join(root, ".lemmascript", "blobs", `${r.tsHash}.ts`))); + } finally { + rmSync(root, { recursive: true, force: true }); + } +}); + +test("a run without member results, or with a filter, is partial", () => { + const root = tempDir(); + try { + const source = join(root, "a.ts"); + writeFileSync(source, ""); + 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" }) + .finish({ stage: "ok", exit: 0, dfyPath: join(root, "missing.dfy"), results: { passed: ["a"], failed: [] } }); + const [diff, filtered] = records(root); + assert.equal(diff.partial, true); + assert.deepEqual(diff.passed, []); + assert.equal(diff.dfyHash, null); + assert.equal(filtered.partial, true); + } finally { + rmSync(root, { recursive: true, force: true }); + } +}); + +test("an unwritable log directory never throws", () => { + const root = tempDir(); + try { + const blocker = join(root, "blocker"); + 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" }); + assert.doesNotThrow(() => log.dafnyArgs()); + assert.doesNotThrow(() => log.finish({ stage: "ok", exit: 0, dfyPath: source })); + } 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" }); + assert.equal(log.readResults(), null); + const args = log.dafnyArgs(); + assert.equal(args[0], "--log-format"); + const file = args[1].replace(/^text;LogFileName=/, ""); + assert.equal(log.readResults(), null); + writeFileSync(file, TEXT_LOG); + assert.deepEqual(log.readResults(), { passed: ["sumTo"], failed: ["arraySum"] }); + log.finish({ stage: "verify", exit: 1, dfyPath: source, results: log.readResults() }); + assert.equal(existsSync(file), false); + } finally { + rmSync(root, { recursive: true, force: true }); + } +}); From 7d11246ba65a9dde499508983e0a9ddfc990d735 Mon Sep 17 00:00:00 2001 From: Annie Vella Date: Mon, 5 Oct 2026 15:18:12 +1300 Subject: [PATCH 05/12] record lsc check runs in the run log --- tools/src/dafny-commands.ts | 22 +++++- tools/src/lsc.ts | 12 +++- tools/tests/batch-options.test.ts | 23 +++++-- tools/tests/run-log.test.ts | 109 +++++++++++++++++++++++++++++- 4 files changed, 155 insertions(+), 11 deletions(-) diff --git a/tools/src/dafny-commands.ts b/tools/src/dafny-commands.ts index 9559e30..d874143 100644 --- a/tools/src/dafny-commands.ts +++ b/tools/src/dafny-commands.ts @@ -6,6 +6,7 @@ import { existsSync, readFileSync, writeFileSync, copyFileSync, unlinkSync } fro import { execFileSync } from "child_process"; import path from "path"; import { DEFAULT_OPTIONS, parseOptionValue, type LscOptions } from "./config.js"; +import type { RunLog } from "./run-log.js"; function writeGen(genPath: string, text: string) { writeFileSync(genPath, text); @@ -20,7 +21,13 @@ export function dafnyGen(genPath: string, dfyPath: string, text: string) { } } -export function dafnyCheckDiff(genPath: string, dfyPath: string): boolean { +export function dafnyCheckDiff(genPath: string, dfyPath: string, log?: RunLog): boolean { + const ok = additionsOnly(genPath, dfyPath); + if (!ok) log?.finish({ stage: "diff", exit: 1, dfyPath }); + return ok; +} + +function additionsOnly(genPath: string, dfyPath: string): boolean { for (const filePath of [genPath, dfyPath]) { if (!existsSync(filePath)) { console.error(`ERROR: cannot verify additions-only diff; file does not exist: ${filePath}`); @@ -134,18 +141,27 @@ export function dafnyVerifyArgs(content: string, timeLimit?: number, extraFlags? return { args }; } -export function dafnyVerify(dfyPath: string, dir: string, timeLimit?: number, extraFlags?: string): boolean { +export function dafnyVerify(dfyPath: string, dir: string, timeLimit?: number, extraFlags?: string, log?: RunLog): boolean { console.log("Running dafny verify..."); try { const { args, error } = dafnyVerifyArgs(readFileSync(dfyPath, "utf-8"), timeLimit, extraFlags); - if (error) { console.error(error); return false; } + if (error) { + console.error(error); + log?.finish({ stage: "resolve", exit: 1, dfyPath }); + return false; + } + if (log) args.push(...log.dafnyArgs()); args.push(dfyPath); execFileSync("dafny", args, { cwd: dir, stdio: "inherit" }); + log?.finish({ stage: "ok", exit: 0, dfyPath, results: log.readResults() }); return true; } catch (e: any) { if (e?.code === "ENOENT") { console.error("ERROR: `dafny` not found on PATH — verification never ran. Install Dafny 4.x: https://dafny.org/"); } + // Dafny writes no results when it stops at parsing or resolution. + const results = log?.readResults() ?? null; + log?.finish({ stage: results ? "verify" : "resolve", exit: 1, dfyPath, results }); return false; } } diff --git a/tools/src/lsc.ts b/tools/src/lsc.ts index 1be9824..1ab840d 100755 --- a/tools/src/lsc.ts +++ b/tools/src/lsc.ts @@ -21,6 +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 { findUp, loadConfigOptions, @@ -420,6 +421,13 @@ function runFile( guardRelocatedDafnyProof(dir, artifactDir, base, dfyPath); mkdirSync(artifactDir, { recursive: true }); + // Record check/regen runs in the run log. Created after the proof-dir guard + // 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 && runLogEnabled(options["run-log"]) + ? new RunLog({ logDir: resolveLogDir(absPath, configFile), cmd: logCmd, sourcePath: absPath, extraFlags, lscVersion: lscVersion() }) + : undefined; + if (cmd === "gen") { dafnyGen(genPath, dfyPath, text); return; } if (cmd === "gen-check") { dafnyGen(genPath, dfyPath, text); @@ -428,8 +436,8 @@ function runFile( } if (cmd === "check") { dafnyGen(genPath, dfyPath, text); - if (!dafnyCheckDiff(genPath, dfyPath)) process.exit(1); - if (!dafnyVerify(dfyPath, artifactDir, timeLimit, extraFlags)) process.exit(1); + if (!dafnyCheckDiff(genPath, dfyPath, log)) process.exit(1); + if (!dafnyVerify(dfyPath, artifactDir, timeLimit, extraFlags, log)) process.exit(1); return; } if (cmd === "regen") { dafnyRegen(genPath, dfyPath, basePath, text, artifactDir, timeLimit, extraFlags, noVerify); return; } diff --git a/tools/tests/batch-options.test.ts b/tools/tests/batch-options.test.ts index 0315195..9c50127 100644 --- a/tools/tests/batch-options.test.ts +++ b/tools/tests/batch-options.test.ts @@ -1,7 +1,7 @@ import { test } from "node:test"; import assert from "node:assert/strict"; import { spawnSync } from "node:child_process"; -import { mkdtempSync, mkdirSync, readFileSync, readdirSync, realpathSync, rmSync, writeFileSync } from "node:fs"; +import { existsSync, mkdtempSync, mkdirSync, readFileSync, readdirSync, realpathSync, rmSync, writeFileSync } from "node:fs"; import { createRequire } from "node:module"; import { tmpdir } from "node:os"; import { delimiter, join } from "node:path"; @@ -12,7 +12,9 @@ const loader = createRequire(import.meta.url).resolve("tsx"); const posixOnly = { skip: process.platform === "win32" }; // Run the real CLI against a verifier that records arguments without proving. -function runCli(entries: string[], args: string[]) { +// The run log is off unless a test asks for it, so `calls` holds only the +// arguments under test. +function runCli(entries: string[], args: string[], runLog = false) { const dir = realpathSync(mkdtempSync(join(tmpdir(), "lsc-batch-options-"))); try { const bin = join(dir, "bin"); @@ -29,12 +31,19 @@ require("node:fs").appendFileSync(process.env.LSC_ARGV_LOG, JSON.stringify(proce `, { mode: 0o755 }); const result = spawnSync(process.execPath, ["--import", loader, cli, "--backend=dafny", ...args], { cwd: dir, - env: { ...process.env, PATH: `${bin}${delimiter}${process.env.PATH ?? ""}`, LSC_ARGV_LOG: log }, + env: { + ...process.env, PATH: `${bin}${delimiter}${process.env.PATH ?? ""}`, LSC_ARGV_LOG: log, + LSC_RUN_LOG: runLog ? "true" : "false", + }, encoding: "utf8", timeout: 30_000, }); assert.ifError(result.error); const calls: string[][] = readFileSync(log, "utf8").trim().split("\n").filter(Boolean).map(line => JSON.parse(line)); - return { ...result, dir, calls, files: readdirSync(dir) }; + const runsPath = join(dir, ".lemmascript", "runs.jsonl"); + const runs: { file: string }[] = existsSync(runsPath) + ? readFileSync(runsPath, "utf8").trim().split("\n").map(line => JSON.parse(line)) + : []; + return { ...result, dir, calls, runs, files: readdirSync(dir) }; } finally { rmSync(dir, { recursive: true, force: true }); } @@ -129,6 +138,12 @@ for (const flags of [[], ["--extra-flags=--cores=2"]]) { }); } +test("batch check records one run per verified entry and none for gen-check entries", posixOnly, () => { + const result = runCli(["a.ts 61", "b.ts 11", "c.ts"], ["check"], true); + assert.equal(result.status, 0, result.stderr); + assert.deepEqual(result.runs.map(r => r.file), ["b.ts", "c.ts"]); +}); + test("an explicit file keeps its existing CLI behavior", posixOnly, () => { const result = runCli(["a.ts 11 --isolate-assertions"], ["check", "a.ts", "--time-limit=120", "--extra-flags=--cores=2"]); assert.equal(result.status, 0, result.stderr); diff --git a/tools/tests/run-log.test.ts b/tools/tests/run-log.test.ts index e0d2d9f..a08bd8e 100644 --- a/tools/tests/run-log.test.ts +++ b/tools/tests/run-log.test.ts @@ -1,8 +1,9 @@ import { test } from "node:test"; import assert from "node:assert/strict"; -import { existsSync, mkdirSync, mkdtempSync, readFileSync, realpathSync, rmSync, writeFileSync } from "node:fs"; +import { chmodSync, existsSync, mkdirSync, mkdtempSync, readFileSync, realpathSync, rmSync, writeFileSync } from "node:fs"; import { tmpdir } from "node:os"; -import { join } from "node:path"; +import { delimiter, join } from "node:path"; +import { dafnyCheckDiff, dafnyVerify } from "../src/dafny-commands.ts"; import { RunLog, ensureLogDir, hashText, isPartialRun, parseTextLog, resolveLogDir, runLogEnabled, snapshotSource, } from "../src/run-log.ts"; @@ -203,3 +204,107 @@ test("dafnyArgs points Dafny at a temporary text log that readResults parses", ( rmSync(root, { recursive: true, force: true }); } }); + +// A stand-in for `dafny`: writes $FAKE_DAFNY_LOG to the text log path it is +// given (if any) and exits with $FAKE_DAFNY_EXIT. +const FAKE_DAFNY = `#!/bin/sh +out="" +for arg in "$@"; do + case "$arg" in + "text;LogFileName="*) out="\${arg#text;LogFileName=}" ;; + esac +done +if [ -n "$out" ] && [ -n "$FAKE_DAFNY_LOG" ]; then printf '%s' "$FAKE_DAFNY_LOG" > "$out"; fi +exit "\${FAKE_DAFNY_EXIT:-0}" +`; + +function withFakeDafny(env: { log?: string; exit?: number }, run: (root: string) => void): void { + const root = tempDir(); + const saved = { PATH: process.env.PATH, LOG: process.env.FAKE_DAFNY_LOG, EXIT: process.env.FAKE_DAFNY_EXIT }; + try { + mkdirSync(join(root, "bin")); + writeFileSync(join(root, "bin", "dafny"), FAKE_DAFNY); + chmodSync(join(root, "bin", "dafny"), 0o755); + process.env.PATH = `${join(root, "bin")}${delimiter}${saved.PATH ?? ""}`; + if (env.log === undefined) delete process.env.FAKE_DAFNY_LOG; else process.env.FAKE_DAFNY_LOG = env.log; + process.env.FAKE_DAFNY_EXIT = String(env.exit ?? 0); + run(root); + } finally { + for (const [key, value] of [["PATH", saved.PATH], ["FAKE_DAFNY_LOG", saved.LOG], ["FAKE_DAFNY_EXIT", saved.EXIT]] as const) { + if (value === undefined) delete process.env[key]; else process.env[key] = value; + } + rmSync(root, { recursive: true, force: true }); + } +} + +function verifyWithLog(root: string): boolean { + const source = join(root, "a.ts"); + const dfy = join(root, "a.dfy"); + writeFileSync(source, "export const a = 1;\n"); + writeFileSync(dfy, "lemma L() {}\n"); + const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: "0" }); + return dafnyVerify(dfy, root, undefined, undefined, log); +} + +const posixOnly = { skip: process.platform === "win32" }; + +test("a passing verification is recorded as ok with its members", posixOnly, () => + withFakeDafny({ log: "Results for L (correctness)\n Overall outcome: Correct\n", exit: 0 }, root => { + assert.equal(verifyWithLog(root), true); + const [r] = records(root); + assert.equal(r.stage, "ok"); + assert.equal(r.exit, 0); + assert.deepEqual(r.passed, ["L"]); + assert.equal(r.partial, false); + })); + +test("a failing verification is recorded as verify with the failed member", posixOnly, () => + withFakeDafny({ log: "Results for L (correctness)\n Overall outcome: Errors\n", exit: 4 }, root => { + assert.equal(verifyWithLog(root), false); + const [r] = records(root); + assert.equal(r.stage, "verify"); + assert.equal(r.exit, 1); + assert.deepEqual(r.failed, ["L"]); + })); + +test("a Dafny run that writes no results is recorded as resolve", posixOnly, () => + withFakeDafny({ exit: 2 }, root => { + assert.equal(verifyWithLog(root), false); + const [r] = records(root); + assert.equal(r.stage, "resolve"); + assert.equal(r.partial, true); + })); + +function checkDiffWithLog(root: string, generated: string, proof: string): boolean { + const source = join(root, "a.ts"); + const gen = join(root, "a.dfy.gen"); + const dfy = join(root, "a.dfy"); + writeFileSync(source, ""); + writeFileSync(gen, generated); + writeFileSync(dfy, proof); + const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: "0" }); + return dafnyCheckDiff(gen, dfy, log); +} + +test("an additions-only failure is recorded as diff", () => { + const root = tempDir(); + try { + assert.equal(checkDiffWithLog(root, "method M() {}\n", "method Changed() {}\n"), false); + const [r] = records(root); + assert.equal(r.stage, "diff"); + assert.equal(r.exit, 1); + assert.equal(r.partial, true); + } finally { + rmSync(root, { recursive: true, force: true }); + } +}); + +test("a passing additions-only check leaves the run open for verification to record", () => { + const root = tempDir(); + try { + assert.equal(checkDiffWithLog(root, "method M() {}\n", "method M() {}\nlemma Proof() {}\n"), true); + assert.equal(existsSync(join(root, ".lemmascript", "runs.jsonl")), false); + } finally { + rmSync(root, { recursive: true, force: true }); + } +}); From 4ff080860518f3e17563abd33c65c89520fe4cba Mon Sep 17 00:00:00 2001 From: Annie Vella Date: Mon, 5 Oct 2026 15:46:27 +1300 Subject: [PATCH 06/12] record lsc regen runs, including conflicts and diff failures --- tools/src/dafny-commands.ts | 14 ++- tools/src/lsc.ts | 2 +- tools/tests/run-log.test.ts | 182 ++++++++++++++++++++++++------------ 3 files changed, 134 insertions(+), 64 deletions(-) diff --git a/tools/src/dafny-commands.ts b/tools/src/dafny-commands.ts index d874143..60575de 100644 --- a/tools/src/dafny-commands.ts +++ b/tools/src/dafny-commands.ts @@ -166,7 +166,7 @@ export function dafnyVerify(dfyPath: string, dir: string, timeLimit?: number, ex } } -export function dafnyRegen(genPath: string, dfyPath: string, basePath: string, text: string, dir: string, timeLimit?: number, extraFlags?: string, noVerify = false) { +export function dafnyRegen(genPath: string, dfyPath: string, basePath: string, text: string, dir: string, timeLimit?: number, extraFlags?: string, noVerify = false, log?: RunLog) { // 1. Read old gen before overwriting (needed for base seeding) const oldGen = existsSync(genPath) ? readFileSync(genPath, "utf-8") : ""; @@ -177,10 +177,11 @@ export function dafnyRegen(genPath: string, dfyPath: string, basePath: string, t if (!existsSync(dfyPath)) { writeFileSync(dfyPath, text); console.log(`Created: ${path.basename(dfyPath)}`); - if (!noVerify && !dafnyVerify(dfyPath, dir, timeLimit, extraFlags)) { + if (!noVerify && !dafnyVerify(dfyPath, dir, timeLimit, extraFlags, log)) { console.error(`FAILED: ${path.basename(dfyPath)} verification failed on first run.`); process.exit(1); } + log?.finish({ stage: "ok", exit: 0, dfyPath }); return; } @@ -201,6 +202,7 @@ export function dafnyRegen(genPath: string, dfyPath: string, basePath: string, t copyFileSync(dfyPath, mergedPath); writeFileSync(dfyPath, savedDfy); console.error(`CONFLICT: ${path.basename(dfyPath)} — merge had conflicts, dfy restored. See ${path.basename(mergedPath)}`); + log?.finish({ stage: "conflict", exit: 1, dfyPath }); process.exit(1); } throw e; @@ -208,13 +210,13 @@ export function dafnyRegen(genPath: string, dfyPath: string, basePath: string, t } // 6. Check gen invariant (unconditional) - if (!dafnyCheckDiff(genPath, dfyPath)) { + if (!dafnyCheckDiff(genPath, dfyPath, log)) { console.error(`FAILED: ${path.basename(dfyPath)} has modifications to generated lines.`); process.exit(1); } // 7. Verify (skipped under --no-verify: caller verifies separately) - if (!noVerify && !dafnyVerify(dfyPath, dir, timeLimit, extraFlags)) { + if (!noVerify && !dafnyVerify(dfyPath, dir, timeLimit, extraFlags, log)) { // The clean merge already incorporated this generation into the proof // file. Keep that generation as the next merge anchor even though the // verifier rejected the current proof state; otherwise the next regen @@ -224,6 +226,8 @@ export function dafnyRegen(genPath: string, dfyPath: string, basePath: string, t process.exit(1); } - // 8. Success — delete base (gen is now the anchor) + // 8. Success — delete base (gen is now the anchor). After a verified run + // dafnyVerify has already recorded the outcome; this records --no-verify. if (existsSync(basePath)) unlinkSync(basePath); + log?.finish({ stage: "ok", exit: 0, dfyPath }); } diff --git a/tools/src/lsc.ts b/tools/src/lsc.ts index 1ab840d..b7379e5 100755 --- a/tools/src/lsc.ts +++ b/tools/src/lsc.ts @@ -440,7 +440,7 @@ function runFile( if (!dafnyVerify(dfyPath, artifactDir, timeLimit, extraFlags, log)) process.exit(1); return; } - if (cmd === "regen") { dafnyRegen(genPath, dfyPath, basePath, text, artifactDir, timeLimit, extraFlags, noVerify); return; } + if (cmd === "regen") { dafnyRegen(genPath, dfyPath, basePath, text, artifactDir, timeLimit, extraFlags, noVerify, log); return; } console.error(`Unknown command: ${cmd}`); process.exit(1); } diff --git a/tools/tests/run-log.test.ts b/tools/tests/run-log.test.ts index a08bd8e..2d0ef8e 100644 --- a/tools/tests/run-log.test.ts +++ b/tools/tests/run-log.test.ts @@ -3,15 +3,22 @@ import assert from "node:assert/strict"; import { chmodSync, existsSync, mkdirSync, mkdtempSync, readFileSync, realpathSync, rmSync, writeFileSync } from "node:fs"; import { tmpdir } from "node:os"; import { delimiter, join } from "node:path"; -import { dafnyCheckDiff, dafnyVerify } from "../src/dafny-commands.ts"; +import { dafnyCheckDiff, dafnyRegen, dafnyVerify } from "../src/dafny-commands.ts"; import { RunLog, ensureLogDir, hashText, isPartialRun, parseTextLog, resolveLogDir, runLogEnabled, snapshotSource, } from "../src/run-log.ts"; +const posixOnly = { skip: process.platform === "win32" }; + function tempDir(): string { return realpathSync(mkdtempSync(join(tmpdir(), "lsc-run-log-test-"))); } +function records(logDir: string): any[] { + return readFileSync(join(logDir, ".lemmascript", "runs.jsonl"), "utf8") + .trim().split("\n").map(line => JSON.parse(line)); +} + // Trimmed from real Dafny 4.11 `--log-format text` output for a broken arraySum. const TEXT_LOG = ` Results for sumTo (well-formedness) @@ -25,6 +32,89 @@ Results for arraySum (correctness) Overall outcome: Errors `; +// A stand-in for `dafny`: writes $FAKE_DAFNY_LOG to the text log path it is +// given (if any) and exits with $FAKE_DAFNY_EXIT. +const FAKE_DAFNY = `#!/bin/sh +out="" +for arg in "$@"; do + case "$arg" in + "text;LogFileName="*) out="\${arg#text;LogFileName=}" ;; + esac +done +if [ -n "$out" ] && [ -n "$FAKE_DAFNY_LOG" ]; then printf '%s' "$FAKE_DAFNY_LOG" > "$out"; fi +exit "\${FAKE_DAFNY_EXIT:-0}" +`; + +function withFakeDafny(env: { log?: string; exit?: number }, run: (root: string) => void): void { + const root = tempDir(); + const saved = { PATH: process.env.PATH, LOG: process.env.FAKE_DAFNY_LOG, EXIT: process.env.FAKE_DAFNY_EXIT }; + try { + mkdirSync(join(root, "bin")); + writeFileSync(join(root, "bin", "dafny"), FAKE_DAFNY); + chmodSync(join(root, "bin", "dafny"), 0o755); + process.env.PATH = `${join(root, "bin")}${delimiter}${saved.PATH ?? ""}`; + if (env.log === undefined) delete process.env.FAKE_DAFNY_LOG; else process.env.FAKE_DAFNY_LOG = env.log; + process.env.FAKE_DAFNY_EXIT = String(env.exit ?? 0); + run(root); + } finally { + for (const [key, value] of [["PATH", saved.PATH], ["FAKE_DAFNY_LOG", saved.LOG], ["FAKE_DAFNY_EXIT", saved.EXIT]] as const) { + if (value === undefined) delete process.env[key]; else process.env[key] = value; + } + rmSync(root, { recursive: true, force: true }); + } +} + +function verifyWithLog(root: string): boolean { + const source = join(root, "a.ts"); + const dfy = join(root, "a.dfy"); + writeFileSync(source, "export const a = 1;\n"); + writeFileSync(dfy, "lemma L() {}\n"); + const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: "0" }); + return dafnyVerify(dfy, root, undefined, undefined, log); +} + +function checkDiffWithLog(root: string, generated: string, proof: string): boolean { + const source = join(root, "a.ts"); + const gen = join(root, "a.dfy.gen"); + const dfy = join(root, "a.dfy"); + writeFileSync(source, ""); + writeFileSync(gen, generated); + writeFileSync(dfy, proof); + const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: "0" }); + return dafnyCheckDiff(gen, dfy, log); +} + +class ExitSignal extends Error { + constructor(readonly code: number | undefined) { super(`process.exit(${code})`); } +} + +const generation = (n: number): string => `method M() {\n var value := ${n};\n}\n`; +const addition = "\nlemma AddedProof() {}\n"; + +/** Run dafnyRegen with process.exit turned into a throw, then return the recorded run. */ +function regenRecord(root: string, proof: string, next: string, opts: { base?: string; noVerify?: boolean } = {}): any { + const f = { gen: join(root, "x.dfy.gen"), proof: join(root, "x.dfy"), base: join(root, "x.dfy.base"), source: join(root, "x.ts") }; + writeFileSync(f.source, ""); + 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 originalExit = process.exit; + process.exit = ((code?: number) => { throw new ExitSignal(code); }) as typeof process.exit; + try { + dafnyRegen(f.gen, f.proof, f.base, next, root, undefined, undefined, opts.noVerify ?? false, log); + } catch (e) { + if (!(e instanceof ExitSignal)) throw e; + } finally { + process.exit = originalExit; + } + const all = records(root); + assert.equal(all.length, 1, "exactly one record per run"); + return all[0]; +} + +// Parsing, hashing, settings and location. + test("parseTextLog lists each member once, failed if any check failed", () => { assert.deepEqual(parseTextLog(TEXT_LOG), { passed: ["sumTo"], failed: ["arraySum"] }); }); @@ -83,10 +173,7 @@ test("the log lives beside lemmascript.json, else at the git root, else in cwd", } }); -function records(logDir: string): any[] { - return readFileSync(join(logDir, ".lemmascript", "runs.jsonl"), "utf8") - .trim().split("\n").map(line => JSON.parse(line)); -} +// The log directory, snapshots and records. test("ensureLogDir creates a self-ignoring directory and keeps an edited .gitignore", () => { const root = tempDir(); @@ -205,48 +292,7 @@ test("dafnyArgs points Dafny at a temporary text log that readResults parses", ( } }); -// A stand-in for `dafny`: writes $FAKE_DAFNY_LOG to the text log path it is -// given (if any) and exits with $FAKE_DAFNY_EXIT. -const FAKE_DAFNY = `#!/bin/sh -out="" -for arg in "$@"; do - case "$arg" in - "text;LogFileName="*) out="\${arg#text;LogFileName=}" ;; - esac -done -if [ -n "$out" ] && [ -n "$FAKE_DAFNY_LOG" ]; then printf '%s' "$FAKE_DAFNY_LOG" > "$out"; fi -exit "\${FAKE_DAFNY_EXIT:-0}" -`; - -function withFakeDafny(env: { log?: string; exit?: number }, run: (root: string) => void): void { - const root = tempDir(); - const saved = { PATH: process.env.PATH, LOG: process.env.FAKE_DAFNY_LOG, EXIT: process.env.FAKE_DAFNY_EXIT }; - try { - mkdirSync(join(root, "bin")); - writeFileSync(join(root, "bin", "dafny"), FAKE_DAFNY); - chmodSync(join(root, "bin", "dafny"), 0o755); - process.env.PATH = `${join(root, "bin")}${delimiter}${saved.PATH ?? ""}`; - if (env.log === undefined) delete process.env.FAKE_DAFNY_LOG; else process.env.FAKE_DAFNY_LOG = env.log; - process.env.FAKE_DAFNY_EXIT = String(env.exit ?? 0); - run(root); - } finally { - for (const [key, value] of [["PATH", saved.PATH], ["FAKE_DAFNY_LOG", saved.LOG], ["FAKE_DAFNY_EXIT", saved.EXIT]] as const) { - if (value === undefined) delete process.env[key]; else process.env[key] = value; - } - rmSync(root, { recursive: true, force: true }); - } -} - -function verifyWithLog(root: string): boolean { - const source = join(root, "a.ts"); - const dfy = join(root, "a.dfy"); - writeFileSync(source, "export const a = 1;\n"); - writeFileSync(dfy, "lemma L() {}\n"); - const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: "0" }); - return dafnyVerify(dfy, root, undefined, undefined, log); -} - -const posixOnly = { skip: process.platform === "win32" }; +// Recording `check` runs. test("a passing verification is recorded as ok with its members", posixOnly, () => withFakeDafny({ log: "Results for L (correctness)\n Overall outcome: Correct\n", exit: 0 }, root => { @@ -275,17 +321,6 @@ test("a Dafny run that writes no results is recorded as resolve", posixOnly, () assert.equal(r.partial, true); })); -function checkDiffWithLog(root: string, generated: string, proof: string): boolean { - const source = join(root, "a.ts"); - const gen = join(root, "a.dfy.gen"); - const dfy = join(root, "a.dfy"); - writeFileSync(source, ""); - writeFileSync(gen, generated); - writeFileSync(dfy, proof); - const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: "0" }); - return dafnyCheckDiff(gen, dfy, log); -} - test("an additions-only failure is recorded as diff", () => { const root = tempDir(); try { @@ -308,3 +343,34 @@ test("a passing additions-only check leaves the run open for verification to rec rmSync(root, { recursive: true, force: true }); } }); + +// Recording `regen` runs. + +test("a regen merge conflict is recorded before lsc exits", posixOnly, () => + withFakeDafny({ exit: 0 }, root => { + const r = regenRecord(root, generation(99) + addition, generation(1)); + assert.equal(r.stage, "conflict"); + assert.equal(r.exit, 1); + assert.equal(r.partial, true); + })); + +test("a regen additions-only failure is recorded as diff", posixOnly, () => + withFakeDafny({ exit: 0 }, root => { + const r = regenRecord(root, generation(99), generation(0), { base: generation(0) }); + assert.equal(r.stage, "diff"); + })); + +test("a regen verification failure is recorded as verify", posixOnly, () => + withFakeDafny({ log: "Results for M (correctness)\n Overall outcome: Errors\n", exit: 4 }, root => { + const r = regenRecord(root, generation(0) + addition, generation(1)); + assert.equal(r.stage, "verify"); + assert.deepEqual(r.failed, ["M"]); + })); + +test("a clean regen --no-verify is recorded as ok but partial", posixOnly, () => + withFakeDafny({ exit: 0 }, root => { + const r = regenRecord(root, generation(0) + addition, generation(2), { noVerify: true }); + assert.equal(r.stage, "ok"); + assert.equal(r.exit, 0); + assert.equal(r.partial, true); + })); From 41411d2bcc128f139e4f0d5f9b9677f781e451bf Mon Sep 17 00:00:00 2001 From: Annie Vella Date: Mon, 5 Oct 2026 15:55:04 +1300 Subject: [PATCH 07/12] run log fixture and docs --- AGENTS.md | 2 ++ DESIGN_RUN_LOG.md | 46 ++++++++++++++++++++---------------------- SPEC.md | 20 ++++++++++++++++-- TOOLS.md | 2 ++ tools/test-fixtures.sh | 34 +++++++++++++++++++++++++++++++ 5 files changed, 78 insertions(+), 26 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 92a00d3..674d917 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -23,6 +23,8 @@ Default backend is Dafny. Pass `--backend=...` explicitly anyway — case-study If `lemmascript.json` sets `proof-dir`, all Dafny companions (`.dfy.gen`, `.dfy`, `.dfy.base`, `.dfy.merged`) live in the mirrored directory reported by `lsc config`, not beside the TS file. The edit boundaries and regen rules below apply at that mapped location unchanged. +`lsc check` and `lsc regen` record each Dafny run in `.lemmascript/` (self-ignored by git; see SPEC.md §7.7). Leave it alone — it is the record of what verification caught. `LSC_RUN_LOG=false` turns it off for one run. + After editing `lsc` itself (anything under `tools/`), run `npm run build` before re-invoking `npx lsc` — the CLI runs the compiled `tools/dist/lsc.js`, not the TS source. ## File-edit boundaries diff --git a/DESIGN_RUN_LOG.md b/DESIGN_RUN_LOG.md index d8dc01c..3632ccf 100644 --- a/DESIGN_RUN_LOG.md +++ b/DESIGN_RUN_LOG.md @@ -1,6 +1,6 @@ # DESIGN_RUN_LOG — Counting what verification caught -**Status:** proposal; nothing is implemented in `lsc`. A stopgap wrapper on the `lemmascript-catch-log` branch of lemmascript-skills confirmed the Dafny CSV approach in §2 against `lsc` 0.6.1, passing the flag through `--extra-flags`. +**Status:** slice 1 implemented (recording `check` and `regen` runs). `lsc runs`, claimcheck records, labels and reports are not yet built. A stopgap wrapper on the `lemmascript-catch-log` branch of lemmascript-skills confirmed the Dafny CSV approach against `lsc` 0.6.1, passing the flag through `--extra-flags`; slice 1 uses the text format instead (§2). **Date:** September 2026 ## Goal @@ -11,6 +11,8 @@ Asking the agent to keep a tally at the end of a session does not give honest co Labeling a catch as a code bug or a spec bug happens afterward, at report time. A reporting skill reads the log, looks at what changed in the source between the failing and the passing run, and labels each catch from that diff. The agent doing the work has no extra duties while it works. +In this document a **catch** is a fact about the history, not a bug: a member that failed in one run and passed in a later one. Most catches are ordinary proof work; only some are bugs, and §4 and §5 sort them. + ## Requirements 1. **Mechanical first.** A catch exists only if the log shows a failure followed by a pass. @@ -18,8 +20,9 @@ Labeling a catch as a code bug or a spec bug happens afterward, at report time. 3. **No change to what the user sees.** Logging does not alter `lsc` output, exit codes, or generated files. Dafny's output still streams to the terminal while it runs. 4. **Invisible to git.** The log directory ignores itself, so it never shows up in `git status` and needs no `.gitignore` edit. 5. **Code and proof are kept apart.** The record shows whether the fix touched the `.ts` (the program or its spec) or only the `.dfy` (the proof). The two are reported separately. -6. **Labels are made after the fact, from evidence.** The log keeps enough to label a catch later without the working agent's memory: the source before and after the fix, and the error that preceded it. +6. **Labels are made after the fact, from evidence.** The log keeps enough to label a catch later without the working agent's memory: the source before and after the fix, and the error that preceded it (error text is not yet recorded; see §2). 7. **Claimcheck is counted the same way, and is not modified.** `lsc` reads the report file that claimcheck already writes. +8. **Logging never fails a run.** A logging error (unwritable directory, full disk) is swallowed; output and exit codes are unchanged. ## 1. Where the log lives @@ -31,7 +34,9 @@ Logging is on by default. A project turns it off with a config-only entry in the } ``` -`LSC_RUN_LOG=0` turns it off for a single run. +`LSC_RUN_LOG=false` turns it off for a single run; like `lemmascript.json`, the variable accepts only `true` or `false`. + +`run-log` is config-only, not a `//@ option`: a file that could switch off its own logging would let an agent hide the failures the log exists to count. The log lives in `.lemmascript/` in the directory that holds the selected `lemmascript.json`. Without a config file, it goes in the git repository root, or in the current working directory outside a repository. When `lsc` creates the directory, it writes `.lemmascript/.gitignore` containing `*`, so git ignores the whole directory without any change to the project's own `.gitignore`. @@ -48,33 +53,26 @@ The log lives in `.lemmascript/` in the directory that holds the selected `lemma `dafnyVerify` (`tools/src/dafny-commands.ts`) gains one extra Dafny argument when logging is on: ``` ---log-format csv;LogFileName=/verify.csv -``` - -Dafny writes one row per verified member and still prints its normal output. Here is the real output for a two-lemma file, one lemma good and one bad, run with Dafny 4.11: - -``` -TestResult.DisplayName,TestResult.Outcome,TestResult.Duration,TestResult.ResourceCount,RandomSeed -bad (correctness),Failed,00:00:00.0356494,3134,0 -good (correctness),Passed,00:00:00.0256170,3017,0 +--log-format text;LogFileName=/verify.txt ``` -With this flag, Dafny also prints a `Results File: ` line, which `lsc` removes from the output it passes on. +Dafny writes one `Results for ()` block per verified member, each with an `Overall outcome`, and its terminal output is unchanged. `lsc` keeps Dafny's stdio inherited. The CSV format was rejected because it always prints an extra `Results File:` line, which `lsc` could only remove by piping Dafny's output, and streaming piped output would make the whole check/regen path asynchronous. The cost is that records do not yet carry Dafny's error messages. -To keep the error text, `lsc` runs Dafny with its output piped rather than inherited and forwards each chunk to the terminal as it arrives. The output still streams, and `lsc` keeps a copy. After Dafny exits, `lsc` reads the CSV and appends one record: +The helper that detects how the run ended appends one record: `dafnyCheckDiff` for `diff`, `dafnyVerify` for `ok`, `verify` and `resolve`, and `dafnyRegen` for `conflict` and `--no-verify` runs. ```json -{"type":"verify","id":"r_7f3a","ts":"2026-09-30T21:14:02Z", - "cmd":"check","file":"src/domain.ts","stage":"verify","exit":4, +{"v":1,"type":"verify","id":"6f1c…","ts":"2026-10-05T21:14:02Z", + "cmd":"check","file":"src/domain.ts","stage":"verify","exit":1,"partial":false, "failed":["applyDiscount_ensures"],"passed":["clamp","clamp_ensures","applyDiscount"], "tsHash":"9c1e04b2d7aa","dfyHash":"41d0f93be812", - "errors":["domain.dfy(41,2): Error: a postcondition could not be proved on this return path", "..."]} + "lsc":"0.6.4","ci":false} ``` -- **`stage`** tells where the run stopped. `diff` means the additions-only check failed, so Dafny never ran. `resolve` means Dafny exited with a parse or resolution error and wrote no CSV rows. `conflict` means a `regen` merge conflicted. `verify` means Dafny ran and wrote rows. `ok` means everything passed. -- **`failed` / `passed`** are the member names with Dafny's ` (correctness)` / ` (well-formedness)` suffix removed. A member that fails on both counts appears once. -- **`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 after Dafny exits, because `check` may create it and `regen` may merge into it, and the post-run file is the one Dafny verified. -- **`errors`** holds Dafny's `Error:` lines and their related-location lines, capped at 40 lines. It is present only on failing runs. +- **`stage`** tells where the run stopped. `diff` means the additions-only check failed, so Dafny never ran. `resolve` means Dafny wrote no results (a parse or resolution error, or Dafny did not run). `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) and `ci` give context; fields such as the git commit 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. @@ -108,7 +106,7 @@ npx lsc runs report # write a dated report of everything not yet report There are no sessions. `lsc runs` always derives catches from the whole log, because a failure can be fixed days after it happened, and then shows only what falls after the most recent report. -**A verify catch** is a member `M` in file `F` that appears in `failed` in some run, and in `passed` in the first later run of `F`. Its kind comes from comparing the hashes of the two runs: +**A verify catch** is a member `M` in file `F` that appears in `failed` in some run, and in `passed` in the first later run of `F` that reported on `M`. Runs that did not report on `M` (a `diff`, `resolve` or `conflict` stage, `--no-verify`, or a filter) are skipped. Its kind comes from comparing the hashes of the two runs: | `.ts` changed | `.dfy` changed | Kind | |---|---|---| @@ -125,7 +123,7 @@ There are no sessions. `lsc runs` always derives catches from the whole log, bec | yes | yes | `both-fixed` | | no | no | `flaky`: claimcheck's LLM step changed its verdict on unchanged input. | -A failure that has no later pass yet is **open**. If a member disappears from later runs because it was renamed or deleted, the failure is reported as **dropped**, never as a catch. +A failure that has no later pass yet is **open**. If a member is missing from a later run that is not `partial`, because it was renamed or deleted, the failure is reported as **dropped**, never as a catch. Each catch has an ID, formed from the failing run and the member name, such as `r_7f3a:applyDiscount_ensures`. @@ -222,7 +220,7 @@ The report file ends with one line per catch: its kind, label, file, failure dat |---|---| | `tools/src/config.ts` | Add a `run-log` registry entry (boolean, default `true`, config-only). | | `tools/src/run-log.ts` (new) | Create `.lemmascript/` with its `.gitignore`, append records, hash and snapshot files, read the Dafny CSV, extract error lines, derive catches, compute diffs and `change` hints, write labels, write dated reports and their markers. | -| `tools/src/dafny-commands.ts` | `dafnyVerify` and `dafnyRegen` take an optional log context. When it is present, they add `--log-format`, pipe and forward Dafny's output instead of inheriting it, and append a record after Dafny exits. `dafnyCheckDiff` failures are recorded as `stage: "diff"`. | +| `tools/src/dafny-commands.ts` | `dafnyCheckDiff`, `dafnyVerify` and `dafnyRegen` take an optional log context, and each records the stage it detects. `dafnyVerify` adds `--log-format text` and reads the member outcomes after Dafny exits; Dafny's output stays inherited. | | `tools/src/lsc.ts` | Pass the log context from resolved options. Record claimcheck results in both branches. Add the `runs`, `runs label`, and `runs report` subcommands. | | `tools/fixtures/` | One fixture that goes fail → proof fix → pass, one that goes fail → code fix → pass (`code-only`), and one that goes fail → annotation fix → pass (`annotations-only`), checking the derived kinds and hints. | | `lemmascript-catch-report` skill (new, in lemmascript-skills) | Label unlabeled `source-fix` catches from `lsc runs --json` evidence, list open claimcheck disputes for the user, and write the report. | diff --git a/SPEC.md b/SPEC.md index 753db23..0a086ef 100644 --- a/SPEC.md +++ b/SPEC.md @@ -1347,11 +1347,11 @@ For Dafny `check`, an explicit timeout enables verification even above 60s witho ### 7.2 `check` - **Lean:** gen + `lake build` (checks `.def.lean` + `.proof.lean` + `.spec.lean`) -- **Dafny:** gen + additions-only check + `dafny verify` +- **Dafny:** gen + additions-only check + `dafny verify`; the run is recorded in the run log (§7.7) ### 7.3 `regen` (Dafny only) -Three-way merge when generated code changes. See [SPEC_DAFNY.md](SPEC_DAFNY.md). +Three-way merge when generated code changes. See [SPEC_DAFNY.md](SPEC_DAFNY.md). Each run, including a conflict or additions-only failure, is recorded in the run log (§7.7). ### 7.4 `info` @@ -1424,6 +1424,22 @@ See [examples/utf16.ts](examples/utf16.ts) and its Dafny proof. Compatibility is after project values and file directives are merged. Collection libraries may differ between files; unlike the string model, they do not change the meaning of contracts. +### 7.7 Run log + +Every Dafny `check` and `regen` appends one JSON record to `.lemmascript/runs.jsonl`, in the +directory of the selected `lemmascript.json` (else the source's git root, else the current +directory), and stores the source as `.lemmascript/blobs/.ts`. The directory contains a +`.gitignore` of `*`, so it never appears in `git status`. A record names the file, the command, +the stage where the run stopped (`ok`, `verify`, `resolve`, `diff`, `conflict`), the members that +passed and failed, hashes of the `.ts` and `.dfy`, and `partial: true` when the run did not +report on every member. Logging never changes `lsc` output or exit codes. + +```json +{ "run-log": false } +``` + +turns it off for a project; `LSC_RUN_LOG=false` turns it off for one run. + --- ## 8. Pipeline diff --git a/TOOLS.md b/TOOLS.md index d5394f3..fdaa10f 100644 --- a/TOOLS.md +++ b/TOOLS.md @@ -172,6 +172,8 @@ not implement routing themselves. - `lsc regen --backend=dafny foo.ts` — regenerate `.dfy.gen`, three-way merge, verify - `lsc check --backend=dafny foo.ts` — gen + additions-only check + `dafny verify` +`check` and `regen` pass an optional `RunLog` (`run-log.ts`) to these helpers, and each records the stage it detects: `dafnyCheckDiff` records `diff`, `dafnyVerify` records `ok`/`verify`/`resolve`, and `dafnyRegen` records `conflict` and `--no-verify` runs. Dafny keeps inherited stdio; member outcomes come from `--log-format text` written to a temp file. + ## Narrow Rules `narrow.ts` (structural-narrowing rewrite pass) takes typed IR and rewrites narrowing patterns into IR nodes that transform lowers uniformly: `someMatch` (binary, for optional checks) or `tagMatch` (multi-case, for discriminated unions). Each carries the scrutinee, the matched cases, and the fallthrough. diff --git a/tools/test-fixtures.sh b/tools/test-fixtures.sh index 81903d4..60ef9d4 100755 --- a/tools/test-fixtures.sh +++ b/tools/test-fixtures.sh @@ -2,6 +2,10 @@ set -euo pipefail cd "$(dirname "$0")/.." +# Fixture runs use temp dirs outside any git repo, so the run log would land in +# the current directory. Keep it off; the run-log section turns it on locally. +export LSC_RUN_LOG=false + # Run executable tests before the Dafny fixture checks. npx tsx --test tools/tests/*.test.ts @@ -279,3 +283,33 @@ if grep -Fq '// lsc options:' "$fixture_dir/legacy-safe-slice.dfy.gen"; then echo "ERROR: unicode-scalar stamped an options header" exit 1 fi + +# Run log: a real check → broken proof → fixed proof sequence is recorded with +# member outcomes and hashes, inside a self-ignoring .lemmascript/ beside the config. +run_log_dir="$fixture_dir/run-log-project" +mkdir -p "$run_log_dir" +echo '{}' > "$run_log_dir/lemmascript.json" +cp examples/arraySum.ts examples/arraySum.dfy "$run_log_dir/" +LSC_RUN_LOG=true npx tsx tools/src/lsc.ts check --backend=dafny "$run_log_dir/arraySum.ts" +cp "$run_log_dir/arraySum.dfy" "$run_log_dir/arraySum.dfy.good" +# Break the proof with an addition (a false invariant on its own line), so the +# additions-only check passes and Dafny itself rejects it. +awk '{ print } /invariant \(sum == sumTo\(arr, i\)\)/ { print " invariant sum == 0" }' \ + "$run_log_dir/arraySum.dfy.good" > "$run_log_dir/arraySum.dfy" +expect_failure \ + "run log fixture: a false added invariant verified" \ + env LSC_RUN_LOG=true npx tsx tools/src/lsc.ts check --backend=dafny "$run_log_dir/arraySum.ts" +mv "$run_log_dir/arraySum.dfy.good" "$run_log_dir/arraySum.dfy" +LSC_RUN_LOG=true npx tsx tools/src/lsc.ts check --backend=dafny "$run_log_dir/arraySum.ts" +node -e ' +const runs = require("fs").readFileSync(process.argv[1], "utf8").trim().split("\n").map(l => JSON.parse(l)); +const fail = msg => { console.error("ERROR: run log fixture: " + msg); process.exit(1); }; +const stages = runs.map(r => r.stage).join(","); +if (stages !== "ok,verify,ok") fail("stages were " + stages); +if (!runs[1].failed.includes("arraySum")) fail("arraySum was not recorded as failing"); +if (!runs[2].passed.includes("arraySum")) fail("arraySum was not recorded as passing again"); +if (new Set(runs.map(r => r.tsHash)).size !== 1) fail("the .ts hash changed although the .ts did not"); +if (runs[1].dfyHash === runs[0].dfyHash || runs[2].dfyHash !== runs[0].dfyHash) fail("dfy hashes did not track the proof edit"); +' "$run_log_dir/.lemmascript/runs.jsonl" +grep -qx '\*' "$run_log_dir/.lemmascript/.gitignore" +expect_absent .lemmascript From d464116e7694d40af2518a9c3b15d13af1b8b26c Mon Sep 17 00:00:00 2001 From: Annie Vella Date: Mon, 5 Oct 2026 17:30:26 +1300 Subject: [PATCH 08/12] review fixes: resolution errors as resolve, LSC_RUN_LOG checked everywhere, drop ci field, more tests, docs --- DESIGN_RUN_LOG.md | 6 +-- site/src/content/docs/reference/cli.md | 9 +++- tools/src/lsc.ts | 4 +- tools/src/run-log.ts | 12 +++-- tools/tests/run-log.test.ts | 69 +++++++++++++++++++++++--- 5 files changed, 82 insertions(+), 18 deletions(-) diff --git a/DESIGN_RUN_LOG.md b/DESIGN_RUN_LOG.md index 3632ccf..37e3a4d 100644 --- a/DESIGN_RUN_LOG.md +++ b/DESIGN_RUN_LOG.md @@ -65,13 +65,13 @@ The helper that detects how the run ended appends one record: `dafnyCheckDiff` f "cmd":"check","file":"src/domain.ts","stage":"verify","exit":1,"partial":false, "failed":["applyDiscount_ensures"],"passed":["clamp","clamp_ensures","applyDiscount"], "tsHash":"9c1e04b2d7aa","dfyHash":"41d0f93be812", - "lsc":"0.6.4","ci":false} + "lsc":"0.6.4"} ``` - **`stage`** tells where the run stopped. `diff` means the additions-only check failed, so Dafny never ran. `resolve` means Dafny wrote no results (a parse or resolution error, or Dafny did not run). `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) and `ci` give context; fields such as the git commit 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) 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. @@ -219,7 +219,7 @@ The report file ends with one line per catch: its kind, label, file, failure dat | File | Change | |---|---| | `tools/src/config.ts` | Add a `run-log` registry entry (boolean, default `true`, config-only). | -| `tools/src/run-log.ts` (new) | Create `.lemmascript/` with its `.gitignore`, append records, hash and snapshot files, read the Dafny CSV, extract error lines, derive catches, compute diffs and `change` hints, write labels, write dated reports and their markers. | +| `tools/src/run-log.ts` (new) | Create `.lemmascript/` with its `.gitignore`, append records, hash and snapshot files, read Dafny's text results file, derive catches, compute diffs and `change` hints, write labels, write dated reports and their markers. | | `tools/src/dafny-commands.ts` | `dafnyCheckDiff`, `dafnyVerify` and `dafnyRegen` take an optional log context, and each records the stage it detects. `dafnyVerify` adds `--log-format text` and reads the member outcomes after Dafny exits; Dafny's output stays inherited. | | `tools/src/lsc.ts` | Pass the log context from resolved options. Record claimcheck results in both branches. Add the `runs`, `runs label`, and `runs report` subcommands. | | `tools/fixtures/` | One fixture that goes fail → proof fix → pass, one that goes fail → code fix → pass (`code-only`), and one that goes fail → annotation fix → pass (`annotations-only`), checking the derived kinds and hints. | diff --git a/site/src/content/docs/reference/cli.md b/site/src/content/docs/reference/cli.md index a06329d..5b57e66 100644 --- a/site/src/content/docs/reference/cli.md +++ b/site/src/content/docs/reference/cli.md @@ -97,7 +97,8 @@ at the current directory. Use `--config=` to pin a particular file. "string-semantics": "unicode-scalar", "dafny-library": "stdlib", "safe-slice": true, - "proof-dir": "proofs" + "proof-dir": "proofs", + "run-log": true } ``` @@ -105,6 +106,12 @@ at the current directory. Use `--config=` to pin a particular file. operations. Enabling `"string-semantics": "javascript-utf16"` requires explicitly setting `"dafny-library": "local"`; an omitted or explicit `stdlib` choice is an error. +`run-log` (default `true`) records every Dafny `check` and `regen` in `.lemmascript/` +beside `lemmascript.json`: one line per run in `runs.jsonl` (the stage it stopped at and +which members passed or failed) plus a snapshot of the source. The directory ignores +itself in git, and logging never changes `lsc` output or exit codes. Set it to `false` to +turn logging off for the project, or `LSC_RUN_LOG=false` for a single run. + A file can override both project settings before its first statement: ```typescript diff --git a/tools/src/lsc.ts b/tools/src/lsc.ts index b7379e5..f8a63ec 100755 --- a/tools/src/lsc.ts +++ b/tools/src/lsc.ts @@ -338,6 +338,8 @@ function runFile( const fullText = sourceFile.getFullText(); const { options, configFile } = effectiveOptions(absPath, fullText, configPath); + // Validate LSC_RUN_LOG for every command, as a bad config value would be. + const runLogOn = runLogEnabled(options["run-log"]); // Check //@ backend directive — skip if backend doesn't match. // `extract` and `info` are backend-neutral and always run. @@ -424,7 +426,7 @@ function runFile( // Record check/regen runs in the run log. Created after the proof-dir guard // 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 && runLogEnabled(options["run-log"]) + const log = logCmd && runLogOn ? new RunLog({ logDir: resolveLogDir(absPath, configFile), cmd: logCmd, sourcePath: absPath, extraFlags, lscVersion: lscVersion() }) : undefined; diff --git a/tools/src/run-log.ts b/tools/src/run-log.ts index c45431b..ceffa10 100644 --- a/tools/src/run-log.ts +++ b/tools/src/run-log.ts @@ -67,7 +67,7 @@ export const RUN_LOG_SCHEMA_VERSION = 1; /** * Where a run stopped: `diff` (additions-only check failed, Dafny never ran), - * `conflict` (regen merge conflict), `resolve` (Dafny produced no results), + * `conflict` (regen merge conflict), `resolve` (Dafny produced no member results), * `verify` (Dafny reported failures), or `ok`. */ export type RunStage = "ok" | "verify" | "resolve" | "diff" | "conflict"; @@ -87,7 +87,6 @@ export interface VerifyRecord { tsHash: string | null; dfyHash: string | null; lsc: string; - ci: boolean; } export interface RunLogInit { @@ -150,10 +149,14 @@ export class RunLog { return this.textLogDir === null ? [] : ["--log-format", `text;LogFileName=${this.textLogPath()}`]; } - /** Member outcomes from Dafny's text log, or null when Dafny wrote none. */ + /** + * Member outcomes from Dafny's text log, or null when it names no members: + * Dafny writes no file for a parse error and an empty one for a resolution error. + */ readResults(): MemberResults | null { if (this.textLogDir === null) return null; - return safely(() => parseTextLog(readFileSync(this.textLogPath(), "utf8"))); + const results = safely(() => parseTextLog(readFileSync(this.textLogPath(), "utf8"))); + return results && results.passed.length + results.failed.length > 0 ? results : null; } /** Append this run's record. Never throws; only the first call writes. */ @@ -179,7 +182,6 @@ export class RunLog { tsHash: this.tsHash, dfyHash: safely(() => hashText(readFileSync(outcome.dfyPath, "utf8"))), lsc: this.init.lscVersion, - ci: Boolean(process.env.CI), }; 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 2d0ef8e..94b412f 100644 --- a/tools/tests/run-log.test.ts +++ b/tools/tests/run-log.test.ts @@ -1,5 +1,8 @@ import { test } from "node:test"; import assert from "node:assert/strict"; +import { spawnSync } from "node:child_process"; +import { createRequire } from "node:module"; +import { fileURLToPath } from "node:url"; import { chmodSync, existsSync, mkdirSync, mkdtempSync, readFileSync, realpathSync, rmSync, writeFileSync } from "node:fs"; import { tmpdir } from "node:os"; import { delimiter, join } from "node:path"; @@ -33,15 +36,17 @@ Results for arraySum (correctness) `; // A stand-in for `dafny`: writes $FAKE_DAFNY_LOG to the text log path it is -// given (if any) and exits with $FAKE_DAFNY_EXIT. +// given (if any, even when empty), creates any CSV log a user asked for, and +// exits with $FAKE_DAFNY_EXIT. const FAKE_DAFNY = `#!/bin/sh out="" for arg in "$@"; do case "$arg" in "text;LogFileName="*) out="\${arg#text;LogFileName=}" ;; + "csv;LogFileName="*) : > "\${arg#csv;LogFileName=}" ;; esac done -if [ -n "$out" ] && [ -n "$FAKE_DAFNY_LOG" ]; then printf '%s' "$FAKE_DAFNY_LOG" > "$out"; fi +if [ -n "$out" ] && [ "\${FAKE_DAFNY_LOG+set}" = set ]; then printf '%s' "$FAKE_DAFNY_LOG" > "$out"; fi exit "\${FAKE_DAFNY_EXIT:-0}" `; @@ -64,13 +69,13 @@ function withFakeDafny(env: { log?: string; exit?: number }, run: (root: string) } } -function verifyWithLog(root: string): boolean { +function verifyWithLog(root: string, opts: { extraFlags?: string; proof?: string } = {}): boolean { const source = join(root, "a.ts"); const dfy = join(root, "a.dfy"); writeFileSync(source, "export const a = 1;\n"); - writeFileSync(dfy, "lemma L() {}\n"); - const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, lscVersion: "0" }); - return dafnyVerify(dfy, root, undefined, undefined, log); + writeFileSync(dfy, opts.proof ?? "lemma L() {}\n"); + const log = new RunLog({ logDir: root, cmd: "check", sourcePath: source, extraFlags: opts.extraFlags, lscVersion: "0" }); + return dafnyVerify(dfy, root, undefined, opts.extraFlags, log); } function checkDiffWithLog(root: string, generated: string, proof: string): boolean { @@ -155,6 +160,23 @@ test("LSC_RUN_LOG accepts only true or false, like lemmascript.json", () => { } }); +test("a bad LSC_RUN_LOG is rejected by every file command, not only check and regen", () => { + const root = tempDir(); + try { + const source = join(root, "a.ts"); + writeFileSync(source, "export function identity(value: number): number { return value; }\n"); + const cli = fileURLToPath(new URL("../src/lsc.ts", import.meta.url)); + const loader = createRequire(import.meta.url).resolve("tsx"); + const result = spawnSync(process.execPath, ["--import", loader, cli, "gen", "--backend=dafny", source], { + cwd: root, env: { ...process.env, LSC_RUN_LOG: "0" }, encoding: "utf8", timeout: 30_000, + }); + assert.equal(result.status, 1, result.stdout); + assert.match(result.stderr, /LSC_RUN_LOG must be true or false/); + } finally { + rmSync(root, { recursive: true, force: true }); + } +}); + test("the log lives beside lemmascript.json, else at the git root, else in cwd", () => { const root = tempDir(); try { @@ -216,7 +238,7 @@ test("finish appends one complete record and ignores later calls", () => { const [r, ...rest] = records(root); assert.equal(rest.length, 0); assert.deepEqual(Object.keys(r).sort(), [ - "ci", "cmd", "dfyHash", "exit", "failed", "file", "id", "lsc", "partial", "passed", "stage", "ts", "tsHash", "type", "v", + "cmd", "dfyHash", "exit", "failed", "file", "id", "lsc", "partial", "passed", "stage", "ts", "tsHash", "type", "v", ]); assert.equal(r.v, 1); assert.equal(r.type, "verify"); @@ -231,7 +253,6 @@ test("finish appends one complete record and ignores later calls", () => { assert.equal(r.tsHash, hashText("export const a = 1;\n")); assert.equal(r.dfyHash, hashText("lemma L() {}\n")); assert.equal(r.lsc, "9.9.9"); - assert.equal(typeof r.ci, "boolean"); assert.ok(existsSync(join(root, ".lemmascript", "blobs", `${r.tsHash}.ts`))); } finally { rmSync(root, { recursive: true, force: true }); @@ -321,6 +342,38 @@ test("a Dafny run that writes no results is recorded as resolve", posixOnly, () assert.equal(r.partial, true); })); +test("a Dafny resolution error, which writes an empty results file, is recorded as resolve", posixOnly, () => + withFakeDafny({ log: "", exit: 2 }, root => { + assert.equal(verifyWithLog(root), false); + const [r] = records(root); + assert.equal(r.stage, "resolve"); + assert.equal(r.partial, true); + })); + +test("a user's own --log-format still reaches Dafny alongside the run log's", posixOnly, () => + withFakeDafny({ log: "Results for L (correctness)\n Overall outcome: Correct\n", exit: 0 }, root => { + const mine = join(root, "mine.csv"); + assert.equal(verifyWithLog(root, { extraFlags: `--log-format csv;LogFileName=${mine}` }), true); + assert.ok(existsSync(mine), "the user's CSV log was not written"); + const [r] = records(root); + assert.equal(r.stage, "ok"); + assert.deepEqual(r.passed, ["L"]); + })); + +test("a proof lsc refuses before running Dafny is recorded as resolve", () => { + const root = tempDir(); + try { + // UTF-16 strings with Dafny's standard library: dafnyVerifyArgs refuses this combination. + const proof = "// lsc options: string-semantics=javascript-utf16\nimport opened Std.Strings\n"; + assert.equal(verifyWithLog(root, { proof }), false); + const [r] = records(root); + assert.equal(r.stage, "resolve"); + assert.equal(r.partial, true); + } finally { + rmSync(root, { recursive: true, force: true }); + } +}); + test("an additions-only failure is recorded as diff", () => { const root = tempDir(); try { From 448aab8390b5dcf32bfee73dde6a3e8f2af7b2f5 Mon Sep 17 00:00:00 2001 From: Annie Vella Date: Mon, 5 Oct 2026 18:58:27 +1300 Subject: [PATCH 09/12] architecture review fixes: read LSC_RUN_LOG in lsc.ts, document it, opt-out fixture, docs --- DESIGN_RUN_LOG.md | 4 ++-- SPEC.md | 2 ++ TOOLS.md | 3 ++- site/src/content/docs/reference/cli.md | 3 ++- tools/src/lsc.ts | 4 ++-- tools/src/run-log.ts | 8 ++++---- tools/test-fixtures.sh | 9 +++++++++ tools/tests/run-log.test.ts | 14 +++++++------- 8 files changed, 30 insertions(+), 17 deletions(-) diff --git a/DESIGN_RUN_LOG.md b/DESIGN_RUN_LOG.md index 37e3a4d..c26e8b7 100644 --- a/DESIGN_RUN_LOG.md +++ b/DESIGN_RUN_LOG.md @@ -38,7 +38,7 @@ Logging is on by default. A project turns it off with a config-only entry in the `run-log` is config-only, not a `//@ option`: a file that could switch off its own logging would let an agent hide the failures the log exists to count. -The log lives in `.lemmascript/` in the directory that holds the selected `lemmascript.json`. Without a config file, it goes in the git repository root, or in the current working directory outside a repository. When `lsc` creates the directory, it writes `.lemmascript/.gitignore` containing `*`, so git ignores the whole directory without any change to the project's own `.gitignore`. +The log lives in `.lemmascript/` in the directory that holds the selected `lemmascript.json`. Without a config file, it goes in the git repository root, or in the current working directory outside a repository; in that last case the run history depends on where `lsc` is run from, so add a `lemmascript.json` to anchor it. When `lsc` creates the directory, it writes `.lemmascript/.gitignore` containing `*`, so git ignores the whole directory without any change to the project's own `.gitignore`. ``` .lemmascript/ @@ -220,7 +220,7 @@ The report file ends with one line per catch: its kind, label, file, failure dat |---|---| | `tools/src/config.ts` | Add a `run-log` registry entry (boolean, default `true`, config-only). | | `tools/src/run-log.ts` (new) | Create `.lemmascript/` with its `.gitignore`, append records, hash and snapshot files, read Dafny's text results file, derive catches, compute diffs and `change` hints, write labels, write dated reports and their markers. | -| `tools/src/dafny-commands.ts` | `dafnyCheckDiff`, `dafnyVerify` and `dafnyRegen` take an optional log context, and each records the stage it detects. `dafnyVerify` adds `--log-format text` and reads the member outcomes after Dafny exits; Dafny's output stays inherited. | +| `tools/src/dafny-commands.ts` | `dafnyCheckDiff`, `dafnyVerify` and `dafnyRegen` take an optional log context, and each records the stage it detects; recording lives there only because these helpers end runs with `process.exit`, and would move to `lsc.ts` if they returned outcomes instead. `dafnyVerify` adds `--log-format text` and reads the member outcomes after Dafny exits; Dafny's output stays inherited. | | `tools/src/lsc.ts` | Pass the log context from resolved options. Record claimcheck results in both branches. Add the `runs`, `runs label`, and `runs report` subcommands. | | `tools/fixtures/` | One fixture that goes fail → proof fix → pass, one that goes fail → code fix → pass (`code-only`), and one that goes fail → annotation fix → pass (`annotations-only`), checking the derived kinds and hints. | | `lemmascript-catch-report` skill (new, in lemmascript-skills) | Label unlabeled `source-fix` catches from `lsc runs --json` evidence, list open claimcheck disputes for the user, and write the report. | diff --git a/SPEC.md b/SPEC.md index 0a086ef..abb62e1 100644 --- a/SPEC.md +++ b/SPEC.md @@ -1334,6 +1334,8 @@ Default backend is Dafny. `extract` and `info` are backend-neutral and always ru - `--extra-flags=` — extra flags forwarded verbatim to the backend prover. - `--slow` — in batch mode, verify entries whose manifest timeout exceeds 60s (otherwise those get `gen-check`, unless `--time-limit` is supplied). +**Environment:** `LSC_RUN_LOG=false` turns the run log (§7.7) off for one invocation; `true` or unset leaves it to `run-log` in `lemmascript.json`. Any other value is an error. It is the only environment variable `lsc` reads. + In batch mode, `--time-limit` and `--extra-flags` independently override the corresponding manifest values; omitted options retain the per-entry settings. For Dafny `check`, an explicit timeout enables verification even above 60s without `--slow`. diff --git a/TOOLS.md b/TOOLS.md index fdaa10f..5b8edc3 100644 --- a/TOOLS.md +++ b/TOOLS.md @@ -172,7 +172,7 @@ not implement routing themselves. - `lsc regen --backend=dafny foo.ts` — regenerate `.dfy.gen`, three-way merge, verify - `lsc check --backend=dafny foo.ts` — gen + additions-only check + `dafny verify` -`check` and `regen` pass an optional `RunLog` (`run-log.ts`) to these helpers, and each records the stage it detects: `dafnyCheckDiff` records `diff`, `dafnyVerify` records `ok`/`verify`/`resolve`, and `dafnyRegen` records `conflict` and `--no-verify` runs. Dafny keeps inherited stdio; member outcomes come from `--log-format text` written to a temp file. +`check` and `regen` pass an optional `RunLog` (`run-log.ts`) to these helpers, and each records the stage it detects: `dafnyCheckDiff` records `diff`, `dafnyVerify` records `ok`/`verify`/`resolve`, and `dafnyRegen` records `conflict` and `--no-verify` runs. Recording lives in the helpers only because they end runs with `process.exit`; if they ever return outcomes instead, it belongs in `lsc.ts`. Dafny keeps inherited stdio; member outcomes come from `--log-format text` written to a temp file. ## Narrow Rules @@ -306,4 +306,5 @@ The Dafny emitter wraps `if-then-else` and `let` (var-binding) expressions in pa | `dafny-commands.ts` | CLI | Dafny gen/gen-check/regen/check commands | | `info-command.ts` | CLI | `lsc info` — per-function spec summary JSON; `--typed` — Typed IR contract for satellites | | `config.ts` | CLI/shared | Option registry, config discovery/validation, file overrides, artifact path mapping | +| `run-log.ts` | CLI | Run log: `.lemmascript/` directory, source snapshots, one record per Dafny `check`/`regen` | | `lsc.ts` | CLI | Wires the pipeline, dispatches to backend | diff --git a/site/src/content/docs/reference/cli.md b/site/src/content/docs/reference/cli.md index 5b57e66..1d5b58c 100644 --- a/site/src/content/docs/reference/cli.md +++ b/site/src/content/docs/reference/cli.md @@ -107,7 +107,8 @@ operations. Enabling `"string-semantics": "javascript-utf16"` requires explicitl `"dafny-library": "local"`; an omitted or explicit `stdlib` choice is an error. `run-log` (default `true`) records every Dafny `check` and `regen` in `.lemmascript/` -beside `lemmascript.json`: one line per run in `runs.jsonl` (the stage it stopped at and +beside `lemmascript.json` (without one, at the git repository root, or else in the current +directory): one line per run in `runs.jsonl` (the stage it stopped at and which members passed or failed) plus a snapshot of the source. The directory ignores itself in git, and logging never changes `lsc` output or exit codes. Set it to `false` to turn logging off for the project, or `LSC_RUN_LOG=false` for a single run. diff --git a/tools/src/lsc.ts b/tools/src/lsc.ts index f8a63ec..c2208ac 100755 --- a/tools/src/lsc.ts +++ b/tools/src/lsc.ts @@ -338,8 +338,8 @@ function runFile( const fullText = sourceFile.getFullText(); const { options, configFile } = effectiveOptions(absPath, fullText, configPath); - // Validate LSC_RUN_LOG for every command, as a bad config value would be. - const runLogOn = runLogEnabled(options["run-log"]); + // Checked here, for every command, so a bad LSC_RUN_LOG fails like a bad config value. + const runLogOn = runLogEnabled(options["run-log"], process.env.LSC_RUN_LOG); // Check //@ backend directive — skip if backend doesn't match. // `extract` and `info` are backend-neutral and always run. diff --git a/tools/src/run-log.ts b/tools/src/run-log.ts index ceffa10..fcd328d 100644 --- a/tools/src/run-log.ts +++ b/tools/src/run-log.ts @@ -46,11 +46,11 @@ export function isPartialRun(extraFlags: string | undefined): boolean { } /** - * `LSC_RUN_LOG=false` turns logging off for one run; `true` or unset leaves it - * to the config. Like lemmascript.json, any other value is an error. + * Combine the `run-log` option with the `LSC_RUN_LOG` value lsc.ts read: + * `false` turns logging off for one run; `true` or unset leaves it to the + * config. Like lemmascript.json, any other value is an error. */ -export function runLogEnabled(option: boolean, env: NodeJS.ProcessEnv = process.env): boolean { - const value = env.LSC_RUN_LOG; +export function runLogEnabled(option: boolean, value: string | undefined): boolean { if (value === undefined || value === "" || value === "true") return option; if (value === "false") return false; throw new Error(`LSC_RUN_LOG must be true or false (got ${JSON.stringify(value)})`); diff --git a/tools/test-fixtures.sh b/tools/test-fixtures.sh index 60ef9d4..1c51701 100755 --- a/tools/test-fixtures.sh +++ b/tools/test-fixtures.sh @@ -313,3 +313,12 @@ if (runs[1].dfyHash === runs[0].dfyHash || runs[2].dfyHash !== runs[0].dfyHash) ' "$run_log_dir/.lemmascript/runs.jsonl" grep -qx '\*' "$run_log_dir/.lemmascript/.gitignore" expect_absent .lemmascript + +# "run-log": false in lemmascript.json keeps logging off; LSC_RUN_LOG=true leaves +# the decision to the config rather than overriding it. +run_log_off_dir="$fixture_dir/run-log-off-project" +mkdir -p "$run_log_off_dir" +echo '{ "run-log": false }' > "$run_log_off_dir/lemmascript.json" +cp examples/arraySum.ts examples/arraySum.dfy "$run_log_off_dir/" +LSC_RUN_LOG=true npx tsx tools/src/lsc.ts check --backend=dafny "$run_log_off_dir/arraySum.ts" +expect_absent "$run_log_off_dir/.lemmascript" diff --git a/tools/tests/run-log.test.ts b/tools/tests/run-log.test.ts index 94b412f..6b4611a 100644 --- a/tools/tests/run-log.test.ts +++ b/tools/tests/run-log.test.ts @@ -146,17 +146,17 @@ test("filtered Dafny runs are partial", () => { }); test("LSC_RUN_LOG=false turns logging off for one run; true or unset defers to config", () => { - assert.equal(runLogEnabled(true, {}), true); - assert.equal(runLogEnabled(false, {}), false); - assert.equal(runLogEnabled(true, { LSC_RUN_LOG: "false" }), false); - assert.equal(runLogEnabled(true, { LSC_RUN_LOG: "true" }), true); - assert.equal(runLogEnabled(false, { LSC_RUN_LOG: "true" }), false); - assert.equal(runLogEnabled(true, { LSC_RUN_LOG: "" }), true); + assert.equal(runLogEnabled(true, undefined), true); + assert.equal(runLogEnabled(false, undefined), false); + assert.equal(runLogEnabled(true, "false"), false); + assert.equal(runLogEnabled(true, "true"), true); + assert.equal(runLogEnabled(false, "true"), false); + assert.equal(runLogEnabled(true, ""), true); }); test("LSC_RUN_LOG accepts only true or false, like lemmascript.json", () => { for (const value of ["0", "1", "no", "FALSE"]) { - assert.throws(() => runLogEnabled(true, { LSC_RUN_LOG: value }), /LSC_RUN_LOG must be true or false/); + assert.throws(() => runLogEnabled(true, value), /LSC_RUN_LOG must be true or false/); } }); From da82813506ace28e52abe5725bf7dac44e10b018 Mon Sep 17 00:00:00 2001 From: Annie Vella Date: Mon, 5 Oct 2026 19:21:17 +1300 Subject: [PATCH 10/12] don't record runs when dafny is not installed; tidy run-log.ts order --- DESIGN_RUN_LOG.md | 2 +- tools/src/dafny-commands.ts | 2 + tools/src/run-log.ts | 130 ++++++++++++++++++++---------------- tools/tests/run-log.test.ts | 32 +++++++++ 4 files changed, 106 insertions(+), 60 deletions(-) diff --git a/DESIGN_RUN_LOG.md b/DESIGN_RUN_LOG.md index c26e8b7..1444b64 100644 --- a/DESIGN_RUN_LOG.md +++ b/DESIGN_RUN_LOG.md @@ -68,7 +68,7 @@ The helper that detects how the run ended appends one record: `dafnyCheckDiff` f "lsc":"0.6.4"} ``` -- **`stage`** tells where the run stopped. `diff` means the additions-only check failed, so Dafny never ran. `resolve` means Dafny wrote no results (a parse or resolution error, or Dafny did not run). `conflict` means a `regen` merge conflicted. `verify` means Dafny ran and reported failures. `ok` means everything that ran passed. +- **`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. diff --git a/tools/src/dafny-commands.ts b/tools/src/dafny-commands.ts index 60575de..a56cc6b 100644 --- a/tools/src/dafny-commands.ts +++ b/tools/src/dafny-commands.ts @@ -158,6 +158,8 @@ export function dafnyVerify(dfyPath: string, dir: string, timeLimit?: number, ex } catch (e: any) { if (e?.code === "ENOENT") { console.error("ERROR: `dafny` not found on PATH — verification never ran. Install Dafny 4.x: https://dafny.org/"); + log?.discard(); + return false; } // Dafny writes no results when it stops at parsing or resolution. const results = log?.readResults() ?? null; diff --git a/tools/src/run-log.ts b/tools/src/run-log.ts index fcd328d..b29b51f 100644 --- a/tools/src/run-log.ts +++ b/tools/src/run-log.ts @@ -1,6 +1,7 @@ /** * Run log: record each Dafny `lsc check` / `lsc regen` run in - * `.lemmascript/runs.jsonl`, with a snapshot of the source, so that a later + * `.lemmascript/runs.jsonl` (a run where Dafny is not installed records + * nothing), with a snapshot of the source, so that a later * report can tell which failures were fixed and whether the fix changed the * program or only the proof. Logging must never change lsc's output or exit * code, so every filesystem step is best-effort and swallows its own errors. @@ -12,59 +13,13 @@ import { tmpdir } from "os"; import path from "path"; import { findUp } from "./config.js"; +export const RUN_LOG_SCHEMA_VERSION = 1; + export interface MemberResults { passed: string[]; failed: string[]; } -/** - * Parse Dafny's `--log-format text` file. Each member gets one entry per - * check (`correctness`, `well-formedness`); it passes only if every check's - * outcome is `Correct`. - */ -export function parseTextLog(text: string): MemberResults { - const seen = new Set(); - const failed = new Set(); - for (const m of text.matchAll(/^Results for (.+?) \([a-z-]+\)\r?\n\s+Overall outcome: (\S+)/gm)) { - seen.add(m[1]); - if (m[2] !== "Correct") failed.add(m[1]); - } - return { - passed: [...seen].filter(name => !failed.has(name)).sort(), - failed: [...failed].sort(), - }; -} - -/** First 12 hex characters of the SHA-256 of `text`. */ -export function hashText(text: string): string { - return createHash("sha256").update(text).digest("hex").slice(0, 12); -} - -/** A filtered Dafny run verifies only some members, so absences mean nothing. */ -export function isPartialRun(extraFlags: string | undefined): boolean { - return /--filter-(symbol|position)\b/.test(extraFlags ?? ""); -} - -/** - * Combine the `run-log` option with the `LSC_RUN_LOG` value lsc.ts read: - * `false` turns logging off for one run; `true` or unset leaves it to the - * config. Like lemmascript.json, any other value is an error. - */ -export function runLogEnabled(option: boolean, value: string | undefined): boolean { - if (value === undefined || value === "" || value === "true") return option; - if (value === "false") return false; - throw new Error(`LSC_RUN_LOG must be true or false (got ${JSON.stringify(value)})`); -} - -/** The selected lemmascript.json's directory, else the source's git root, else cwd. */ -export function resolveLogDir(sourcePath: string, configFile: string | null): string { - if (configFile) return path.dirname(path.resolve(configFile)); - const git = findUp(".git", sourcePath); - return git ? path.dirname(git) : process.cwd(); -} - -export const RUN_LOG_SCHEMA_VERSION = 1; - /** * Where a run stopped: `diff` (additions-only check failed, Dafny never ran), * `conflict` (regen merge conflict), `resolve` (Dafny produced no member results), @@ -97,6 +52,52 @@ export interface RunLogInit { lscVersion: string; } +/** + * Combine the `run-log` option with the `LSC_RUN_LOG` value lsc.ts read: + * `false` turns logging off for one run; `true` or unset leaves it to the + * config. Like lemmascript.json, any other value is an error. + */ +export function runLogEnabled(option: boolean, value: string | undefined): boolean { + if (value === undefined || value === "" || value === "true") return option; + if (value === "false") return false; + throw new Error(`LSC_RUN_LOG must be true or false (got ${JSON.stringify(value)})`); +} + +/** The selected lemmascript.json's directory, else the source's git root, else cwd. */ +export function resolveLogDir(sourcePath: string, configFile: string | null): string { + if (configFile) return path.dirname(path.resolve(configFile)); + const git = findUp(".git", sourcePath); + return git ? path.dirname(git) : process.cwd(); +} + +/** A filtered Dafny run verifies only some members, so absences mean nothing. */ +export function isPartialRun(extraFlags: string | undefined): boolean { + return /--filter-(symbol|position)\b/.test(extraFlags ?? ""); +} + +/** + * Parse Dafny's `--log-format text` file. Each member gets one entry per + * check (`correctness`, `well-formedness`); it passes only if every check's + * outcome is `Correct`. + */ +export function parseTextLog(text: string): MemberResults { + const seen = new Set(); + const failed = new Set(); + for (const m of text.matchAll(/^Results for (.+?) \([a-z-]+\)\r?\n\s+Overall outcome: (\S+)/gm)) { + seen.add(m[1]); + if (m[2] !== "Correct") failed.add(m[1]); + } + return { + passed: [...seen].filter(name => !failed.has(name)).sort(), + failed: [...failed].sort(), + }; +} + +/** First 12 hex characters of the SHA-256 of `text`. */ +export function hashText(text: string): string { + return createHash("sha256").update(text).digest("hex").slice(0, 12); +} + function safely(fn: () => T): T | null { try { return fn(); @@ -123,8 +124,9 @@ export function snapshotSource(dir: string, text: string): string { } /** - * One verification run. `lsc.ts` creates it before generating; the code path - * where the run ends calls `finish` exactly once (later calls are ignored). + * One verification run. `lsc.ts` creates it before generating and passes it to + * the Dafny helpers; whichever helper sees how the run ended calls `finish`, or + * `discard` when nothing was verified. Only the first of these calls counts. */ export class RunLog { private readonly dir: string | null; @@ -139,10 +141,6 @@ export class RunLog { : safely(() => snapshotSource(this.dir!, readFileSync(init.sourcePath, "utf8"))); } - private textLogPath(): string { - return path.join(this.textLogDir!, "verify.txt"); - } - /** Extra Dafny arguments that write member outcomes to a temporary text log. */ dafnyArgs(): string[] { this.textLogDir = safely(() => mkdtempSync(path.join(tmpdir(), "lsc-run-log-"))); @@ -186,9 +184,23 @@ export class RunLog { appendFileSync(path.join(dir, "runs.jsonl"), JSON.stringify(record) + "\n"); }); } - if (this.textLogDir !== null) { - const tmp = this.textLogDir; - safely(() => rmSync(tmp, { recursive: true, force: true })); - } + this.removeTextLogDir(); + } + + /** End the run without a record, because nothing was verified (for example, no Dafny). */ + discard(): void { + if (this.done) return; + this.done = true; + this.removeTextLogDir(); + } + + private textLogPath(): string { + return path.join(this.textLogDir!, "verify.txt"); + } + + private removeTextLogDir(): void { + if (this.textLogDir === null) return; + const tmp = this.textLogDir; + safely(() => rmSync(tmp, { recursive: true, force: true })); } } diff --git a/tools/tests/run-log.test.ts b/tools/tests/run-log.test.ts index 6b4611a..40b4752 100644 --- a/tools/tests/run-log.test.ts +++ b/tools/tests/run-log.test.ts @@ -387,6 +387,38 @@ test("an additions-only failure is recorded as diff", () => { } }); +test("a run where Dafny is not installed is not recorded", posixOnly, () => { + const root = tempDir(); + const savedPath = process.env.PATH; + try { + mkdirSync(join(root, "empty-bin")); + process.env.PATH = join(root, "empty-bin"); + assert.equal(verifyWithLog(root), false); + assert.equal(existsSync(join(root, ".lemmascript", "runs.jsonl")), false); + } finally { + process.env.PATH = savedPath; + rmSync(root, { recursive: true, force: true }); + } +}); + +test("discard ends a run without a record and removes Dafny's temporary results folder", () => { + 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 file = log.dafnyArgs()[1].replace(/^text;LogFileName=/, ""); + const folder = join(file, ".."); + assert.ok(existsSync(folder)); + log.discard(); + log.finish({ stage: "ok", exit: 0, dfyPath: source }); + assert.equal(existsSync(folder), false); + assert.equal(existsSync(join(root, ".lemmascript", "runs.jsonl")), false); + } finally { + rmSync(root, { recursive: true, force: true }); + } +}); + test("a passing additions-only check leaves the run open for verification to record", () => { const root = tempDir(); try { From 8304f2f3f5e7a467908229e3c349e8fd3f6df2bc Mon Sep 17 00:00:00 2001 From: Annie Vella Date: Mon, 5 Oct 2026 19:28:23 +1300 Subject: [PATCH 11/12] tidy up run-log.test.ts order --- tools/tests/run-log.test.ts | 48 ++++++++++++++++++------------------- 1 file changed, 24 insertions(+), 24 deletions(-) diff --git a/tools/tests/run-log.test.ts b/tools/tests/run-log.test.ts index 40b4752..4b4dd2b 100644 --- a/tools/tests/run-log.test.ts +++ b/tools/tests/run-log.test.ts @@ -313,6 +313,24 @@ test("dafnyArgs points Dafny at a temporary text log that readResults parses", ( } }); +test("discard ends a run without a record and removes Dafny's temporary results folder", () => { + 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 file = log.dafnyArgs()[1].replace(/^text;LogFileName=/, ""); + const folder = join(file, ".."); + assert.ok(existsSync(folder)); + log.discard(); + log.finish({ stage: "ok", exit: 0, dfyPath: source }); + assert.equal(existsSync(folder), false); + assert.equal(existsSync(join(root, ".lemmascript", "runs.jsonl")), false); + } finally { + rmSync(root, { recursive: true, force: true }); + } +}); + // Recording `check` runs. test("a passing verification is recorded as ok with its members", posixOnly, () => @@ -374,19 +392,6 @@ test("a proof lsc refuses before running Dafny is recorded as resolve", () => { } }); -test("an additions-only failure is recorded as diff", () => { - const root = tempDir(); - try { - assert.equal(checkDiffWithLog(root, "method M() {}\n", "method Changed() {}\n"), false); - const [r] = records(root); - assert.equal(r.stage, "diff"); - assert.equal(r.exit, 1); - assert.equal(r.partial, true); - } finally { - rmSync(root, { recursive: true, force: true }); - } -}); - test("a run where Dafny is not installed is not recorded", posixOnly, () => { const root = tempDir(); const savedPath = process.env.PATH; @@ -401,19 +406,14 @@ test("a run where Dafny is not installed is not recorded", posixOnly, () => { } }); -test("discard ends a run without a record and removes Dafny's temporary results folder", () => { +test("an additions-only failure is recorded as diff", () => { 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 file = log.dafnyArgs()[1].replace(/^text;LogFileName=/, ""); - const folder = join(file, ".."); - assert.ok(existsSync(folder)); - log.discard(); - log.finish({ stage: "ok", exit: 0, dfyPath: source }); - assert.equal(existsSync(folder), false); - assert.equal(existsSync(join(root, ".lemmascript", "runs.jsonl")), false); + assert.equal(checkDiffWithLog(root, "method M() {}\n", "method Changed() {}\n"), false); + const [r] = records(root); + assert.equal(r.stage, "diff"); + assert.equal(r.exit, 1); + assert.equal(r.partial, true); } finally { rmSync(root, { recursive: true, force: true }); } From fefffe11b73040780dcfd11cff63eaf0aa4d4f78 Mon Sep 17 00:00:00 2001 From: Annie Vella Date: Mon, 5 Oct 2026 19:36:03 +1300 Subject: [PATCH 12/12] design doc status without planning terms --- DESIGN_RUN_LOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DESIGN_RUN_LOG.md b/DESIGN_RUN_LOG.md index 1444b64..d645e85 100644 --- a/DESIGN_RUN_LOG.md +++ b/DESIGN_RUN_LOG.md @@ -1,6 +1,6 @@ # DESIGN_RUN_LOG — Counting what verification caught -**Status:** slice 1 implemented (recording `check` and `regen` runs). `lsc runs`, claimcheck records, labels and reports are not yet built. A stopgap wrapper on the `lemmascript-catch-log` branch of lemmascript-skills confirmed the Dafny CSV approach against `lsc` 0.6.1, passing the flag through `--extra-flags`; slice 1 uses the text format instead (§2). +**Status:** recording of `check` and `regen` runs is implemented (§1–§2). `lsc runs`, claimcheck records, labels and reports are not yet built. A stopgap wrapper on the `lemmascript-catch-log` branch of lemmascript-skills confirmed the Dafny CSV approach against `lsc` 0.6.1, passing the flag through `--extra-flags`; the implementation uses the text format instead (§2). **Date:** September 2026 ## Goal