fix: lake: check normalized packages directory path before rename (#3795

)

Normalize the relative packages directory paths in the pre-rename check
to avoid renames if the difference in paths is only in the path
separators. Also adds a log message on rename.

src/lake/Lake/Load/Main.lean

@@ -160,14 +160,13 @@ def Workspace.updateAndMaterialize
             modifyThe (NameMap PackageEntry) (·.insert entry.name entry)
       if let some oldRelPkgsDir := manifest.packagesDir? then
         let oldPkgsDir := ws.dir / oldRelPkgsDir
-        if oldPkgsDir != ws.pkgsDir && (← oldPkgsDir.pathExists) then
+        if oldRelPkgsDir.normalize != ws.relPkgsDir.normalize && (← oldPkgsDir.pathExists) then
+          logInfo s!"workspace packages directory changed; renaming '{oldPkgsDir}' to '{ws.pkgsDir}'"
           let doRename : IO Unit := do
             createParentDirs ws.pkgsDir
             IO.FS.rename oldPkgsDir ws.pkgsDir
           if let .error e ← doRename.toBaseIO then
-            error <|
-              s!"{rootName}: could not rename packages directory " ++
-              s!"({oldPkgsDir} -> {ws.pkgsDir}): {e}"
+            error s!"could not rename workspace packages directory: {e}"
     | .error (.noFileOrDirectory ..) =>
       logInfo s!"{rootName}: no previous manifest, creating one from scratch"
     | .error e =>