diff --git a/CHANGELOG.md b/CHANGELOG.md index 260b660e..da8fe628 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,7 +12,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/). ### Fixed -- **`vera compile` prints the E602 "function skipped" warning on the text error path** ([#1004](https://github.com/aallan/vera/issues/1004)). When a `CodegenSkip` drops a *called* function, the caller's dangling `call $f` fails WAT assembly with an opaque `unknown func`; the warning explaining *why* the function was dropped was suppressed on the text error path (the `--json` envelope already carried it) and is now printed alongside the error. The type-error text path is corrected the same way, so a warning alongside a type error is no longer dropped. +- **`vera compile` prints the E602 "function skipped" warning on the text error path** ([#1004](https://github.com/aallan/vera/issues/1004)). When a `CodegenSkip` drops a *called* function, the caller's dangling `call $f` fails WAT assembly with an opaque `unknown func`; the warning explaining *why* the function was dropped was suppressed on the text error path (the `--json` envelope already carried it) and is now printed alongside the error. The type-error and `--target wasi-p2` family-gate text paths are corrected the same way, so a warning alongside those errors is no longer dropped. ## [0.1.4] - 2026-07-11 diff --git a/README.md b/README.md index 4346671a..4e2bcb65 100644 --- a/README.md +++ b/README.md @@ -224,7 +224,7 @@ cp /path/to/vera/SKILL.md ~/.claude/skills/vera-language/SKILL.md ## Project status -Vera is in **active development** at v0.1.4: 1,900+ commits, 202 releases, 7,403 tests, 91% code coverage, 157 conformance programs, 38 examples, and a 14-chapter specification. Known bugs and limitations are tracked in **[KNOWN_ISSUES.md](KNOWN_ISSUES.md)**. See **[HISTORY.md](HISTORY.md)** for how the compiler was built. +Vera is in **active development** at v0.1.4: 1,900+ commits, 202 releases, 7,404 tests, 91% code coverage, 157 conformance programs, 38 examples, and a 14-chapter specification. Known bugs and limitations are tracked in **[KNOWN_ISSUES.md](KNOWN_ISSUES.md)**. See **[HISTORY.md](HISTORY.md)** for how the compiler was built. The reference compiler — parser, AST, type checker, contract verifier (Z3), WASM code generator, module system, browser runtime, and runtime contract insertion — is working. The language specification is in draft across [14 chapters](spec/). diff --git a/ROADMAP.md b/ROADMAP.md index 7650f01f..593d45a9 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -12,7 +12,7 @@ Ordering derives from the design principles ([DESIGN.md](DESIGN.md)): verificati ## Where we are -7,403 tests, 157 conformance programs, 38 examples, 14 spec chapters. [KNOWN_ISSUES.md](KNOWN_ISSUES.md) tracks the open bugs — burndown material rather than stage work — plus the *limitations* the stages below retire. +7,404 tests, 157 conformance programs, 38 examples, 14 spec chapters. [KNOWN_ISSUES.md](KNOWN_ISSUES.md) tracks the open bugs — burndown material rather than stage work — plus the *limitations* the stages below retire. ## Stage 19 — The verification completeness sprint diff --git a/TESTING.md b/TESTING.md index 09c804b2..de49abae 100644 --- a/TESTING.md +++ b/TESTING.md @@ -6,7 +6,7 @@ This is the single source of truth for Vera's testing infrastructure, coverage d | Metric | Value | |--------|-------| -| **Tests** | 7,403 across 120 files (~104,000 lines of test code; 7,307 passed + 26 stress, 70 skipped) | +| **Tests** | 7,404 across 120 files (~104,000 lines of test code; 7,308 passed + 26 stress, 70 skipped) | | **Compiler code coverage** | 95% Python, 61% JavaScript — 91% combined (CI minimum: 80%) | | **Conformance programs** | 157 programs across 9 spec chapters, validating every language feature | | **Example programs** | 38, all validated through `vera check` + `vera verify` | @@ -138,7 +138,7 @@ python scripts/check_wheel_availability.py # pre-flight: every runtime | `test_errors.py` | 62 | 657 | Error code registry, diagnostic formatting, serialisation, SourceLocation, and error display sync — the canonical `E001` diagnostic must match each of its mirrors: `README.md`, `docs/index.html`, `spec/00-introduction.md`, `AGENTS.md`'s example `--json` block, and the hardcoded example in `scripts/build_site.py` that generates `docs/index.md` (#829; `AGENTS.md`'s ellipsis-truncated description/rationale are prefix-compared, its `error_code`/`spec_ref`/`fix` exactly) | | `test_eq_contract_874.py` | 11 | 378 | `eq`/`compare` ability ops in contract position: codegen canonicalization + verifier Tier-1 discharge/counterexample, where-fn contracts, compare Ordering-sort materialization, shadowing guard (#874) | | `test_formatter.py` | 130 | 1,074 | Comment extraction, interior comment positioning, expression/declaration formatting, match arm block bodies, idempotency, parenthesization, spec rules, ability declarations | -| `test_cli.py` | 263 | 4,109 | CLI commands (check, verify, compile, run, serve, test, fmt, version, quiet), subprocess integration, JSON error paths (including the `verify --json` `obligations` array and its summary-reproducibility pin, #967), runtime traps, arg validation, multi-file resolution, IO exit codes, --explain-slots, `builtins`/`effects`/`errors` introspection dispatch, and a USAGE-completeness guard (every dispatched `cmd_` handler has a help row) | +| `test_cli.py` | 264 | 4,142 | CLI commands (check, verify, compile, run, serve, test, fmt, version, quiet), subprocess integration, JSON error paths (including the `verify --json` `obligations` array and its summary-reproducibility pin, #967), runtime traps, arg validation, multi-file resolution, IO exit codes, --explain-slots, `builtins`/`effects`/`errors` introspection dispatch, and a USAGE-completeness guard (every dispatched `cmd_` handler has a help row) | | `test_introspect.py` | 38 | 192 | `vera builtins/effects/errors --json` registry introspection (#539): the `{schema, items}` envelope, count-equals-registry differential per registry, error-phase derivation, effect/ability `kind` tagging, the parameterised `Exn` effect, and best-effort `since` attribution with full-coverage guards | | `test_resolver.py` | 20 | 602 | Module resolution, path lookup, parse caching, circular import detection, the E011/E012/E013 diagnostic contract, internal-error isolation (a compiler bug is not masked as E013), and the transitive-closure return of `resolve_imports` (#890 — a diamond yields each reachable module once, direct imports tagged `direct`, the transitive one not) | | `test_types.py` | 73 | 388 | Type operations: subtyping, effect subtyping, equality, substitution, pretty-printing, canonical names | diff --git a/tests/test_cli.py b/tests/test_cli.py index efb735a5..3a658a39 100644 --- a/tests/test_cli.py +++ b/tests/test_cli.py @@ -815,6 +815,39 @@ def test_compile_type_warnings_shown_on_error_path_1004( assert "[E121]" in err # the type error still shows assert "[E200]" in err # the type warning previously dropped in text mode + # `main` uses `` (unsupported by wasi-p2), so `emit_wasi_component` + # raises AFTER a successful compile; `unused` is dropped with an E602 skip + # warning but is uncalled, so codegen still succeeds and the warning + # survives into `all_warnings`. + _WASI_P2_UNSUPPORTED_WITH_WARNING = ( + "private fn unused(@Decimal -> @Int) " + "requires(true) ensures(hash(@Decimal.0) == 0) effects(pure) { 0 }\n" + "public fn main(@Unit -> @Int) " + "requires(true) ensures(true) effects() " + '{ let @Result = Http.get("http://example.com"); 0 }\n' + ) + + def test_compile_wasi_p2_warnings_shown_on_error_path_1004( + self, + tmp_path: Path, + capsys: pytest.CaptureFixture[str], + ) -> None: + """#1004 review: the ``--target wasi-p2`` family-gate error prints warnings. + + The family gate rejects ```` *after* a successful compile, so its + text error path must print accumulated warnings too — the third sibling + of the type-error and codegen-error paths. (The JSON envelope already + carried them.) + """ + path = _bad_vera(tmp_path, self._WASI_P2_UNSUPPORTED_WITH_WARNING) + rc = cmd_compile(path, target="wasi-p2") + assert rc == 1 + err = capsys.readouterr().err + assert "does not support" in err # the family-gate error still shows + assert "[E602]" in err # the skip warning previously dropped in text mode + # Ordering is the contract: warnings are flushed BEFORE the error. + assert err.index("[E602]") < err.index("Error: --target wasi-p2:") + def test_compile_syntax_error( self, tmp_path: Path, diff --git a/vera/cli.py b/vera/cli.py index d3869546..3059a5dd 100644 --- a/vera/cli.py +++ b/vera/cli.py @@ -481,6 +481,12 @@ def cmd_compile( "warnings": [w.to_dict() for w in all_warnings], }, indent=2)) return 1 + # Print warnings on this error path too (#1004 review): the + # wasi-p2 family gate rejects AFTER a successful compile, so + # accumulated warnings must not be dropped in text mode — + # the third sibling of the type-error and codegen-error paths. + for w in all_warnings: + print(f"warning: {w.format()}", file=sys.stderr) print(f"Error: {msg}", file=sys.stderr) return 1