RFC: Std.Path

Summary

This proposal replaces System.FilePath with Std.Path. FilePath is a plain String wrapper that relies on System.Platform functions to check the OS and handle platform differences such as path separators. Std.Path instead stores a parsed Array Path.Component, that makes all platform specific logic to IO so that path manipulation is pure by default. This proposal is inspired by Python's pathlib and Rust's pathlib crate.

Migration

Std.Path is a prerequisite for Std.FS (#13638) and will be implemented first. Several modules in Init/System/, like FilePath.lean, Uri.lean, and IO.lean, depend on path representation and will need to move to Std/ as part of this migration (Init/System/IO.lean itself is not changed, only the path-related surface area is relocated). The biggest impact is the removal of Coe String FilePath, which forces many files to be refactored to use functions that now require IO like Path.fromString; most of these changes affect Lake, requiring modifications to more than 60 files. Expressions like "src" / "Main.lean" will need an alternative for usability, either a macro or Path.ofPosixString "src/Main.lean" |>.get!. To keep backward compatibility during the transition, Init.System.FilePath and related files like Uri and IO.lean will be kept until the migration is complete, at which point they are deprecated and eventually removed. This full deprecation and removal is a long-term plan, intended for when Std.Path is mature and battle-tested.

Path

inductive Path.Component where
  | drivePrefix (value : String) -- Windows drive letter prefix, e.g. 'C' (from "C:")
  | root (s : String)            -- leading separator (/ on POSIX, \ on Windows)
  | current                      -- "."
  | parent                       -- ".."
  | normal (value : String)      -- ordinary path segment
deriving Inhabited, BEq, Hashable, Repr

structure Path where
  private mk ::
  components : Array Path.Component
deriving Inhabited, BEq, Hashable, Repr

API

Pure Operations

All of these work directly on the components array. No platform branching, no string parsing. But functions that accept string segments allow strings like "src/Main.lean" as a single segment. It is not split into multiple components, which means it has different meanings on different platforms (one single valid segment on Windows, two segments on POSIX).

IO Operations

Path.fromString and Path.toString are IO because detecting the platform separator requires reading runtime state.

URI Integration

Init.System.Uri exposes two functions used by the LSP: pathToUri and fileUriToPath?. Both uses System.FilePath and will need to be updated with Std.Path. I thought about creating a dedicated Std.URI for them but it would require:

• Measure the impact on the LSP, given that changing structures (from String to a dedicated URI type) can lead to more memory comsumption, allocations and indirections.
• A dedicated implementation based on RFC 3986 and probably a broader approach to Std.Http.Uri so it could be reused as part of the Http library (given that Http URI implementation restricts a lot of URIs to avoid security problems)

Start by reviewing the proposed API and migration plan, then inspect Init/System/FilePath.lean, Init/System/Uri.lean, and the path-related parts of Init/System/IO.lean. Done means implementing the proposed Std.Path representation and operations, then accounting for the dependent migration described in the issue; the proposal leaves usability details and the full deprecation timeline open.