fix: explicit drive letter normalization in FilePath <-> URI conversions

src/Init/System/Uri.lean

@@ -83,33 +83,32 @@ a single unicode code point and these will also be decoded correctly. -/
 def unescapeUri (s: String) : String :=
   UriEscape.decodeUri s
 
-/-- Convert the given FilePath to a "file:///encodedpath" Uri
-where the encoded path may contain %xx escaping when needed. -/
+/-- Convert the given FilePath to a "file:///encodedpath" Uri. -/
 def pathToUri (fname : System.FilePath) : String := Id.run do
   let mut uri := fname.normalize.toString
   if System.Platform.isWindows then
+    -- normalize drive letter
+    -- lower-case drive letters seem to be preferred in URIs
+    if uri.length >= 2 && (uri.get 0).isUpper && uri.get ⟨1⟩ == ':' then
+      uri := uri.set 0 (uri.get 0).toLower
     uri := uri.map (fun c => if c == '\\' then '/' else c)
   uri := uri.foldl (fun s c => s ++ UriEscape.uriEscapeAsciiChar c) ""
   let result := if uri.startsWith "/" then "file://" ++ uri else "file:///" ++ uri
   result
 
 /-- Convert the given uri to a FilePath stripping the 'file://' prefix,
-ignoring the optional host name and unescaping any %HH escaped chars.
-It is also careful to create correct paths on Windows that start with a drive letter. -/
+ignoring the optional host name. -/
 def fileUriToPath? (uri : String) : Option System.FilePath := Id.run do
   if !uri.startsWith "file://" then
     none
   else
     let mut p := (unescapeUri uri).drop "file://".length
     p := p.dropWhile (λ c => c != '/') -- drop the hostname.
-    -- on windows the path "/c:/temp" needs to become "c:/temp"
-    -- but only when it is a valid drive letter.
-    if System.Platform.isWindows &&
-      p.length > 3 &&
-      "/" == (p.take 1) &&
-      ((p.drop 1).take 1).all Char.isAlpha &&
-      ":" == ((p.drop 2).take 1)  then
-      p := p.drop 1
+    -- On Windows, the path "/c:/temp" needs to become "C:/temp"
+    if System.Platform.isWindows && p.length >= 2 &&
+        p.get 0 == '/' && (p.get ⟨1⟩).isAlpha && p.get ⟨2⟩ == ':' then
+      -- see also `pathToUri`
+      p := p.drop 1 |>.modify 0 .toUpper
     some p
 
 end Uri