Skip to content

Add Hello World example and spec design notes#3

Merged
aallan merged 1 commit intomainfrom
spec-and-readme-updates
Feb 23, 2026
Merged

Add Hello World example and spec design notes#3
aallan merged 1 commit intomainfrom
spec-and-readme-updates

Conversation

@aallan
Copy link
Copy Markdown
Owner

@aallan aallan commented Feb 23, 2026

Summary

  • Add Hello World as the first example in README "What Vera Looks Like" section — the example humans will look for first
  • Add three forward-looking design notes to spec Chapter 0.8:
    • Abilities — Roc-style restricted type constraints, auto-derivable, no HKTs
    • LLM Inference<Inference> as an algebraic effect for AI runtime calls
    • Stdlib collectionsSet<T>, Map<K, V>, Decimal

Tagged as v0.0.5-1 (spec/docs update, not a compiler release).

Test plan

  • Verify README renders correctly on GitHub
  • Verify spec design notes are consistent with Chapters 2 (types) and 7 (effects)
  • No compiler changes — all pre-commit hooks pass

🤖 Generated with Claude Code

Add Hello World as first example in README "What Vera Looks Like"
section. Add three design notes to spec Chapter 0.8: Roc-style
restricted abilities, LLM inference as an algebraic effect, and
standard library collections (Set, Map, Decimal).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@aallan aallan merged commit 5c35fce into main Feb 23, 2026
5 checks passed
@aallan aallan deleted the spec-and-readme-updates branch February 23, 2026 08:27
aallan added a commit that referenced this pull request May 7, 2026
1. HISTORY.md "137 tagged releases" -> 138 (line 315): the v0.0.138
   row was added but the rollup footer count still said 137.

2. ROADMAP.md stabilisation-gate sentence: "order #5 starts when
   #1-#4 are closed" -> "order #4 starts when #1-#3 are closed".
   The earlier deletion of the #593 row (now closed) shifted the
   stabilisation tier to three items; the agent-integration tier
   numbering is also renumbered 5/6/7 -> 4/5/6 to match.

3. New test: test_eager_gc_array_mapi_with_non_allocating_string_closure
   mirrors the existing array_map String eager-GC test for the
   array_mapi unwind path with a fn(@Bool, @nat -> @string) closure
   returning pick(@Bool.0).  The existing array_mapi ADT test
   (test_array_mapi_non_allocating_closure_emits_balanced_push)
   covered the i32 branch; this new test covers the i32-pair branch.

4. Tighten the structural #593 predicate.  Pre-fix it accepted any
   "global.set $gc_sp" + absent "call $alloc"; CodeRabbit observed
   that a bare "global.set $gc_sp" could in principle be a stack-
   restore rather than a push.  In practice the prologue's
   gc_sp_save/restore is gated on ctx.needs_alloc and the regex
   already excludes call $alloc, so a non-allocating body cannot
   contain a restore -- but the literal predicate was weaker than
   the intent.  Adds _has_gc_shadow_push helper that anchors on the
   canonical "i32.const 4 / i32.add / global.set $gc_sp" SP-increment
   sequence emitted by gc_shadow_push (vera/wasm/helpers.py).  Used
   by both the i32-pair and i32-ADT structural tests; a non-push
   artefact in the body can no longer satisfy the assertion.

Plus: HISTORY.md tooling section gains a v0.0.138 row for
VERA_EAGER_GC alongside the existing tooling milestones (cross-
linked to ENVIRONMENT.md, which already has the full reference
section for it).

