gap-3 test: assert resume-write behaviour, not the NOT NULL bit
ci / test (push) Successful in 55m32s

- test_column_notnull_probe_sees_gap3_outcome now branches on the
  post-ensure probe: when outcome is relaxed (PG; SQLite 3.53+)
  the resume write must land and read back NULL; on older SQLite
  the ALTER is swallowed and INSERT OR IGNORE drops the row
  (version-dependent boundary, not a migration failure).
- attempt_ledger.py comments updated: ALTER COLUMN DROP NOT NULL
  works on Postgres and SQLite 3.53.0+, swallowed before that.
- PG proof summary section 3.9/8 corrected to the same boundary.
This commit is contained in:
host committed 2026-11-06 05:24:20 +00:00
1 parent 2fcde375a4
commit 37ba6876bf
2 files changed
+36 -16

No files matched your search

+14 -11
View File
@@ -133,11 +133,12 @@ Persistence notes:
three legacy shapes migrated in place, both writers, PK,
idempotent ensure; see
``verification/codex-task-attempts-pg-proof-20261106.md``).
One gap-3-only step is Postgres-only by nature: a gap-3
table's ``outcome`` was created NOT NULL, and ``ensure``
relaxes it with ``ALTER COLUMN outcome DROP NOT NULL``
(see ``ensure_task_attempts_table``); on SQLite that
statement is not valid and the column stays NOT NULL.
One gap-3-only step relaxes a gap-3 table's ``outcome``
from NOT NULL with ``ALTER COLUMN outcome DROP NOT NULL``
(see ``ensure_task_attempts_table``); the statement works
on Postgres and on SQLite 3.53.0+, and is swallowed by
``try/except`` on older SQLite, where the column stays
NOT NULL.
- The read path (``GET /metrics-report``) never creates the table:
a read-only endpoint must not mutate schema. Table creation
happens only on the write path, inside ``record_attempt`` /
@@ -310,8 +311,9 @@ def ensure_task_attempts_table(conn):
nullable or defaulted, so existing rows are never blocked,
and no row is dropped or rewritten. A gap-3 table's
``outcome`` was created NOT NULL; ensure also relaxes it to
nullable on Postgres (``ALTER COLUMN outcome DROP NOT
NULL``), because the resume writer inserts outcome NULL --
nullable (``ALTER COLUMN outcome DROP NOT NULL`` -- works
on Postgres and on SQLite 3.53.0+, swallowed on older
SQLite), because the resume writer inserts outcome NULL --
without the relax every resume write on such a table fails.
This replaces the
rehearsal-era runtime column-completion workaround: the
@@ -332,10 +334,11 @@ def ensure_task_attempts_table(conn):
# gap-3 形态的 outcome 是 NOT NULL,而统一 DDL 要求它可空
# (恢复写路不报 outcome,NOT NULL 会使它在 PG 上每次写
# 行都报 NotNullViolation)。只在探针报 NOT NULL 时放宽:
# Postgres 上是 ALTER COLUMN DROP NOT NULL(已是可空时
# 不会走到这里);SQLite 上该语句不合法,try/except 吞
# 掉——SQLite 的 gap-3 表仍保留 NOT NULL(放宽需重建表,
# 与“迁移不做重建式类型收紧”的边界一致,本批只修 PG 路径)。
# ALTER COLUMN outcome DROP NOT NULL 在 Postgres 上生效;
# SQLite 3.53.0 起也支持该语法,在此之前不合法、被
# try/except 吞掉,gap-3 表仍保留 NOT NULL(恢复写路
# 会被 INSERT OR IGNORE 静默丢弃——版本相关边界,见
# test_column_notnull_probe_sees_gap3_outcome)。
if _column_notnull(conn, "task_attempts").get("outcome"):
try:
conn.execute(