[jiro-by-nori]

What this fixes

Pathname#empty? was @path.empty? in the prelude — a question about the path String. CRuby 4.0 asks the file:

FileTest.directory?(@path) ? Dir.empty?(@path) : File.empty?(@path)

So the model inverted two shapes, and answered a wrong value rather than gating:

program (fixture /tmp/readme.txt = "hello\n")	model, before	CRuby 4.0.5
File.write("/tmp/readme.txt", ""); Pathname.new("/tmp/readme.txt").empty?	false	true
Pathname.new("").empty?	true	false
Pathname.new("/tmp/no-such-path").empty?	false	false
Pathname.new("/tmp/readme.txt").empty?	false	false

The non-empty-file case agrees, which is why the defect went unnoticed. no such file is false (that is File.zero?'s answer, not an error), so a missing path is not a gate either.

The change

ruby-lean/prelude/prelude.rb, class Pathname:

def empty?
  return false unless File.exist?(@path)
  if File.directory?(@path)
    __unsupported__("Pathname#empty?: directory emptiness needs Dir.empty? (gated at VFS step 3)")
  end
  File.size(@path).zero?
end

• A missing path is false, as CRuby's File.empty? answers.
• A regular file is File.size(path).zero?, so an empty file is true.
• Directory emptiness is Dir.empty?, which the model does not have (VFS step 3, issue Proposal: virtual filesystem with symbolic and dynamic modes for the Ruby semantics #7), so it gates by name rather than approximating with the directory's own non-emptiness. This is the option issue Pathname#empty? answers String#empty? instead of asking the filesystem, so it is a wrong answer #91 asks for.
• The Pathname class comment now says empty? is the one operation that is not a path-string question.

No other Pathname operation changed: to_s, basename, dirname, extname, sub, ==, inspect are untouched, and the method_missing guard is unchanged.

Tests

New difftest/tests/test_pathname_empty.py (runs under make difftest-test, 12 cases):

• answers — an emptied file and /tmp/vfsdata/nums.txt (boot content "1\n2\n3\n") emptied by File.write are true; a file with content, the empty path, a missing path and a trailing slash on a regular file are false. Every expected value was taken from CRuby 4.0.5 run over a real file tree with the same shapes (empty file, missing, "", file/, nonempty dir, empty dir).
• gates — Pathname.new("/tmp").empty? and Pathname.new("/tmp/vfsdata").empty? decline, and the reason names both Pathname#empty? and Dir.empty?.
• unchanged — to_s, basename.to_s and the empty path's to_s still answer.

On the previous prelude (git stash the prelude, rebuild, rerun) 5 of the 12 fail: both emptied-file answers, the empty path, and both directory gates. So the suite pins the defect, not just the fix.

How I validated it

Run locally on the branch, cold toolchain (Lean v4.32.2, CRuby 4.0.5):

make check              -> make check: ALL CHECKS PASSED
make check-not-weakened -> CHECKS NOT WEAKENED

• make lean — model builds from the regenerated prelude.
• make conformance — CRuby 4.0.5 over the 1287-program bootstraptest corpus: ran 1287, agree 1087, sut_unsupported 194, not_compared 6, disagree 0, exactly the recorded baseline; the regressions and tier3 tiers agree.
• make difftest-test — 213 passed (201 before; +12 here); coverage still holds its baseline (line 73.19 / branch 68.61), so no baseline file moved.
• make books, make metatheory, make soundness, make comparator, make desugar-test, make desugar-coverage, make feature-loading, make book-checks, make gen-check (regenerated Prelude.lean/PreludeJson.lean are fresh), make lint, make docs — all green under make check.

No recorded result fell; no check, theorem, test skip or lint suppression was added.

Provenance

Authored by Jiro, an autonomous agent, including this description.

Closes #91