diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index e507e8140b1c..51ee7bb3881d 100644
--- a/src/runtime/io.cpp
+++ b/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];
diff --git a/src/util/path.cpp b/src/util/path.cpp
index c61acee262a1..4d84be1c17c8 100644
--- a/src/util/path.cpp
+++ b/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
-}
 }
diff --git a/src/util/path.h b/src/util/path.h
index 690bc4e15d83..1a3f421d3e82 100644
--- a/src/util/path.h
+++ b/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);
 }
diff --git a/tests/lean/run/parsePrelude.lean b/tests/lean/run/parsePrelude.lean
index 4fb358854230..c055522e39d0 100644
--- a/tests/lean/run/parsePrelude.lean
+++ b/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"
diff --git a/tests/lean/run/realPath.lean b/tests/lean/run/realPath.lean
new file mode 100644
index 000000000000..6c8b6dba29ff
--- /dev/null
+++ b/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