Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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/).

Expand Down
2 changes: 1 addition & 1 deletion ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
4 changes: 2 additions & 2 deletions TESTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -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` |
Expand Down Expand Up @@ -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_<name>` 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_<name>` 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<T>` 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 |
Expand Down
33 changes: 33 additions & 0 deletions tests/test_cli.py
Original file line number Diff line number Diff line change
Expand Up @@ -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 `<Http>` (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(<Http>) "
'{ let @Result<String, String> = 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 ``<Http>`` *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
Comment thread
coderabbitai[bot] marked this conversation as resolved.
# 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,
Expand Down
6 changes: 6 additions & 0 deletions vera/cli.py
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down