Skip to content
This repository has been archived by the owner on Oct 25, 2023. It is now read-only.

fix: do not call git checkout unless necessary #64

Merged
merged 2 commits into from
May 15, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion Lake/Config/Resolve.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 5 additions & 1 deletion Lake/Util/Git.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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}")

Expand Down