From 3ad841e665025ec0ca2af69da5f04e195898bdd2 Mon Sep 17 00:00:00 2001 From: tydeu Date: Tue, 15 Aug 2023 19:21:36 -0400 Subject: [PATCH] feat: warn on local changes to dependency & related fixes --- src/lake/Lake/Load/Main.lean | 2 +- src/lake/Lake/Load/Materialize.lean | 74 +++++++++++++++++++---------- src/lake/Lake/Util/Git.lean | 16 +++++-- src/lake/test/clone/test.sh | 6 +++ 4 files changed, 68 insertions(+), 30 deletions(-) diff --git a/src/lake/Lake/Load/Main.lean b/src/lake/Lake/Load/Main.lean index 357ebbfb09b8..4b84884f5826 100644 --- a/src/lake/Lake/Load/Main.lean +++ b/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 () diff --git a/src/lake/Lake/Load/Materialize.lean b/src/lake/Lake/Load/Materialize.lean index 65bc38cd6c13..ed207066b104 100644 --- a/src/lake/Lake/Load/Materialize.lean +++ b/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 diff --git a/src/lake/Lake/Util/Git.lean b/src/lake/Lake/Util/Git.lean index c70be972b028..3f36e0a1c413 100644 --- a/src/lake/Lake/Util/Git.lean +++ b/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 diff --git a/src/lake/test/clone/test.sh b/src/lake/test/clone/test.sh index cc11b160517b..821da192fd74 100755 --- a/src/lake/test/clone/test.sh +++ b/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