feat: lake: use / in Windows manifest file paths

leanprover · Nov 2, 2023 · 4a5b2b8 · 4a5b2b8
1 parent 64561c0
commit 4a5b2b8
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 2 deletions.
diff --git a/src/lake/Lake/Load/Manifest.lean b/src/lake/Lake/Load/Manifest.lean
@@ -26,6 +26,17 @@ inductive PackageEntryV6
     (inputRev? : Option String) (subDir? : Option FilePath)
 deriving FromJson, ToJson, Inhabited
 
+/--
+Use `/` and instead of `\\` in file paths
+when serializing the manifest on Windows.
+-/
+local instance : ToJson FilePath where
+  toJson path :=
+    if System.Platform.isWindows then
+      Json.str <| path.toString.map fun c => if c = '\\' then '/' else c
+    else
+      Json.str path.toString
+
 /-- An entry for a package stored in the manifest. -/
 inductive PackageEntry
   /--

diff --git a/src/lake/tests/manifest/test.sh b/src/lake/tests/manifest/test.sh
@@ -36,7 +36,6 @@ $LAKE resolve-deps
 # Test update produces the expected V7 manifest
 $LAKE update
 sed_i "s/$REV/0538596b94a0510f55dc820cabd3bde41ad93c3e/g" lake-manifest.json
-sed_i 's/\\\\/\//g' lake-manifest.json # normalize Windows paths
 diff --strip-trailing-cr lake-manifest-v7.json lake-manifest.json
 
 # Test successful loading of a V6 manifest
@@ -47,5 +46,4 @@ $LAKE resolve-deps
 # Test update produces the expected V7 manifest
 $LAKE update
 sed_i "s/$REV/0538596b94a0510f55dc820cabd3bde41ad93c3e/g" lake-manifest.json
-sed_i 's/\\\\/\//g' lake-manifest.json # normalize Windows paths
 diff --strip-trailing-cr lake-manifest-v7.json lake-manifest.json