testsuite: correct stale command-execution and exit-code docstrings - #145
Merged
Conversation
Contributor
|
Verifier report preview: https://talos-verifier-report-pr-145.vercel.app (This URL is stable for this PR — it always points to the latest build of f800259.) |
Follow-up to #130, fixing docstring inaccuracies that the same cleanup left in place. Behaviour unchanged — comments only. - The module docstring claimed "Only `module`, `assert_return`, `assert_trap`, and `action` are executed". `register` (executed since it records a binding) and `assert_exception` are also executed; list them. - It listed `assert_invalid`/`assert_malformed` under "reported as `Skipped(<kind>)`", but those are executed: we decode and validate the module, `Pass` on correct rejection, and `Skipped(<kind>: not rejected)` only on wrongful acceptance. This also matches the `skippedBucket` comment #130 added. - The "Exit code: nonzero iff any `Fail`/`InterpreterError`/`OutOfFuel`" line ignored the exit-code-3 setup-failure paths (bad args, unreadable testsuite dir, no matching files, temp-dir failure). Spell out both codes. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
mfornet
force-pushed
the
claude/fix-testsuite-docstrings
branch
from
July 14, 2026 12:26
769a647 to
f800259
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Follow-up to #130. That PR set out to fix stale testsuite docstrings but left three inaccuracies in the
Interpreter/Testsuite.leanmodule docstring (and, in one case, partially introduced an inconsistency by only half-updating a sentence). This is a comment-only change — no behaviour change.Fixes
Incomplete "executed" list. The docstring claimed "Only
module,assert_return,assert_trap, andactionare executed". Butregisteris executed (it records a binding — the testsuite: fix stale help/docstring text, drop dead helper #130 commit message itself says so;Exec.lean:746) and so isassert_exception(Exec.lean:804). Both are now listed.assert_invalid/assert_malformedmislabelled as skipped. They were listed under "reported asSkipped(<kind>)", but they are executed: we decode + statically validate the module, recordPasson correct rejection, andSkipped(<kind>: not rejected)only when we wrongly accept it (Exec.lean:826-836). This also aligns the top-of-file docstring with theskippedBucketcomment that testsuite: fix stale help/docstring text, drop dead helper #130 added lower in the same file.Exit-code claim ignored the setup-failure path. "Exit code: nonzero iff any
Fail,InterpreterError, orOutOfFueloutcome was recorded" omitted the exit-code-3paths (bad arguments, unreadable testsuite dir, no matching files, temp-dir creation failure). Both codes are now spelled out.Verification
Comment-only edit confined to the existing
/-! … -/docstring block; delimiters untouched. Local oleans are stale from the v4.32.0 toolchain bump (#144), so a full local rebuild would rebuild Mathlib — disproportionate for a docstring change; CI will build it.🤖 Generated with Claude Code