Run log: record check and regen runs

[codefrenzy]

@graciolli-f @namin

Summary

The first part of DESIGN_RUN_LOG.md. Every Dafny lsc check and lsc regen appends one record to .lemmascript/runs.jsonl (stage reached, members passed and failed, .ts and .dfy hashes) and snapshots the .ts. The directory ignores itself in git, and logging never changes lsc output or exit codes. lsc runs, claimcheck records and reports come in later PRs.

Changes from the design

The design doc is updated to match; reasons are there.

• Dafny's text log instead of CSV, so Dafny's output stays inherited and the command path stays synchronous. Records don't carry error text yet.
• A partial flag, so a run that didn't check every member can't make one look dropped.
• A schema version (v) and a UUID id on every record, so the format can evolve and records stay unique if logs are ever combined.
• LSC_RUN_LOG takes true/false, like the config; anything else is an error.
• A run where Dafny isn't installed isn't recorded.

Testing

New unit tests in tools/tests/run-log.test.ts (fake dafny on PATH, as in dafny-regen.test.ts) and real-Dafny fixtures in test-fixtures.sh; existing fixtures run with logging off. Full suite 191/191, both typechecks, test-fixtures.sh and regen-lean.sh pass.

Open question

Capturing Dafny's error text needs piped output, which would make check/regen async. Worth it, or decide once there's a real log to look at?

[graciolli-f]

Thanks, @codefrenzy ! I tried it out — works reliably.

I think this is a design doc gap but the initial lsc gen followed by verify are not logged. Usually that's where most catches happen since it's the first iteration.

For now, we can skip the exact error text as long as it's clear whether it was a ts or dfy catch.