feat: warn on local changes to dependency & related fixes

src/lake/Lake/Load/Main.lean

@@ -158,7 +158,7 @@ def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) : LogIO Wor
               "use `lake update` to update"
           if let .some entry := manifest.find? dep.name then
           match dep.src, entry with
-          | .git (url := url) (rev := rev) .., .git (url := url') (rev := rev')  .. =>
+          | .git (url := url) (rev := rev) .., .git (url := url') (inputRev? := rev')  .. =>
             if url ≠ url' then warnOutOfDate "git url"
             if rev ≠ rev' then warnOutOfDate "git revision"
           | .path .., .path .. => pure ()

src/lake/Lake/Load/Materialize.lean

@@ -10,14 +10,23 @@ import Lake.Config.Package
 
 open System Lean
 
+/-! # Dependency Materialization
+Definitions to "materialize" a package dependency.
+That is, clone a local copy of a Git dependency at a specific revision
+or resolve a local path dependency.
+-/
+
 namespace Lake
 
 /-- Update the Git package in `repo` to `rev` if not already at it. -/
-def updateGitPkg (repo : GitRepo) (rev? : Option String) : LogIO PUnit := do
+def updateGitPkg (repo : GitRepo) (rev? : Option String) (name : String) : LogIO PUnit := do
   let rev ← repo.findRemoteRevision rev?
-  if (← repo.headRevision) == rev then return
-  logInfo s!"updating {repo} to revision {rev}"
-  repo.checkoutDetach rev
+  if (← repo.getHeadRevision) = rev then
+    if (← repo.hasDiff) then
+      logWarning s!"{name}: repository '{repo.dir}' has local changes"
+  else
+    logInfo s!"{name}: updating repository '{repo.dir}' to revision '{rev}'"
+    repo.checkoutDetach rev
 
 /-- Clone the Git package as `repo`. -/
 def cloneGitPkg (repo : GitRepo) (url : String) (rev? : Option String) : LogIO PUnit := do
@@ -27,21 +36,36 @@ def cloneGitPkg (repo : GitRepo) (url : String) (rev? : Option String) : LogIO P
     let hash ← repo.resolveRemoteRevision rev
     repo.checkoutDetach hash
 
+/--
+Update the Git repository from `url` in `repo` to `rev?`.
+If `repo` is already from `url`, just checkout the new revision.
+Otherwise, delete the local repository and clone a fresh copy from `url`.
+-/
 def updateGitRepo (repo : GitRepo) (url : String)
 (rev? : Option String) (name : String) : LogIO Unit := do
-  if (← repo.dirExists) then
-    if (← repo.getRemoteUrl?) = url then
-      updateGitPkg repo rev?
+  let sameUrl ← EIO.catchExceptions (h := fun _ => pure false) <| show IO Bool from do
+    let some remoteUrl ← repo.getRemoteUrl? | return false
+    return (← IO.FS.realPath remoteUrl) = (← IO.FS.realPath url)
+  if sameUrl then
+    updateGitPkg repo rev? name
+  else
+    if System.Platform.isWindows then
+      -- Deleting git repositories via IO.FS.removeDirAll does not work reliably on windows
+      logInfo s!"{name}: URL has changed; you might need to delete '{repo.dir}' manually"
+      updateGitPkg repo rev? name
     else
-      -- TODO: git resolves local file paths so we always hit this case for local repos
-      if System.Platform.isWindows then
-        -- Deleting git repositories via IO.FS.removeDirAll does not work reliably on windows
-        logInfo s!"{name}: URL has changed; you might need to delete {repo.dir} manually"
-        updateGitPkg repo rev?
-      else
-        logInfo s!"{name}: URL has changed; deleting {repo.dir} and cloning again"
-        IO.FS.removeDirAll repo.dir
-        cloneGitPkg repo url rev?
+      logInfo s!"{name}: URL has changed; deleting '{repo.dir}' and cloning again"
+      IO.FS.removeDirAll repo.dir
+      cloneGitPkg repo url rev?
+
+/--
+Materialize the Git repository from `url` into `repo` at `rev?`.
+Clone it if no local copy exists, otherwise update it.
+-/
+def materializeGitRepo (repo : GitRepo) (url : String)
+(rev? : Option String) (name : String) : LogIO Unit := do
+  if (← repo.dirExists) then
+    updateGitRepo repo url rev? name
   else
     cloneGitPkg repo url rev?
 
