diff --git a/Lake/Config/Resolve.lean b/Lake/Config/Resolve.lean index c3e12c2..4aac201 100644 --- a/Lake/Config/Resolve.lean +++ b/Lake/Config/Resolve.lean @@ -21,8 +21,9 @@ cloning and/or updating it as necessary. def materializeGit (name : String) (dir : FilePath) (url rev : String) : (LogT IO) PUnit := do if ← dir.isDir then - logInfo s!"{name}: trying to update {dir} to revision {rev}" let hash ← parseOriginRevision rev dir + if (← headRevision dir) == hash then return + logInfo s!"{name}: trying to update {dir} to revision {rev}" unless ← revisionExists hash dir do fetch dir checkoutDetach hash dir else diff --git a/Lake/Util/Git.lean b/Lake/Util/Git.lean index f1f236c..bb2ad8a 100644 --- a/Lake/Util/Git.lean +++ b/Lake/Util/Git.lean @@ -10,6 +10,9 @@ namespace Lake.Git def upstreamBranch := "master" +def isFullObjectName (rev : String) : Bool := + rev.length == 40 && rev.all fun c => c.isDigit || ('a' <= c && c <= 'f') + def defaultRevision : Option String → String | none => upstreamBranch | some branch => branch @@ -51,7 +54,8 @@ def parseRevision (rev : String) (repo : Option FilePath := none) : IO String := def headRevision (repo : Option FilePath := none) : IO String := parseRevision "HEAD" repo -def parseOriginRevision (rev : String) (repo : Option FilePath := none) : IO String := +def parseOriginRevision (rev : String) (repo : Option FilePath := none) : IO String := do + if isFullObjectName rev then return rev (parseRevision ("origin/" ++ rev) repo) <|> parseRevision rev repo <|> throw (IO.userError s!"cannot find revision {rev} in repository {repo}")