diff --git a/src/lake/Lake/Load/Manifest.lean b/src/lake/Lake/Load/Manifest.lean index 9856e8dd4cab..d8ba2a31d042 100644 --- 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 index 4818437cf41a..3835d83c2e22 100755 --- 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