Repository navigation
Dir.exist? asks for a directory, not for existence (fixes #125) - #126
jiro-by-nori[bot] wants to merge 1 commit into
Conversation
`runFS` answered `File#exist?` and `Dir#exist?` from one branch, so both asked
whether *something* was at the path. CRuby's `Dir.exist?` asks whether there is
a *directory* there: `Dir.exist?("/tmp/readme.txt")` is `false` for a regular
file, while the model answered `true` — a wrong boolean, not a gate, on an
ordinary modeled builtin (issue #7 step 3). `File#file?` and `File#directory?`
already discriminate on the payload; `Dir#exist?` now does too, answering
`false` for a missing path exactly as CRuby does (that is an answer, not a
gate).
Found by the filesystem corpus added in the previous commit: its first run
disagreed on this case. The case (`difftest/corpus/vfs/06-dir-exist.rb`) lands
here, and covers both file paths, both directory paths, a missing path, and
`File.exist?` on the same paths for contrast.
Validation: `bin/ruby-lean --compare` over the reproducer now agrees on all
seven lines. The model builds; the booted heap literal is unchanged; `lake
build` of the books package (every proof book) passes; `check-metatheory.sh`
passes (the booted heap still satisfies the proofs' assumptions), as does
`check-soundness.sh`; `make gen-check`'s five checks are fresh; feature loading
and FastPower's `check.rb` agree. Tier 0 of the differential test over
bootstraptest holds the recorded baseline exactly (1287 ran, 1087 agree, 194
gated, 0 disagree); the filesystem corpus is 5 agree and 1 gated; tier 3 and
the regressions corpus are unchanged (57/13 and 221 held/1 gated); the difftest
suite passes in CI mode (204 passed, 0 skipped); `make check-not-weakened`
reports CHECKS NOT WEAKENED.
Authored by Jiro, an autonomous agent (Nori sessions), on behalf of @sam-xif.
Co-authored-by: Nori <contact@tilework.tech>
ab56ce2 to
d66f6dd
Compare
![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 d66f6dd.
Checks observed: all green at this head — CI, proofs (build, every book, axioms, soundness, comparator), conformance (the model against CRuby), front-end (the desugarer against CRuby), lint, docs, checks not weakened.
Files reviewed (this PR's own diff, 3 files, 24 lines):
ruby-lean/RubyCore/Builtins/FS.leandifftest/corpus/vfs/06-dir-exist.rb,.json
Validation: no Lean toolchain or CRuby here, so the vfs tier was not re-run; CI covers it. I checked the new Dir#exist? arm against its immediate neighbours in the same match: it is now byte-for-byte the shape of File#directory? — VFS.lookup, then true only for a .dir payload, false on a miss — which is CRuby's semantics, and File#exist? keeps the existence question it is supposed to answer. The new corpus case pins exactly the distinguishing rows: Dir.exist? on a regular file, a file inside a directory, a directory, /tmp, a missing path; File.exist? on the file and on the missing path. No pinned count or baseline in the vfs corpus had to move, and the sidecar follows the {"vfs": "v1"} convention.
Risk: none in the change itself. One workflow caveat that a human should see: this PR's GitHub base is jiro/vfs-difftest-corpus, not main — it is stacked on #124, which touches the human-gated Makefile and is over the size limit. This approval covers only the three files above and is explicitly not approval of #124, which still needs @sam-xif.
Verdict: approve.
Fixes #125. Stacked on #124 (the filesystem corpus that found it): base is
jiro/vfs-difftest-corpus, and the new corpus case depends on that PR'sfixture. Merge #124 first.
What was wrong
runFSansweredFile#exist?andDir#exist?from one branch, so both askedwhether something was at the path. CRuby's
Dir.exist?asks whether there isa directory there:
Dir.exist?("/tmp/readme.txt")truefalseDir.exist?("/tmp/vfsdata/nums.txt")truefalseDir.exist?("/tmp/vfsdata")truetrueDir.exist?("/tmp/nope")falsefalseA wrong boolean rather than a refusal, so a program using the ordinary
Dir.exist?(p) ? … : …branch took the wrong branch.File#file?andFile#directory?immediately below it already discriminate on the payload.The change
ruby-lean/RubyCore/Builtins/FS.lean: split the branch.File#exist?isunchanged;
Dir#exist?is true only for a.dirpayload, andfalsefor amissing path (CRuby answers
falsethere, so that is an answer, not a gate).difftest/corpus/vfs/06-dir-exist.rb: the case the new corpus found, pinningboth file paths, both directory paths, a missing path, and
File.exist?onthe same paths for contrast.
Nothing in
books/mentions either builtin id, so no proof statement changes.Test plan
bin/ruby-lean --compareover the issue's reproducer:AGREEon all sevenlines (before:
DIFFERon the two file paths).lake buildof the books package: every proof book builds (1399 jobs).books/scripts/check-metatheory.sh: PASSED, including the booted heap'sassumptions;
books/scripts/check-soundness.sh: SOUNDNESS CHECK PASSED.make gen-check's five freshness checks: fresh.check-feature-loading.py: agree;books/Books/FastPower/check.rb: 72/72inputs agree.
gated, 0 disagree —
check-conformance.shholds the recorded baselineexactly, so no baseline update is owed.
--tier vfs --sut lean): 5 agree, 1 gated (the descriptorcase), 0 disagree. Tier 3: 57 agree / 13 gated. Regressions: 221 held, 1
gated, 0 regressed.
DIFFTEST_NO_SKIPS=1 uv run pytest: 204 passed, 0skipped.
make check-not-weakened: CHECKS NOT WEAKENED.Not run locally:
make checkas one command (this machine has no C toolchain,so
make depscannot install the pinned gems, andmakeitself is absent).Every target it runs was run individually, as listed above.
Authored by Jiro, an autonomous agent (Nori sessions), on behalf of
@sam-xif. The code and this description were written by the agent.