Skip to content

Remove Git workflow section from CLAUDE.md - #1

Merged
janstrakowski merged 1 commit into
mainfrom
janstrakowski-patch-1
Aug 27, 2026
Merged

Remove Git workflow section from CLAUDE.md#1
janstrakowski merged 1 commit into
mainfrom
janstrakowski-patch-1

Conversation

@janstrakowski

Copy link
Copy Markdown
Owner

Removed detailed Git workflow instructions including branching strategy, feature landing process, and commit message guidelines.

@janstrakowski

Copy link
Copy Markdown
Owner Author

Test review.

Removed detailed Git workflow instructions including branching strategy, feature landing process, and commit message guidelines.
@janstrakowski
janstrakowski force-pushed the janstrakowski-patch-1 branch from 5b6d41d to e08fc10 Compare August 27, 2026 21:46
@janstrakowski
janstrakowski merged commit 9870122 into main Aug 27, 2026
4 checks passed
@janstrakowski
janstrakowski deleted the janstrakowski-patch-1 branch August 28, 2026 08:36
janstrakowski added a commit that referenced this pull request Aug 31, 2026
* Make `let rec` build cyclic data, and compare it by bisimulation

`SPEC.md` §6 has always said cycles are possible; nothing could construct
one. A `let rec` over a Table literal now can, so a social graph whose
friendships are mutual is expressible without a placeholder type, a `lazy`
keyword, or a second binding form.

The mechanism is evaluation order, not deferral. The Table is created and
bound to the name before any entry runs, so an entry can mention the Table it
belongs to; entries are then evaluated on demand rather than in source order,
so reaching `people.bob` while `.alice` is mid-flight evaluates `.bob` there
and then. That dissolves every dependency between entries that has a
topological order - which is why mutual references need nothing further, and
why a form binding several names at once is still not needed.

What survives is the residual true cycle: `.bob` reaching back into `.alice`,
already in progress and so with no value to give. Only that yields a forward
reference (rec_build.odin), filled the moment `.alice` completes. Storing one
is what makes the back-edge; inspecting one before it is filled is a
genuinely circular definition and fails with a message naming the entry.
Since every entry completes before the `let rec` returns, no finished value
can hold an unfilled one - which is why this is not one of §3's types.

Scope is deliberately narrow, and the docs say so: this builds cyclic
structures, finite graphs with back-edges, not unbounded ones. A stream that
constructs a fresh node per step still recurses to the depth limit. Only a
Table literal written directly as the bound value has entries to reorder;
`let rec x x + 1` still reports "undefined name".

Two things then have to cope with a graph rather than a tree:

- Equality is bisimulation, so two rings of the same shape built by separate
  bindings are the same value - §6 makes equality a question about content,
  and a pointer comparison would answer it wrongly. Assumptions live in a
  union-find with path compression, keeping it near-linear rather than the
  quadratic a visited-pair set would cost. The map is only created when two
  distinct Tables are first assumed equal, so scalar key lookup on the hot
  path of field access still allocates nothing.
- Printing labels the node a back-edge returns to, `#1{n: 1, self: #1}`, so
  output stays finite and the shape is legible. Acyclic values, including a
  sub-Table merely shared between two branches, print exactly as before.

Hashing a cyclic value is refused rather than hung on, alongside the existing
directory-File and Function gaps. §3 pins what a digest encodes, so choosing
a cyclic encoding is a spec decision; `SPEC.md` §6 records what the answer
looks like and `LANGUAGE.md` lists it as unbuilt.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Reconcile SPEC.md with what the evaluator actually does

Follow-up to the cyclic `let rec` commit, and an audit rather than just its
loose ends: three of these were already wrong before that change.

Already stale:

- §5 said a Table's hash sorts its entries "by key per §6's generic total
  order". It sorts by the key's *digest*, deliberately - §6's cross-type
  ordering is not built, and a digest order is deterministic without it.
- §5 filed hashing, equality and ordering under one heading, which reads as
  though equality were hash-derived. It is structural: entries matched by key
  and compared pairwise. Only `File` compares through its digest, because §3
  defines a File's identity that way. Split into two bullets.
- §8 named the nesting budget's constant `MAX_EVAL_DEPTH`; it has been
  `MAX_NEST_DEPTH` in eval.odin all along.

Stale as of the cyclic `let rec` change:

- §10 stated as a general rule that `rec` "changes which scope the value is
  computed in, and nothing else". True for every shape but the one the same
  section now describes at length, so both the rule and the two consequence
  bullets under it are qualified where they are stated rather than silently
  contradicted further down.
- §10's mutual-recursion bullet explained the one-`rec`-over-a-Table idiom as
  entries being closures over the scope holding the name. That was the whole
  story when only functions could do it. The Table is now bound before its
  entries run and the entries are demanded, which is why the same spelling
  works for data; the closure property still explains why a later call
  resolves, but it is no longer what makes the binding work.
- §8 enumerates failure sources and numbers them, so a circular definition is
  added as the sixth, next to the fourth and before the paragraph that draws
  the conclusion from the list. It is distinguished from the nesting budget:
  detected and named, rather than noticed by running out of stack.
- §15 presented `sha256` as total. It has one gap that is this document's
  rather than an implementation's - a cyclic value, whose digest §6 has not
  settled the encoding of.

Every behavioural claim added here was run against `hb` first: entry order
affecting neither equality nor the digest, the circular-definition message,
`sha256` of a cycle, and an unbounded `let rec` reaching the nesting budget
rather than the circularity check.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Fix cyclic equality reusing assumptions from a comparison that failed

Two unequal Tables could compare equal. Found by testing the case the
original tests missed - cyclic values used as Table *keys*:

  let rec g { .a = { .tag = "a", .next = g.b }, .b = { .tag = "b", .next = g.a } };
  let rec h { .a = { .tag = "a", .next = h.b }, .b = { .tag = "b", .next = h.a } };
  let X { [g.a] = 1, [g.b] = 2, .z = g.a };
  let Y { [h.b] = 2, [h.a] = 1, .z = h.b };
  X == Y        // was true; `g.a == h.b` is false on its own

The bisimulation walk is optimistic: descending into a pair of Tables it
records "assume these two are equal" and compares their entries under that
assumption. Those assumptions are only justified if the descent succeeds.
The header comment claimed nothing needed rolling back because a mismatch
returns false and discards the lot - true of the value spine, where every
caller propagates a false immediately, and false of the one loop that does
not: matching a key scans candidates and keeps going after a failure.

So a failed key match left claims behind. Matching `g.a` against the
candidate `h.b` fails, but not before asserting g.a ~ h.b; the later `.z`
comparison of exactly that pair then short-circuited to true on it.

Key matching is a self-contained question about two subgraphs, so it no
longer shares the walk's state at all - table_find compares each candidate
through values_equal, which makes its own. Isolation costs only the chance to
reuse a valid assumption, and cannot lose an answer: an isolated comparison
re-derives whatever it needs and still terminates on its own back-edges. The
scalar path is untouched, since a Bisim is a stack struct whose map is only
created when two distinct Tables are first assumed equal - and comparing a
scalar key never gets that far.

Five regression tests, covering this and the other gaps the same audit turned
up: different-period cycles that genuinely differ, a cycle against a finite
unrolling, symmetry (the two operands are not handled alike - one is walked,
the other looked up in), and a cyclic value as a key at all.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
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