Hacktoberfest 2026: the issues maintainers tagged for October, open and beginner-friendly. Browse Hacktoberfest issues

`IO.FS.realPath` reports every failure as `noFileOrDirectory` instead of classifying by `errno`

Open Beginner friendly
  • Is something wrong?
#15,683 0 comments 0 reactions 0 assignees View on GitHub

Maintainers usually reply within 1 day

Nobody has claimed this yet.

Assessment

Difficulty
2/5
Estimated time
1-3 hours
Newbie friendliness
66/100
Issue type
Bug
Clarity
Clearly specified
Activity status
Active
Tech stack
cpp
Domain
operating-systems

Research direction

The bug is in the Unix branch of lean_io_realpath in src/runtime/io.cpp, which calls mk_file_not_found_error (hardcoded ENOENT) instead of decode_io_error(errno, filename) as the other primitives do, such as readFile near line 424. Start there and check the Windows branch around line 1025, which ignores GetLastError(). Build the Repro.lean case from the issue to confirm ENOTDIR, ENAMETOOLONG and ELOOP. Done when realPath reports the same errno-based kinds as readFile on those paths.

Written by the indexing model from the issue text.

Description

bug
Prerequisites
Description

IO.FS.realPath maps every realpath(3) failure to IO.Error.noFileOrDirectory (with errno
hardcoded to ENOENT), instead of decoding errno like every other file primitive. Success is fine;
only the error kind is wrong, contradicting the docstring's promise that it "coincides with the POSIX
realpath function".

Context

Code that tells “not found” apart from “permission denied” / “not a directory” / “too many levels of
symbolic links” via IO.Error always gets noFileOrDirectory.

Steps to Reproduce
  1. Repro.lean:
def kind : IO.Error → String
  | .noFileOrDirectory _ c _ => s!"noFileOrDirectory(errno={c})"
  | .inappropriateType _ c _ => s!"inappropriateType(errno={c})"
  | .invalidArgument _ c _ => s!"invalidArgument(errno={c})"
  | e => s!"other: {e}"

def errKind (act : IO α) : IO String := do
  try
    let _ ← act
    return "no error"
  catch e => return kind e

def case (name p : String) : IO Unit := do
  IO.println s!"{name}: realPath {← errKind (IO.FS.realPath p)} | readFile {← errKind (IO.FS.readFile p)}"

def main : IO UInt32 := do
  IO.FS.writeFile "rp_file" "x"
  case "ENOTDIR      " ("rp_file" ++ "/x")
  IO.FS.removeFile "rp_file"
  case "ENAMETOOLONG " (String.ofList (List.replicate 300 'n'))
  let _ ← IO.Process.output { cmd := "sh", args := #["-c", "rm -f rp_loop; ln -s rp_loop rp_loop"] }
  case "ELOOP        " "rp_loop"
  return 0
  1. lean --run Repro.lean (or compile: lean Repro.lean -c Repro.c && leanc -O1 -o Repro Repro.c && ./Repro).

Expected behavior: realPath reports the same errno-based kind as readFile on the same path
(inappropriateType for ENOTDIR, invalidArgument for ENAMETOOLONG/ELOOP).

Actual behavior: realPath reports noFileOrDirectory(errno=2) for every path:

ENOTDIR      : realPath noFileOrDirectory(errno=2) | readFile inappropriateType(errno=20)
ENAMETOOLONG : realPath noFileOrDirectory(errno=2) | readFile invalidArgument(errno=36)
ELOOP        : realPath noFileOrDirectory(errno=2) | readFile invalidArgument(errno=40)
Versions
Lean (version 4.36.0-nightly-2026-10-13, x86_64-unknown-linux-gnu, commit b7725c34da98e6e2f6323d7f382448ddf31477fb, Release)
Linux 7.0.0-38-generic (x86_64)
Additional Information

On Unix, lean_io_realpath calls mk_file_not_found_error (io.cpp:1061),
which hardcodes errno = ENOENT (io.cpp:86),
while other primitives use decode_io_error (io.cpp:370, e.g. readFile at io.cpp:424).
Fix: return io_result_mk_error(decode_io_error(errno, filename));. The Windows branch (io.cpp:1025)
has the same problem, ignoring GetLastError().

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Dominant language
Lean
Stars
9.5k
Forks
1k
Avg merge
23h 14m
Merged PRs (30d)
273

Getting set up

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from leanprover/lean4

All issues in leanprover/lean4

Similar issues

More Operating Systems issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.