From 56211eda682edee5114818b0fba75a0a875140d8 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Sat, 14 May 2022 15:34:00 +0200
Subject: [PATCH 1/2] perf: do not resolve full git object names

---
 Lake/Util/Git.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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}")
 

From 36eeaaa7356ca7392297f76fcb0588261d46027d Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Sat, 14 May 2022 15:42:37 +0200
Subject: [PATCH 2/2] fix: do not call git checkout unless necessary

See #63.
---
 Lake/Config/Resolve.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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