ci: emit verify-lite run summary and refresh docs (#1012) #1034

ootakazuhiko · 2025-10-05T21:07:29Z

Summary

add per-step status tracking to scripts/ci/run-verify-lite-local.sh and emit verify-lite-run-summary.json so Phase A runs can be shared as evidence for Plan: pipeline baseline & TLA+ PoC staging #1012
document the log collection workflow (with the new summary output) and connect the lint/mutation backlog plan to Issues Plan: pipeline baseline & TLA+ PoC staging #1012 / Mutation: calculateChecksum / reviveEntryData の surviving mutant を削減 #1016 for Phase C hand-off
note the JSON summary requirement when reporting verify-lite results so upcoming trace integration (ISSUE: TLA+ 全面活用構成の導入計画 #1011) can reuse the same data set

Testing

VERIFY_LITE_NO_FROZEN=1 VERIFY_LITE_KEEP_LINT_LOG=1 pnpm run verify:lite

Resolves #1012. Refs #1011.

github-actions · 2025-10-05T21:07:36Z

❓ Code Generation Drift Detection

Status:
Regeneration needed: No

Automated by AE-Framework Codegen

github-actions · 2025-10-05T21:07:39Z

Quality Summary

Adapters:
Formal: n/a
Replay: n/a
Trace IDs:

github-actions · 2025-10-05T21:07:58Z

🔍 Verification Summary

Traceability: 3 scenarios
- Tests: 3 (100%)
- Impl: 3 (100%)
- Formal: 3 (100%)

Unlinked (top 5)

Linked examples (up to 3)

- Successful reservation (id: successful-reservation) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/774ec767b7eb4f38bd4862da7da3bff2fb65bc2a/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/774ec767b7eb4f38bd4862da7da3bff2fb65bc2a/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/774ec767b7eb4f38bd4862da7da3bff2fb65bc2a/specs/formal/tla+/Inventory.tla) - Prevent negative stock (id: prevent-negative-stock) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/774ec767b7eb4f38bd4862da7da3bff2fb65bc2a/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/774ec767b7eb4f38bd4862da7da3bff2fb65bc2a/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/774ec767b7eb4f38bd4862da7da3bff2fb65bc2a/specs/formal/tla+/Inventory.tla) - Idempotent by order id (id: idempotent-by-order-id) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/774ec767b7eb4f38bd4862da7da3bff2fb65bc2a/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/774ec767b7eb4f38bd4862da7da3bff2fb65bc2a/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/774ec767b7eb4f38bd4862da7da3bff2fb65bc2a/specs/formal/tla+/Inventory.tla)

Hit basis (tests/formal)

- Test hits: title=3 id=0 tag=0 - Formal hits: title=0 id=3 tag=0

- Model Check (TLC): 2/8 (25%) modules ok

Non-OK modules (top 5)

- KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt) - KvOnceImpl (log: artifacts/codex/KvOnceImpl.tlc.log.txt) - KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt)

- Alloy: detected 2 specs (execution skipped) - Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=true pre=true post=true parseOut=true

github-actions · 2025-10-05T21:08:10Z

Generate Artifacts Preview

Generated at: 2025-10-05T23:40:22.930Z

tests/api/generated: clean
artifacts/codex: clean
artifacts/spec: clean

Copilot

Pull Request Overview

This PR adds comprehensive run summary generation to the verify-lite script and updates documentation to reflect new logging workflows. The changes enable better tracking and reporting of CI pipeline status for issue management and progress monitoring.

Implements JSON summary output with step status tracking and artifact paths
Updates documentation with detailed procedures for local log collection and issue reporting
Adds status variables and conditional logic to capture success/failure states for each pipeline step

Reviewed Changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 4 comments.

File	Description
scripts/ci/run-verify-lite-local.sh	Adds comprehensive status tracking and JSON summary generation for all pipeline steps
docs/notes/verify-lite-lint-plan.md	Updates with issue tracking workflow and log preservation policies
docs/notes/pipeline-baseline.md	Adds detailed procedures for local verify-lite log collection and minimal pipeline workflows

_{Tip: Customize your code reviews with copilot-instructions.md. Create the file or learn how to get started.}

scripts/ci/run-verify-lite-local.sh

github-actions · 2025-10-05T21:08:37Z

CodeX Artifacts Summary

• Contract/E2E templates: 1 files (dir: tests/api/generated)
• Tests: PBT files=122, BDD features=0
• Formal specs: TLA=1, Alloy=1

github-actions · 2025-10-05T21:09:51Z

KvOnce Trace Validation

OTLP: ✅ Success (Issues: 0)
NDJSON: ✅ Success (Issues: 0)

github-actions · 2025-10-05T23:39:47Z

❓ Code Generation Drift Detection

Status:
Regeneration needed: No

Automated by AE-Framework Codegen

ootakazuhiko · 2025-10-05T23:39:48Z

Addressed Copilot suggestions: standardized INSTALL_NOTES key/value format, extracted summary writer into scripts/ci/write-verify-lite-summary.mjs, and ensure summary script exits non-zero on failure.

github-actions · 2025-10-05T23:40:13Z

🔍 Verification Summary

