Repository navigation
IO#gets: honour the global input record separator $/ (fixes #64) - #95
jiro-by-nori[bot] wants to merge 6 commits into
Conversation
Add descriptors to the symbolic virtual filesystem of issue #7. A file is still a heap object; a descriptor is now one too. - Payload.io (inode, mode, pos, closed) and IOMode (read/write/append/ readWrite); each descriptor is its own object so per-descriptor position and closed-ness are observable, while the inode bytes stay shared. - File.open non-block, modes r/w/a/r+ (w truncates, a appends, r+ reads then overwrites at pos). IO#read (to EOF, or at most n, with the CRuby "" vs nil split), IO#write (byte count), IO#close, IO#closed?, IO#flush. - Class-object receivers keep the step-1 File.read/write and IO.read/write paths; .io receivers take the descriptor path. - File#open joins blockSensitiveBids: the block form (step 4) gates rather than silently running the block zero times. - Repr/Trace/nativeReprOwner gained the .io arm, still gating on rendering a descriptor (CRuby's File#inspect is path-bearing). - openIO allocates and mutates the heap, so runFS_frame needed a new openIO_frame lemma; it joins rootFrameLem and closes the same way. Missing path, closed stream, wrong-mode read, negative read length and the block form all gate with a named reason (Errno/IOError are step 7). Verified: lake build rubycore; RATCHET GREEN (run_typed_ratchet.sh, with and without RATCHET_SKIP_AGREEMENT=1); check-isolation.sh OK; check-proofs.sh OK (standard axioms). Model-vs-CRuby 4.0.5 byte-for-byte on a "hello\n" fixture for read/read(n)/read(0)/EOF, w-truncate, a-append, r+ read-then-write, and default mode. Co-authored-by: Nori <contact@tilework.tech>
…ach_line/pos/rewind) Step 5 of issue #7's ship order, over the step-2 descriptors. No new payload: every operation is a position move plus a slice of the inode's bytes. - IO#gets, all four CRuby forms: default "\n" separator, an Integer limit, a String separator, or both, plus gets(nil) reading to EOF. A separator runs through its first occurrence (whole remainder if absent), a limit truncates, and end of file answers nil. The surprising corner gets(0) = "" without moving the position, even at EOF, is modelled and pinned. - IO#pos reads the byte position; IO#pos= seeks (negative gates on the unmodeled Errno::EINVAL); IO#rewind returns the position to zero and answers 0. A closed descriptor gates on all three. - IO#readline and IO#each_line are prelude Ruby over gets, not primitives, so the block form is ordinary evaluation. readline's EOF case and the blockless each_line (CRuby answers an Enumerator a descriptor cannot build) gate by name rather than returning a guess. - ioId's builtin row gained readline/pos/pos=/rewind; gets and each_line were already listed by step 2 but unhandled, so they now resolve for real. No new proof lemma: gets/readline/pos=/rewind mutate the existing descriptor in place, the shape IO#read already had, so runFS_frame covers them. Verified: lake build rubycore/active-ratchet; CLINK REBUILD CHECKS PASS (125 certified, 0 gated, standard axioms); check-proofs.sh OK; check-isolation.sh OK; all 263 corpus programs still run with 0 hard failures. Model-vs-CRuby 4.0.5 byte-for-byte over the fixture /tmp/vfsdata/nums.txt for the gets/limit/separator matrix, pos, pos=, rewind, readline and block-form each_line. The full corpus gate (Sorbet pipeline) cannot run here because sorbet-static is absent (issue Authored by Nori (agent). Co-authored-by: Nori <contact@tilework.tech>
readline and each_line are prelude Ruby over gets, but the first cut took no
arguments, so readline("\n", 5) raised ArgumentError where CRuby answers and
each_line("2") gated. Both now take *args and forward them to gets, matching
CRuby's separator/limit arguments.
Verified: lake build rubycore/active-ratchet; model-vs-CRuby 4.0.5 byte-for-byte
for readline("2") and each_line("2") over /tmp/vfsdata/nums.txt.
Authored by Nori (agent).
Co-authored-by: Nori <contact@tilework.tech>
getsArgsH's two-argument branch only accepted a String separator, so gets(nil, 3) gated where CRuby reads the rest capped at 3. nil as the first argument means "no separator" (read the remainder), and the limit still applies; getsLine already applies the limit after choosing the line, so only the argument parser needed the case. Verified: lake build rubycore/active-ratchet; model-vs-CRuby 4.0.5 byte-for-byte for gets(nil, 3), gets(nil, 100) and gets(nil). Authored by Nori (agent). Co-authored-by: Nori <contact@tilework.tech>
Co-authored-by: Jiro <contact@tilework.tech>
The step-2 descriptor payload carries an IOMode, so deriving Repr for Payload needs an instance for it. Without this the boot-heap generator does not build once the descriptor branch is rebased onto current main. Co-authored-by: Jiro <contact@tilework.tech>
![jiro-approver-samxif[bot]](https://avatars.githubusercontent.com/u/9902953?s=60&v=4){kind=small}
There was a problem hiding this comment.
Reviewed head a76432e.
Verdict: cannot approve — 1,205 changed lines against max_changed_lines = 500. Unlike #103
and #96, a generated-file waiver alone would not unblock this one: after excluding the two
regenerated sources, the hand-authored delta is still ~527 lines.
Where the lines go
| File | Lines |
|---|---|
ruby-lean/RubyCore/Generated/PreludeJson.lean |
+302 / −291 |
ruby-lean/RubyCore/Builtins/FS.lean |
+332 / −26 |
ruby-lean/RubyCore/Generated/Prelude.lean |
+81 / −4 |
books/Books/TypeSoundness/Controls/InputRecordSeparatorControls.lean |
+50 (new) |
ruby-lean/prelude/prelude.rb |
+32 |
books/Books/Metatheory/Framing/RootFramePrimitives.lean |
+27 |
ruby-lean/RubyCore/Heap.lean |
+23 / −1 |
ruby-lean/RubyCore/Repr.lean |
+8 / −8 |
ruby-lean/RubyCore/Trace.lean |
+9 |
ruby-lean/RubyCore/Builtins/Support.lean |
+6 / −1 |
ruby-lean/GenBootedHeap.lean, ruby-lean/RubyCore/Boot.lean |
2 each |
Generated sources account for 678 lines; hand-authored work is 527 (the IO descriptor payload,
open/gets/pos/rewind/readline/each_line, the $/ lookup, a new framing lemma set, and
new runtime controls).
Checks observed at this head: all seven contexts green — CI, checks not weakened,
conformance, lint, docs, front-end, proofs. No unresolved review threads. No human-gated
path touched.
Validation: none run locally — no checkout or Lean toolchain in this session. In particular I did
not re-run make books for the new openIO_frame lemma or evaluate the #guard controls in
InputRecordSeparatorControls.lean; those rest on the green proofs context and the PR's reported
make metatheory / make books.
On the change itself: the $/ handling matches the stated rule — unset means "\n", nil reads
to EOF, a String is an arbitrary separator, and paragraph mode ($/ = "") plus non-String/non-nil
values gate by name instead of guessing. Reading $/ from m.globals rather than getGlobal so
"unset" and "explicitly nil" stay distinct is right. getsLine's limit = some 0 case answering
"" without moving the position is the CRuby probe result, and the controls pin it. IO/IOError
shapes gate rather than fabricate an exception object, which is rule 3. Nothing weakens a check.
What is needed (@sam-xif): this one is over the limit on its own merits, so it needs either a
human read of the FS.lean step-5 arm and the new framing lemma, or splitting — for example the
descriptor/open work (step 2) separate from the gets/$/' work (step 5). The generator reflow
issue raised on #103 applies here too but is not the binding constraint.
Summary
IO#gets— and thereforeIO#readlineandIO#each_line, which the prelude builds on it — now honours the global input record separator$/instead of always splitting on"\n". Fixes #64.$/is read at each call: unset means CRuby's default"\n",$/ = nilreads to end of file, and a String is used verbatim as the separator (including multi-character separators).gets(n)(andgets(nil, n)) uses$/too, as CRuby does.$/ = "") and non-String, non-nil separators gate by name rather than answering an approximated line or fabricating aTypeError.defaultRecordSep_frame/getsArgsH_frameand a#guardcontrol file pinning the separator matrix against the boot fixture/tmp/vfsdata/nums.txt("1\n2\n3\n").This PR is the
$/change stacked on the VFS step-2/step-5 descriptor work that it depends on, rebased onto currentmain. It supersedes #36 (the step-5 stack, rebased here) and #90 (the$/change, rebased onto it). It also derivesReprforIOModesogenbootedheapbuilds with the descriptor payload.Test plan
cd books && lake build— all 1400 targets, including the newInputRecordSeparatorControls#guards (default$/, multi-character separator,$/ = nil, paragraph-mode gate, non-String gate). Passed.uv run difftest run --tier 0 --sut lean— 1287 ran, 1087 agree, 194 unsupported, 6 not compared, 0 disagree.scripts/check-conformance.shprintedCONFORMANCE OK.books/scripts/check-soundness.sh—SOUNDNESS CHECK PASSED.books/scripts/check-metatheory.sh— meta-theory builds, axioms are withinpropext/Classical.choice/Quot.sound, booted-heap probes pass.DIFFTEST_NO_SKIPS=1 uv run pytestindifftest/— 164 passed, no skips.scripts/check-not-weakened.py—CHECKS NOT WEAKENED.make genequivalent:PreludeJson.lean,Prelude.lean,CRubyNames.lean,Unicode.leanand the audited-checker projections are all fresh.Authored by Jiro, an autonomous agent: both the code and this description.