fix: resolve symbolic links through IO.FS.realPath on windows (leanprover#8534)

This PR fixes `IO.FS.realPath` on windows to take symbolic links into
account.

Closes leanprover#810

Author: Rob23oba

src/runtime/io.cpp

@@ -958,17 +958,35 @@ extern "C" LEAN_EXPORT obj_res lean_io_realpath(obj_arg fname, obj_arg) {
 #if defined(LEAN_WINDOWS)
     constexpr unsigned BufferSize = 8192;
     char buffer[BufferSize];
-    DWORD retval = GetFullPathName(string_cstr(fname), BufferSize, buffer, nullptr);
+    HANDLE handle = CreateFile(string_cstr(fname), 0, FILE_SHARE_READ, NULL, OPEN_EXISTING, FILE_FLAG_BACKUP_SEMANTICS, NULL);
+    if (handle == INVALID_HANDLE_VALUE) {
+        obj_res res = mk_file_not_found_error(fname);
+        dec_ref(fname);
+        return res;
+    }
+    DWORD retval = GetFinalPathNameByHandle(handle, buffer, BufferSize, 0);
+    CloseHandle(handle);
     if (retval == 0 || retval > BufferSize) {
         return io_result_mk_ok(fname);
     } else {
         dec_ref(fname);
+        char * res = buffer;
+        if (memcmp(res, "\\\\?\\", 4) == 0) {
+            if (memcmp(res + 4, "UNC\\", 4) == 0) {
+                // network path: convert "\\\\?\\UNC\\..." to "\\\\..."
+                res[6] = '\\';
+                res += 6;
+            } else {
+                // simple path: convert "\\\\?\\C:\\.." to "C:\\..."
+                res += 4;
+            }
+        }
         // Hack for making sure disk is lower case
         // TODO(Leo): more robust solution
-        if (strlen(buffer) >= 2 && buffer[1] == ':') {
-            buffer[0] = tolower(buffer[0]);
+        if (strlen(res) >= 2 && res[1] == ':') {
+            res[0] = tolower(res[0]);
         }
-        return io_result_mk_ok(mk_string(buffer));
+        return io_result_mk_ok(mk_string(res));
     }
 #else
     char buffer[PATH_MAX];

src/util/path.cpp

@@ -233,29 +233,4 @@ std::vector<std::string> read_dir(std::string const &dirname) {
 #endif
     return files;
 }
-
-std::string lrealpath(std::string const & fname) {
-#if defined(LEAN_EMSCRIPTEN)
-    return fname;
-#elif defined(LEAN_WINDOWS)
-    constexpr unsigned BufferSize = 8192;
-    char buffer[BufferSize];
-    DWORD retval = GetFullPathName(fname.c_str(), BufferSize, buffer, nullptr);
-    if (retval == 0 || retval > BufferSize) {
-        return fname;
-    } else {
-        return std::string(buffer);
-    }
-#else
-    constexpr unsigned BufferSize = 8192;
-    char buffer[BufferSize];
-    char * tmp = realpath(fname.c_str(), buffer);
-    if (tmp) {
-        std::string r(tmp);
-        return r;
-    } else {
-        throw file_not_found_exception(fname);
-    }
-#endif
-}
 }

src/util/path.h

@@ -44,6 +44,4 @@ optional<bool> is_dir(std::string const & fn);
 std::vector<std::string> read_dir(std::string const & dirname);
 
 time_t get_mtime(std::string const & fname);
-
-LEAN_EXPORT std::string lrealpath(std::string const & fname);
 }

tests/lean/run/parsePrelude.lean

@@ -1,9 +1,6 @@
 import Lean.Parser
 
-def test : IO Unit :=
-if System.Platform.isWindows then
-  pure () -- TODO investigate why the following doesn't work on Windows
-else do
+def test : IO Unit := do
   let env ← Lean.mkEmptyEnvironment;
   discard <| Lean.Parser.testParseFile env (System.mkFilePath ["..", "..", "..", "src", "Init", "Prelude.lean"]);
   IO.println "done"

tests/lean/run/realPath.lean

@@ -0,0 +1,27 @@
+/-!
+Tests that the `IO.FS.realPath` function on windows resolves links.
+-/
+
+/-
+Note: The test below circumvents #8547 by misusing quotation marks in order to run `mklink`.
+This test will need to be updated once that issue is fixed.
+-/
+
+def realPathTest : IO Unit := do
+  unless System.Platform.isWindows do
+    return
+  let dir ← IO.currentDir
+  let tmpDir := dir / "tmp_realpath_test_dir"
+  let tmpJunct := dir / "tmp_realpath_test_junction"
+  IO.FS.createDir (dir / tmpDir)
+  let cmd := "cmd.exe\" /c mklink /j \"" ++ tmpJunct.toString ++ "\" \"" ++ tmpDir.toString
+  discard <| IO.Process.run { cmd }
+  let realPath1 ← IO.FS.realPath tmpDir
+  let realPath2 ← IO.FS.realPath tmpJunct
+  IO.FS.removeDir tmpJunct
+  IO.FS.removeDir tmpDir
+  IO.println s!"{realPath1} vs {realPath2}"
+  if realPath1 != realPath2 then
+    throw (.userError ("mismatch " ++ realPath1.toString ++ " with " ++ realPath2.toString))
+
+#eval realPathTest