Skip to content

Document CheckStatus contract and enforce CLI status-output examples in CI - #13

Merged
enlorik merged 3 commits into
mainfrom
copilot/update-readme-checkstatus-documentation
Jul 22, 2026
Merged

Document CheckStatus contract and enforce CLI status-output examples in CI#13
enlorik merged 3 commits into
mainfrom
copilot/update-readme-checkstatus-documentation

Conversation

Copilot AI commented May 29, 2026

Copy link
Copy Markdown
Contributor

This follow-up codifies the CheckResult correctness contract (OK, ERROR, UNSUPPORTED) in project docs and adds explicit guardrails that CLI output continues to expose status-prefixed per-line results. The goal is to lock behavior before extending math feature scope.

  • Status contract documentation

    • Added a dedicated CheckResult contract section in README.md defining:
      • OK: claim proved by the trusted internal checker
      • ERROR: checked and false, or expression invalid
      • UNSUPPORTED: outside current supported domain
    • Updated result wording to reflect structured status output rather than binary pass/fail phrasing.
  • CLI output examples

    • Added explicit README examples showing current output shape for both success and failure:
      • Line N: OK
      • Line N: ERROR: ...
  • Workflow assertions for output contract

    • Updated CI steps to assert emitted output matches required status line formats:
      • ^Line [0-9]+: OK$
      • ^Line [0-9]+: ERROR:
    • Adjusted expected-failure command handling to preserve and report the checker’s exit code while still validating stderr/stdout content patterns.
# CI assertions added for output contract
./build/pearlproof test1.proof | tee /tmp/test1.out
grep -Eq '^Line [0-9]+: OK$' /tmp/test1.out

./build/pearlproof test_errors.proof > /tmp/test_errors.out
status=$?
grep -Eq '^Line [0-9]+: ERROR: ' /tmp/test_errors.out

Copilot AI changed the title Document CheckStatus contract and assert CLI status output Document CheckStatus contract and enforce CLI status-output examples in CI May 29, 2026
Copilot AI requested a review from enlorik May 29, 2026 16:19
@enlorik
enlorik marked this pull request as ready for review July 22, 2026 20:17
@enlorik
enlorik merged commit 1fccdf3 into main Jul 22, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants