Repository navigation
IO#gets: honour the global input record separator $/ (fixes #64) - #90
Closed
jiro-by-nori[bot] wants to merge 1 commit into
Closed
jiro-by-nori[bot] wants to merge 1 commit into
jiro-by-nori[bot] wants to merge 1 commit into
Conversation
Co-authored-by: Jiro <contact@tilework.tech>
jiro-by-nori
Bot
force-pushed
the
jiro/issue-64-input-record-separator
branch
from
November 7, 2026 03:38
f386668 to
f6a0064
Compare
jiro-by-nori
Bot
changed the base branch from
nori/vfs-step5-gets-readline-pos
to
jiro/vfs-step5-signed
November 7, 2026 03:39
Contributor
Author
|
Closing this stacked PR: its base is the pre-November VFS step-5 branch, which predates |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Fixes #64:
IO#gets, and thereforeIO#readline/IO#each_line, now honours the global input record separator$/instead of always splitting on"\n".$/is read at each call, so changing it between reads takes effect.$/keeps CRuby's default"\n".$/ = nilreads to end of file.$/is used verbatim as the separator, including multi-character separators.gets(n)also uses$/, as CRuby does.$/ = "") and non-String/non-nil separators gate by name instead of answering an approximated line.The change also adds the framing lemma
getsArgsH_frame(framing must not change the machine's globals) and runtime controls that pin the separator matrix against the boot fixture/tmp/vfsdata/nums.txt.This PR is stacked on the step-5 work in #36. Its base branch
jiro/vfs-step5-signedis a signed copy of #36's tip (nori-git has to re-sign unsigned feature commits to publish them); the diff shown here is only the$/change. It depends on step 5's descriptorgetslanding first.Test plan
cd books && lake build(all 1,397 targets, including the newInputRecordSeparatorControls).bin/ruby-lean --compareover the fixture/tmp/vfsdata/nums.txt("1\n2\n3\n") for:$/→"1\n"$/ = "2"→"1\n2", then"\n3\n"$/ = nil→"1\n2\n3\n", thennil$/ = "2"withgets(2)→"1\n"$/ = "2"withreadlineand the block form ofeach_line$/ = ""gates withIO#gets: paragraph mode (an empty record separator) is not modelledrather than returning a guessed line.Authored by Jiro, an agent: both the code and this description.