Suite: 3,747 passed (+1 from new array_mapi String test), 14 skipped.

Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan added a commit that referenced this pull request May 7, 2026
Two Conway's Life agent experiments on --target browser surfaced
five concrete blockers (issues #602/#603/#604/#609/#610) and an
explicit design memo (#608) mapping each obstacle to a concrete
runtime-only fix.  The current stabilisation framing covers
codegen reliability and walker completeness but treats browser-
target reliability as a separate concern.  The agent's diagnosis
makes that split harder to defend: "write once, run anywhere"
is currently true for pure computation and approximate-to-false
for anything with timing or screen output.  Two of the fixes
(#609 JSPI-driven IO.sleep, #610 ANSI subset interpreter) close
the timing and rendering halves of the seam without language
changes -- adding them to the stabilisation tier commits to
"browser-target Vera is something you'd actually use" before
the agent-integration push.

Changes:
- Expanded the campaign-pattern list from two patterns to three;
  third pattern documents the browser-target seam with links to
  the umbrella issue (#608) and the five concrete blockers.
- Added #609 (JSPI-driven IO.sleep) as item 3 in the stabilisation
  tier, with rationale + the WebAssembly JSPI / Asyncify mechanism.
- Added #610 (ANSI subset interpreter) as item 4 in the same tier,
  paired with #609 -- together they close the seam and let life.vera
  (terminal version) run unchanged on --target browser.
- Renumbered #595 from item 3 to item 5 (now last in stabilisation,
  since it's contingent on an upstream wasmtime-py release).
- Renumbered the agent-integration tier items 4/5/6 -> 6/7/8 to
  match.
- Updated the "What moves when" gate from "#4 starts when #1-#3
  are closed" to "#6 starts when #1-#5 are closed".

Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan added a commit that referenced this pull request May 8, 2026
PR #629 patched eight distinct triggers of the same canonical-name
canonicalisation drift, each one fixed locally. The underlying
pattern — five overlapping canonicalisation helpers in
`vera/wasm/inference.py` plus a silent fallthrough at
`vera/wasm/operators.py:482` that amplifies any inference miss
into invalid WASM — remains exposed.  The 9th trigger is a matter
of when, not if.

Filed #630 to close the bug class structurally:

  - Tier 1: fold the five helpers (`_format_named_type`,
    `_format_named_type_canonical`, `_resolve_i32_pair_ret_te`,
    `_resolve_base_type_name`, ad-hoc while-loops) into a single
    `_canonical_vera_type` covering RefinementType unwrap +
    alias-chain follow + generic substitution + format-with-args.
    Apply at every type-walking inference site.

  - Tier 2: convert the silent fallthrough at operators.py:482
    to a hard compile-time error. Dovetails with #626 Layer 1.

Together they make the 9th trigger either impossible (T1) or
instantly diagnosable (T2). Pure refactor + diagnostic
conversion — no behavioural change for any valid program; all
8 existing regression tests in TestStringInterpolation continue
to pin the now-fixed triggers.

Added to ROADMAP stabilisation tier as item #3 (after #604 and
#626; #630 is a sibling of #626 — single canonicalisation site
rather than the broader translator-returns-None pattern).
Renumbered the rest of the table.

Added to KNOWN_ISSUES.md "Bugs" section alongside #628 — both
are latent bug-class entries where individual instances are
patched but the underlying pattern remains exposed.

Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan added a commit that referenced this pull request May 8, 2026
…ents + CodeRabbit

Four review agents (code-reviewer, pr-test-analyzer, comment-analyzer,
silent-failure-hunter) plus three CodeRabbit comments produced a
batch of cross-cutting findings.  This commit addresses them all
in one pass to avoid the iterative round-trip cost the bug class
itself was filed to eliminate.

**Critical fixes:**

1. **Closure body E615 harvest gap (silent-failure-hunter C1).**
   `_compile_lifted_closure` constructed its own WasmContext but
   never harvested `_interp_inference_failures` — closure bodies
   with E615-triggering interpolation segments were silently
   dropped, producing call_indirect→missing-table-entry WASM
   validation traps with no source-located diagnostic.  Extracted
   the harvest into `CodeGenerator._harvest_interp_inference_failures`
   on the codegen base and called it from both functions.py and
   closures.py.  Removed the now-disproved `# pragma: no cover —
   defensive` claim on closures.py's body-instrs-None path.  New
   regression test `test_e615_in_closure_body_emits_diagnostic`.

2. **`_canonical_named_type` type_args from terminal NamedType
   (CodeRabbit #3 + code-reviewer I1).**  The walker's
   `outer_type_args` capture rule (always read from first NamedType)
   lost type_args when alias_map substitution bound a generic
   param to a parameterised type.  Empirically reachable today via
   `type Mapper<A, B> = fn(A -> B); Mapper<Int, Array<Int>>` etc.
   Fix: drop the "outermost" rule, return type_args from the
   terminal NamedType reached.  All 21 existing #602-class
   regression tests still pass.  New regression test
   `test_canonical_named_type_terminal_args_propagation`.

3. **HISTORY.md footer (CodeRabbit #1).**  141 tagged releases →
   142 to match the v0.0.142 row added in PR #631.

**UX fix:**

4. **Multiple E615 per function (silent-failure-hunter H2).**
   Pre-this-fix `_translate_interpolated_string` returned None on
   the first failing segment, requiring N round-trips for N bad
   segments in one interpolation.  Now collects every failing
   segment via `had_failure` flag, then bails at the end.  New
   regression test `test_multiple_e615_in_one_interpolation`.

**Doc-quality fixes (comment-analyzer):**

5. **Trigger-count drift** in `operators.py:491-494` —
   "every canonicalisation gap (#602 and ten subsequent triggers)"
   implied 11; rewrote to "the ten triggers of the #602 bug class
   accumulated across PRs #627 + #629".

6. **`_format_named_type_canonical` docstring drift** — claim
   "matches the pre-#630 fallback shape" was empirically wrong
   (pre-#630 resolved through aliases, post-#630 fallback doesn't).
   Rewrote to acknowledge the deliberate behavioural change.

7. **"Future closure-arg shapes plug in here without further
   dispatch ladder"** — overstatement.  Adding a `FnCall`
   returning a closure still needs an `elif`; what's saved is
   canonicalisation logic, not dispatch logic.  `IfExpr` between
   closures has no single `return_type` field — example was
   misleading.  Rewrote in both `_infer_fncall_vera_type` and
   `_infer_apply_fn_return_type`.

8. **`_canonical_wasm_type` docstring** — added explicit `Unit →
   None` documentation; clarified that `None` (no WASM type) and
   `"i64"` (unreachable-NamedType default) are distinct return
   shapes that callers must not conflate.

**Tests added (besides the regressions tied to fixes):**

9. **`test_per_function_isolation_of_failures_list`** — pins
   that a clean function and a dirty function in the same source
   produce independent `_interp_inference_failures` lists.

10. **`test_e615_fires_on_result_in_interpolation`** — adjacent
    ADT shape (Result vs Option) so a future Option-handling
    broadening doesn't accidentally regress the parallel Result
    path.

11. **`test_array_map_refinement_returning_closure`** — pins the
    previously-unaudited `_infer_closure_return_vera_type` path
    in `calls_arrays.py`, which the #630 migration broadened to
    handle refinements.

**Test enhancements:**

12. **E615 ordering before matching E602** in the existing test
    (CodeRabbit #2) — pinned via `warnings.index(e615[0])` <
    `warnings.index(matching_e602)`.  Filtered to the E602 that
    mentions the offending function so prelude-skip E602s don't
    confound the assertion.

13. **E615 source-location attached** in the existing test —
    softened to "line > 0" (any location) because SlotRef-inside-
    InterpolatedString spans are unreliable today (#634, separate
    follow-up).  Tightening to "line points at the segment" is
    the natural acceptance test for that follow-up.

**Skipped with reasons:**

- **Cycle-guard regression on `_resolve_base_type_name`** —
  test-analyzer C1 / code-reviewer S4.  Verified pre-existing
  and dead-code-safe today (cycles crash an upstream resolver
  first).  Filed as #633.

- **`_canonical_wasm_type`'s `i64` default for unhandled
  apply_fn / call_indirect shapes** — silent-failure-hunter H1.
  Bigger refactor parallel to Tier 2 but for the WASM-side
  dispatch.  Filed as #632.

- **SlotRef-inside-InterpolatedString span fidelity** —
  surfaced when writing the E615 source-location assertion.
  Diagnostic-quality concern, separate from #630's
  canonicalisation scope.  Filed as #634.

- **`_canonical_named_type` worked-example docstring**
  (comment-analyzer I6) — superseded by fix #2 above (semantics
  changed; docstring rewritten with concrete examples).

- **Per-context isolation prose-vs-test** (comment-analyzer I4)
  — addressed via fix #9 (test added).

- **`_resolve_i32_pair_ret_te` 30-line upper docstring** —
  comment-analyzer style nit.  The prose is load-bearing
  context (#628 cross-module narrative); trimming would lose
  history without obvious gain.  Defer.

**Follow-ups:** #632 (apply_fn / call_indirect E616), #633
(_resolve_base_type_name cycle guard), #634 (interpolation
SlotRef source spans).  Added to KNOWN_ISSUES.md alongside #628.

Counts: 3,792 tests (3,778 passed, 14 skipped) — six new tests
under `TestE615LoudInterpolationFallthrough630`.  CHANGELOG +
KNOWN_ISSUES + ROADMAP + TESTING.md + HISTORY footer all
synced.  mypy clean.

Co-Authored-By: Claude <noreply@anthropic.invalid>
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.

1 participant