feat(builtins): RFC 8259 json exponents, read_line stdin primitive, is_dir (#557 #558 #576)#586
Merged
Merged
Conversation
…s_dir (#557 #558 #576) - json_decode: exact RFC 8259 number grammar — negative exponents parse (1e-06; json_encode's own %.15g output round-trips); malformed tails (1e, 1e+, 1.) raise instead of atof-guessing (#557) - read_line of null: blocking getline(3) on stdin, line without trailing newline, null at EOF; tape-first (TAKE/RECORD like read_bytes — replay serves recorded lines, no live read); freestanding-excluded (#558); test_read_line.sh + suite [42a2] - is_dir of path: stat(2)+S_ISDIR next to file_exists; trace-recorded per the tape-first veto — the untraced legacy fs predicates (file_exists/ls/mkdir/getcwd/exe_path) are flagged as #585 instead of being silently matched (#576); replay test proves the recorded answer wins after the directory is deleted - LSP completions for both new builtins; BUILTINS.md/TRACE.md/CHANGELOG Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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.
Three consumer-filed core-builtin gaps, one per issue.
#557 — json_decode accepts RFC 8259 exponent notation
The number scanner accepted
e/E/+but never the-of a negative exponent, so1e-06(Pythonjson.dumps, JSJSON.stringify, serde — and EigenScript's ownjson_encode, whose%.15gemits scientific notation for tiny/huge magnitudes) failed at the sign: encode→decode did not round-trip.eigs_json_parse_numbernow scans the exact RFC §6 grammar ([minus] int [frac] [exp]) and raises on malformed tails ("1e","1e+","1.") instead of lettingatof()guess silently. Deliberately retained laxity: leading zeros (01) stay accepted, as before.Tests (tests/test_json_hard.eigs JH44–JH55): decode of
1e-06,1E+5,2.5e3, the issue's DeslanStudio value-6.179673164297128e-06, exponent inside an object; malformed tails raise catchable errors; both-direction round-trips for tiny/huge/negative-tiny magnitudes throughjson_encode.(DeslanStudio's exponent-free oracle-generator workaround can now be dropped — deliberately NOT touched here, that's DeslanStudio's repo.)
#558 —
read_line: stream-safe stdin readread_line of null— blockinggetline(3)on stdin: returns the next line without its trailing newline (\r\nstripped as one unit),nullat EOF,""for an empty line (distinguishable from EOF). Closes the pipeline hole:read_text of "/dev/stdin"sizes with fseek/ftell, which fails on unseekable fds, sogen | eigenscript client.eigssilently read"".Tape-first: nondeterministic input, wrapped with the
TRACE_NONDET_TAKE/TRACE_NONDET_RECORDpair likeread_bytes— underEIGS_REPLAYthe recorded lines are served and no live stdin read runs. Freestanding profile excludes it like the other IO builtins. Docs: BUILTINS.md row, TRACE.md wrapped-sources list.Tests (
tests/test_read_line.sh, new suite section [42a2], 7 checks): pipe delivery, empty-line-vs-EOF, unterminated final line, CRLF, seekable redirect, and the replay contract — record under piped stdin, replay with stdin at/dev/nullmust serve the recorded lines; tape carries exactly oneNrecord per call (2 lines + EOF null).NOT done (deliberate): the issue's alternative
read_textchunked-read fallback for unseekable fds —read_linecovers the consumer need (line-based CLI), and changingread_text's pipe behavior is a separate semantic decision.#576 —
is_diris_dir of path→ 1/0 viastat(2)+S_ISDIR, next to thefile_exists/ls/mkdir/renamefamily; replaces DeslanStudio'sfile_exists of f"{path}/."probe. Non-string / missing / plain file → 0.Tape treatment + the consistency finding the brief asked for: I checked how
file_existsis traced first — it is NOT traced (and not replay-blocked either; same forls,mkdir,getcwd,exe_path— they appear in neither of TRACE.md's lists and run live underEIGS_REPLAY). Per the standing tape-first veto for NEW nondet builtins,is_diris trace-recorded (TRACE_NONDET_RET) rather than matching the untraced legacy convention; the pre-existing inconsistency is filed as #585 rather than silently resolved either way here.Tests: functional checks in
tests/test_file_rename.eigs(dir / nested dir / plain file / missing / non-string; section count 12 → 17) and a replay check intests/test_replay.sh(record with the directory present, delete it, replay must still answer 1).Also
read_lineandis_dir(the LSP completion advertises aninputbuiltin that does not exist #559 fix keeps the list honest — both are real registrations).[Unreleased].Gates
detect_leaks=1: tally 0, [87] cleanmake jit-smoke,make freestanding-checkgreen (core touched)tools/doc_drift_check.shrc=0 ([99b] discoverability gate covers the two new BUILTINS.md rows)Closes #557
Closes #558
Closes #576
🤖 Generated with Claude Code