@@ -78,8 +102,8 @@ def Dependency.materialize (dep : Dependency) (inherited : Bool)
     let name := dep.name.toString (escape := false)
     let relGitDir := relPkgsDir / name
     let repo := GitRepo.mk (wsDir / relGitDir)
-    updateGitRepo repo url inputRev? name
-    let rev ← repo.headRevision
+    materializeGitRepo repo url inputRev? name
+    let rev ← repo.getHeadRevision
     let relPkgDir := match subDir? with | .some subDir => relGitDir / subDir | .none => relGitDir
     return {
       relPkgDir
@@ -110,12 +134,14 @@ def PackageEntry.materialize (wsDir relPkgsDir : FilePath) (manifestEntry : Pack
 
     [104]: https://github.com/leanprover/lake/issues/104
     -/
-    let updateNecessary ← id do
-      if (← repo.dirExists) then
-        return (← repo.headRevision?) != rev
-      return true
-    if updateNecessary then
-      updateGitRepo repo url rev name
+    if (← repo.dirExists) then
+      if (← repo.getHeadRevision?) = rev then
+        if (← repo.hasDiff) then
+          logWarning s!"{name}: repository '{repo.dir}' has local changes"
+      else
+        updateGitRepo repo url rev name
+    else
+      cloneGitPkg repo url rev
     let relPkgDir := match subDir? with | .some subDir => relGitDir / subDir | .none => relGitDir
     return {
       relPkgDir

src/lake/Lake/Util/Git.lean

@@ -11,10 +11,10 @@ namespace Lake
 
 namespace Git
 
-def defaultRemote :=
+@[noinline] def defaultRemote :=
   "origin"
 
-def upstreamBranch :=
+@[noinline] def upstreamBranch :=
   "master"
 
 /--
@@ -42,7 +42,7 @@ instance : ToString GitRepo := ⟨(·.dir.toString)⟩
 
 namespace GitRepo
 
-def cwd : GitRepo := ⟨"."⟩
+@[noinline] def cwd : GitRepo := ⟨"."⟩
 
 @[inline] def dirExists (repo : GitRepo) : BaseIO Bool :=
   repo.dir.isDir
@@ -80,10 +80,10 @@ def cwd : GitRepo := ⟨"."⟩
 @[inline] def resolveRevision (rev : String) (repo : GitRepo) : LogIO String := do
   repo.captureGit #["rev-parse", "--verify", rev]
 
-@[inline] def headRevision (repo : GitRepo) : LogIO String :=
+@[inline] def getHeadRevision (repo : GitRepo) : LogIO String :=
   repo.resolveRevision "HEAD"
 
-@[inline] def headRevision? (repo : GitRepo) : BaseIO (Option String) :=
+@[inline] def getHeadRevision? (repo : GitRepo) : BaseIO (Option String) :=
   repo.resolveRevision? "HEAD"
 
 def resolveRemoteRevision (rev : String) (remote := Git.defaultRemote) (repo : GitRepo) : LogIO String := do
@@ -109,3 +109,9 @@ def findRemoteRevision (repo : GitRepo) (rev? : Option String := none) (remote :
 
 def getFilteredRemoteUrl? (remote := Git.defaultRemote) (repo : GitRepo) : BaseIO (Option String) := OptionT.run do
   Git.filterUrl? (← repo.getRemoteUrl? remote)
+
+@[inline] def hasNoDiff (repo : GitRepo) : BaseIO Bool := do
+  repo.testGit #["diff", "--exit-code"]
+
+@[inline] def hasDiff (repo : GitRepo) : BaseIO Bool := do
+  not <$> repo.hasNoDiff

src/lake/test/clone/test.sh

@@ -28,6 +28,12 @@ test -d lake-packages/hello
 $LAKE build
 ./build/bin/test
 
+# test leanprover/lake#167
+sed_i "s/Hello,/Goodbye,/" lake-packages/hello/Main.lean
+! git -C lake-packages/hello diff --exit-code
+$LAKE build 2>&1 | grep -m1 "has local changes"
+./build/bin/test
+
 # test leanprover/lake#104
 TEST_URL=https://example.com/hello.git
 MANIFEST=lake-manifest.json