From decf7a042a84bebf50a73cd32b17df01263c8d8f Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Mon, 25 Sep 2023 16:02:20 -0400
Subject: [PATCH] perf: lake: lazily acquire repo URL/tag in `:release`

---
 src/lake/Lake/Build/Package.lean    | 12 ++++++++++--
 src/lake/Lake/Config/Package.lean   | 11 -----------
 src/lake/Lake/Load/Main.lean        |  4 ----
 src/lake/Lake/Load/Materialize.lean |  5 -----
 4 files changed, 10 insertions(+), 22 deletions(-)

diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean
index dec6f6b3d1..dccbc6b006 100644
--- a/src/lake/Lake/Build/Package.lean
+++ b/src/lake/Lake/Build/Package.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lake.Util.Git
 import Lake.Util.Sugar
 import Lake.Build.Common
 import Lake.Build.Targets
@@ -46,8 +47,15 @@ def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
 
 /-- Download and unpack the package's prebuilt release archive (from GitHub). -/
 def Package.fetchRelease (self : Package) : SchedulerM (BuildJob Unit) := Job.async do
-  let some (repoUrl, tag) := self.release? | do
-    logWarning "wanted prebuilt release, but release repository and tag was not known"
+  let repo := GitRepo.mk self.dir
+  let repoUrl? := self.releaseRepo? <|> self.remoteUrl?
+  let some repoUrl := repoUrl? <|> (← repo.getFilteredRemoteUrl?) | do
+    logWarning <| s!"{self.name}: wanted prebuilt release, " ++
+      "but package's repository URL was not known; it may need to set `releaseRepo?`"
+    return ((), .nil)
+  let some tag ← repo.findTag? | do
+    logWarning <| s!"{self.name}: wanted prebuilt release, " ++
+      "but could not find an associated tag for the package's revision"
     return ((), .nil)
   let url := s!"{repoUrl}/releases/download/{tag}/{self.buildArchive}"
   let logName := s!"{self.name}/{tag}/{self.buildArchive}"
diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean
index a71c255c9d..a387bba7f2 100644
--- a/src/lake/Lake/Config/Package.lean
+++ b/src/lake/Lake/Config/Package.lean
@@ -183,8 +183,6 @@ structure Package where
   leanOpts : Options
   /-- The URL to this package's Git remote. -/
   remoteUrl? : Option String := none
-  /-- The Git tag of this package. -/
-  gitTag? : Option String := none
   /-- (Opaque references to) the package's direct dependencies. -/
   opaqueDeps : Array OpaquePackage := #[]
   /-- Lean library configurations for the package. -/
@@ -269,15 +267,6 @@ namespace Package
 @[inline] def releaseRepo? (self : Package) : Option String :=
   self.config.releaseRepo?
 
-/--
-The package's URL × tag release.
-Tries `releaseRepo?` first and then falls back to `remoteUrl?`.
--/
-def release? (self : Package) : Option (String × String) := do
-  let url ← self.releaseRepo? <|> self.remoteUrl?
-  let tag ← self.gitTag?
-  return (url, tag)
-
 /-- The package's `buildArchive?` configuration. -/
 @[inline] def buildArchive? (self : Package) : Option String :=
   self.config.buildArchive?
diff --git a/src/lake/Lake/Load/Main.lean b/src/lake/Lake/Load/Main.lean
index 65166d6454..ee34a8f363 100644
--- a/src/lake/Lake/Load/Main.lean
+++ b/src/lake/Lake/Load/Main.lean
@@ -38,7 +38,6 @@ def loadDepPackage (wsDir : FilePath) (dep : MaterializedDep)
   return {
     dir, config, configEnv, leanOpts
     remoteUrl? := dep.remoteUrl?
-    gitTag? := dep.gitTag?
   }
 
 /--
@@ -103,12 +102,9 @@ def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
   let configEnv ← importConfigFile config.rootDir config.rootDir
     config.configOpts config.leanOpts config.configFile config.reconfigure
   let pkgConfig ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv config.leanOpts
-  let repo := GitRepo.mk config.rootDir
   let root := {
     configEnv, leanOpts := config.leanOpts
     dir := config.rootDir, config := pkgConfig
-    remoteUrl? := ← repo.getFilteredRemoteUrl?
-    gitTag? := ← repo.findTag?
   }
   return {
     root, lakeEnv := config.env
diff --git a/src/lake/Lake/Load/Materialize.lean b/src/lake/Lake/Load/Materialize.lean
index c01aae4a70..76058b8034 100644
--- a/src/lake/Lake/Load/Materialize.lean
+++ b/src/lake/Lake/Load/Materialize.lean
@@ -74,7 +74,6 @@ structure MaterializedDep where
   /-- Path to the materialized package relative to the workspace's root directory. -/
   relPkgDir : FilePath
   remoteUrl? : Option String
-  gitTag? : Option String
   manifestEntry : PackageEntry
   deriving Inhabited
 
@@ -96,7 +95,6 @@ def Dependency.materialize (dep : Dependency) (inherited : Bool)
     return {
       relPkgDir
       remoteUrl? := none
-      gitTag? := ← (GitRepo.mk <| wsDir / relPkgDir).findTag?
       manifestEntry := .path dep.name dep.opts inherited relPkgDir
     }
   | .git url inputRev? subDir? => do
@@ -109,7 +107,6 @@ def Dependency.materialize (dep : Dependency) (inherited : Bool)
     return {
       relPkgDir
       remoteUrl? := Git.filterUrl? url
-      gitTag? := ← repo.findTag?
       manifestEntry := .git dep.name dep.opts inherited url rev inputRev? subDir?
     }
 
@@ -121,7 +118,6 @@ def PackageEntry.materialize (wsDir relPkgsDir : FilePath) (manifestEntry : Pack
     return {
       relPkgDir
       remoteUrl? := none
-      gitTag? := ← (GitRepo.mk <| wsDir / relPkgDir).findTag?
       manifestEntry
     }
   | .git name _opts _inherited url rev _inputRev? subDir? => do
@@ -147,6 +143,5 @@ def PackageEntry.materialize (wsDir relPkgsDir : FilePath) (manifestEntry : Pack
     return {
       relPkgDir
       remoteUrl? := Git.filterUrl? url
-      gitTag? := ← repo.findTag?
       manifestEntry
     }