Traceability: 3 scenarios
- Tests: 3 (100%)
- Impl: 3 (100%)
- Formal: 3 (100%)

Unlinked (top 5)

Linked examples (up to 3)

- Successful reservation (id: successful-reservation) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/da008cc32f11d649d24d51bd2659f045df879330/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/da008cc32f11d649d24d51bd2659f045df879330/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/da008cc32f11d649d24d51bd2659f045df879330/specs/formal/tla+/Inventory.tla) - Prevent negative stock (id: prevent-negative-stock) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/da008cc32f11d649d24d51bd2659f045df879330/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/da008cc32f11d649d24d51bd2659f045df879330/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/da008cc32f11d649d24d51bd2659f045df879330/specs/formal/tla+/Inventory.tla) - Idempotent by order id (id: idempotent-by-order-id) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/da008cc32f11d649d24d51bd2659f045df879330/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/da008cc32f11d649d24d51bd2659f045df879330/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/da008cc32f11d649d24d51bd2659f045df879330/specs/formal/tla+/Inventory.tla)

Hit basis (tests/formal)

- Test hits: title=3 id=0 tag=0 - Formal hits: title=0 id=3 tag=0

- Model Check (TLC): 2/8 (25%) modules ok

Non-OK modules (top 5)

- KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt) - KvOnceImpl (log: artifacts/codex/KvOnceImpl.tlc.log.txt) - KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt)

- Alloy: detected 2 specs (execution skipped) - Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=true pre=true post=true parseOut=true

github-actions · 2025-10-05T23:40:47Z

CodeX Artifacts Summary

• Contract/E2E templates: 1 files (dir: tests/api/generated)
• Tests: PBT files=122, BDD features=0
• Formal specs: TLA=1, Alloy=1

ci: emit verify-lite run summary and refresh docs (#1012)

774ec76

Copilot AI review requested due to automatic review settings October 5, 2025 21:07

ootakazuhiko mentioned this pull request Oct 5, 2025

Plan: pipeline baseline & TLA+ PoC staging #1012

Closed

10 tasks

ootakazuhiko mentioned this pull request Oct 5, 2025

ISSUE: TLA+ 全面活用構成の導入計画 #1011

Open

17 tasks

Copilot AI reviewed Oct 5, 2025

View reviewed changes

scripts/ci/run-verify-lite-local.sh Outdated Show resolved Hide resolved

scripts/ci/run-verify-lite-local.sh Outdated Show resolved Hide resolved

scripts/ci/run-verify-lite-local.sh Outdated Show resolved Hide resolved

scripts/ci/run-verify-lite-local.sh Outdated Show resolved Hide resolved

ci: refactor verify-lite summary writer per review

da008cc

ootakazuhiko merged commit 66a7bd7 into main Oct 5, 2025
67 of 68 checks passed

ootakazuhiko deleted the feature/verify-lite-run-summary branch October 5, 2025 23:50

ootakazuhiko mentioned this pull request Oct 6, 2025

Verify Lite/Trace パイプラインの堅牢化 (schema・ベースライン・共有レポート) #1036

Closed

10 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

ci: emit verify-lite run summary and refresh docs (#1012) #1034

ci: emit verify-lite run summary and refresh docs (#1012) #1034

ootakazuhiko commented Oct 5, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Oct 5, 2025

Uh oh!

github-actions bot commented Oct 5, 2025

Uh oh!

github-actions bot commented Oct 5, 2025

Uh oh!

github-actions bot commented Oct 5, 2025 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Oct 5, 2025

Uh oh!

github-actions bot commented Oct 5, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Oct 5, 2025

Uh oh!

ootakazuhiko commented Oct 5, 2025

Uh oh!

github-actions bot commented Oct 5, 2025

Uh oh!

github-actions bot commented Oct 5, 2025

Uh oh!

Uh oh!

Uh oh!

ci: emit verify-lite run summary and refresh docs (#1012) #1034

ci: emit verify-lite run summary and refresh docs (#1012) #1034

Conversation

ootakazuhiko commented Oct 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Testing

Uh oh!

github-actions bot commented Oct 5, 2025

❓ Code Generation Drift Detection

Uh oh!

github-actions bot commented Oct 5, 2025

Quality Summary

Uh oh!

github-actions bot commented Oct 5, 2025

🔍 Verification Summary

Uh oh!

github-actions bot commented Oct 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Generate Artifacts Preview

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull Request Overview

Reviewed Changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Oct 5, 2025

CodeX Artifacts Summary

Uh oh!

github-actions bot commented Oct 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

KvOnce Trace Validation

Uh oh!

github-actions bot commented Oct 5, 2025

❓ Code Generation Drift Detection

Uh oh!

ootakazuhiko commented Oct 5, 2025

Uh oh!

github-actions bot commented Oct 5, 2025

🔍 Verification Summary

Uh oh!

github-actions bot commented Oct 5, 2025

CodeX Artifacts Summary

Uh oh!

Uh oh!

Uh oh!

ootakazuhiko commented Oct 5, 2025 •

edited

Loading

github-actions bot commented Oct 5, 2025 •

edited

Loading

github-actions bot commented Oct 5, 2025 •

edited

Loading