diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index c2c42ba959..ad03940333 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/src/lake/Lake/CLI/Main.lean @@ -69,7 +69,7 @@ public structure LakeOptions where scope? : Option CacheServiceScope := none platform? : Option CachePlatform := none toolchain? : Option CacheToolchain := none - rev? : Option String := none + rev? : Option GitRev := none maxRevs : Nat := 100 shake : Shake.Args := {} @@ -563,7 +563,7 @@ private def computePackageRev (pkgDir : FilePath) : CliStateM String := do repo.getHeadRevision private def putCore - (rev : String) (outputs : FilePath) (artDir : FilePath) + (rev : GitRev) (outputs : FilePath) (artDir : FilePath) (service : CacheService) (scope : CacheServiceScope) (platform := CachePlatform.none) (toolchain := CacheToolchain.none) : LoggerIO Unit := do diff --git a/src/lake/Lake/Config/Cache.lean b/src/lake/Lake/Config/Cache.lean index ce28e056c6..208bca7d47 100644 --- a/src/lake/Lake/Config/Cache.lean +++ b/src/lake/Lake/Config/Cache.lean @@ -7,6 +7,7 @@ module prelude import Init.Control.Do +public import Lake.Util.Git public import Lake.Util.Log public import Lake.Util.Version public import Lake.Config.Artifact @@ -469,7 +470,7 @@ public def readOutputs? (cache : Cache) (scope : String) (inputHash : Hash) : Lo cache.dir / "revisions" /-- Returns path to the input-to-output mappings of a downloaded package revision. -/ -@[inline] public def revisionPath (cache : Cache) (scope : String) (rev : String) : FilePath := +@[inline] public def revisionPath (cache : Cache) (scope : String) (rev : GitRev) : FilePath := cache.revisionDir / scope / s!"{rev}.jsonl" end Cache @@ -942,7 +943,7 @@ public def uploadArtifacts public def mapContentType : String := "application/vnd.reservoir.outputs+json-lines" def s3RevisionUrl - (rev : String) (service : CacheService) (scope : CacheServiceScope) + (rev : GitRev) (service : CacheService) (scope : CacheServiceScope) (platform := CachePlatform.none) (toolchain := CacheToolchain.none) : String := match scope.impl with @@ -956,7 +957,7 @@ def s3RevisionUrl return s!"{url}/{rev}.jsonl" public def revisionUrl - (rev : String) (service : CacheService) (scope : CacheServiceScope) + (rev : GitRev) (service : CacheService) (scope : CacheServiceScope) (platform := CachePlatform.none) (toolchain := CacheToolchain.none) : String := if service.isReservoir then Id.run do @@ -974,7 +975,7 @@ public def revisionUrl service.s3RevisionUrl rev scope platform toolchain public def downloadRevisionOutputs? - (rev : String) (cache : Cache) (service : CacheService) + (rev : GitRev) (cache : Cache) (service : CacheService) (localScope : String) (remoteScope : CacheServiceScope) (platform := CachePlatform.none) (toolchain := CacheToolchain.none) (force := false) : LoggerIO (Option CacheMap) := do @@ -998,7 +999,7 @@ public def downloadRevisionOutputs? CacheMap.load path platform.isNone public def uploadRevisionOutputs - (rev : String) (outputs : FilePath) (service : CacheService) (scope : CacheServiceScope) + (rev : GitRev) (outputs : FilePath) (service : CacheService) (scope : CacheServiceScope) (platform := CachePlatform.none) (toolchain := CacheToolchain.none) : LoggerIO Unit := do let url := service.s3RevisionUrl rev scope platform toolchain diff --git a/src/lake/Lake/Config/Dependency.lean b/src/lake/Lake/Config/Dependency.lean index a06fad9cd1..c411e9e483 100644 --- a/src/lake/Lake/Config/Dependency.lean +++ b/src/lake/Lake/Config/Dependency.lean @@ -9,6 +9,7 @@ prelude public import Init.Dynamic public import Init.System.FilePath public import Lean.Data.NameMap.Basic +public import Lake.Util.Git import Init.Data.ToString.Name import Init.Data.ToString.Macro @@ -30,7 +31,7 @@ public inductive DependencySrc where /- A package located at a fixed path relative to the dependent package's directory. -/ | path (dir : FilePath) /- A package cloned from a Git repository available at a fixed Git `url`. -/ -| git (url : String) (rev : Option String) (subDir : Option FilePath) +| git (url : String) (rev : Option GitRev) (subDir : Option FilePath) deriving Inhabited, Repr /-- diff --git a/src/lake/Lake/Load/Manifest.lean b/src/lake/Lake/Load/Manifest.lean index d22fa63345..dd26d7f988 100644 --- a/src/lake/Lake/Load/Manifest.lean +++ b/src/lake/Lake/Load/Manifest.lean @@ -8,6 +8,7 @@ module prelude public import Lake.Util.Version public import Lake.Config.Defaults +public import Lake.Util.Git import Lake.Util.Error public import Lake.Util.FilePath import Lake.Util.JsonObject @@ -75,8 +76,8 @@ public inductive PackageEntrySrc /-- A remote Git package. -/ | git (url : String) - (rev : String) - (inputRev? : Option String) + (rev : GitRev) + (inputRev? : Option GitRev) (subDir? : Option FilePath) deriving Inhabited diff --git a/src/lake/Lake/Load/Materialize.lean b/src/lake/Lake/Load/Materialize.lean index e5490bf5ee..62799afae1 100644 --- a/src/lake/Lake/Load/Materialize.lean +++ b/src/lake/Lake/Load/Materialize.lean @@ -13,6 +13,8 @@ import Lake.Util.Git import Lake.Util.IO import Lake.Reservoir +set_option doc.verso true + open System Lean /-! # Dependency Materialization @@ -23,9 +25,12 @@ or resolve a local path dependency. namespace Lake -/-- Update the Git package in `repo` to `rev` if not already at it. -/ +/-- +Update the Git package in {lean}`repo` to the revision {lean}`rev?` if not already at it. +IF no revision is specified (i.e., {lean}`rev? = none`), then uses the latest {lit}`master`. +-/ def updateGitPkg - (name : String) (repo : GitRepo) (rev? : Option String) + (name : String) (repo : GitRepo) (rev? : Option GitRev) : LoggerIO PUnit := do let rev ← repo.findRemoteRevision rev? if (← repo.getHeadRevision) = rev then @@ -40,9 +45,9 @@ def updateGitPkg -- so stale ones from the previous revision cause incorrect trace computations. repo.clean -/-- Clone the Git package as `repo`. -/ +/-- Clone the Git package as {lean}`repo`. -/ def cloneGitPkg - (name : String) (repo : GitRepo) (url : String) (rev? : Option String) + (name : String) (repo : GitRepo) (url : String) (rev? : Option GitRev) : LoggerIO PUnit := do logInfo s!"{name}: cloning {url}" repo.clone url @@ -52,9 +57,9 @@ def cloneGitPkg repo.checkoutDetach rev /-- -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`. +Update the Git repository from {lean}`url` in {lean}`repo` to {lean}`rev?`. +If {lean}`repo` is already from {lean}`url`, just checkout the new revision. +Otherwise, delete the local repository and clone a fresh copy from {lean}`url`. -/ def updateGitRepo (name : String) (repo : GitRepo) (url : String) (rev? : Option String) @@ -75,8 +80,9 @@ def updateGitRepo IO.FS.removeDirAll repo.dir cloneGitPkg name repo url rev? + /-- -Materialize the Git repository from `url` into `repo` at `rev?`. +Materialize the Git repository from {lean}`url` into {lean}`repo` at {lean}`rev?`. Clone it if no local copy exists, otherwise update it. -/ def materializeGitRepo @@ -114,11 +120,11 @@ namespace MaterializedDep @[inline] public def scope (self : MaterializedDep) : String := self.manifestEntry.scope -/-- Path to the dependency's manfiest file (relative to `relPkgDir`). -/ +/-- Path to the dependency's manfiest file (relative to {lean}`relPkgDir`). -/ @[inline] public def relManifestFile? (self : MaterializedDep) : Option FilePath := self.manifestEntry.manifestFile? -/-- Path to the dependency's manfiest file (relative to `relPkgDir`). -/ +/-- Path to the dependency's manfiest file (relative to {lean}`relPkgDir`). -/ @[inline] public def relManifestFile (self : MaterializedDep) : FilePath := self.relManifestFile?.getD defaultManifestFile @@ -126,7 +132,7 @@ namespace MaterializedDep @[inline] public def manifestFile (self : MaterializedDep) : FilePath := self.pkgDir / self.relManifestFile -/-- Path to the dependency's configuration file (relative to `relPkgDir`). -/ +/-- Path to the dependency's configuration file (relative to {lean}`relPkgDir`). -/ @[inline] public def relConfigFile (self : MaterializedDep) : FilePath := self.manifestEntry.configFile @@ -143,7 +149,7 @@ end MaterializedDep inductive InputVer | none -| git (rev : String) +| git (rev : GitRev) | ver (ver : VerRange) def pkgNotIndexed (scope name : String) (ver : InputVer) : String := diff --git a/src/lake/Lake/Util/Git.lean b/src/lake/Lake/Util/Git.lean index e60d7e2792..fda74794c3 100644 --- a/src/lake/Lake/Util/Git.lean +++ b/src/lake/Lake/Util/Git.lean @@ -10,6 +10,7 @@ public import Init.Data.ToString public import Lake.Util.Proc import Init.Data.String.TakeDrop import Init.Data.String.Search +import Lake.Util.String open System namespace Lake @@ -36,18 +37,48 @@ public def filterUrl? (url : String) : Option String := some url public def isFullObjectName (rev : String) : Bool := - rev.length == 40 && rev.all fun c => c.isDigit || ('a' <= c && c <= 'f') + rev.utf8ByteSize == 40 && isHex rev end Git public structure GitRepo where dir : FilePath -public instance : Coe FilePath GitRepo := ⟨(⟨·⟩)⟩ -public instance : ToString GitRepo := ⟨(·.dir.toString)⟩ + +/-- +A commit-ish [Git revision][1]. + +This can be SHA1 commit hash, a branch name, or one of Git's more complex specifiers. + +[1]: https://git-scm.com/docs/gitrevisions#_specifying_revisions +-/ +public abbrev GitRev := String + +namespace GitRev + +/-- The head revision (i.e., `HEAD`). -/ +@[expose] public def head : GitRev := "HEAD" + +/-- The revision fetched during the last `git fetch` (i.e., `FETCH_HEAD`). -/ +@[expose] public def fetchHead : GitRev := "FETCH_HEAD" + +/-- Returns whether this revision is a 40-digit hexadecimal (SHA1) commit hash. -/ +public def isFullSha1 (rev : GitRev) : Bool := + rev.utf8ByteSize == 40 && isHex rev + +attribute [deprecated GitRev.isFullSha1 (since := "2026-04-17")] Git.isFullObjectName + +/-- Scopes the revision by the remote. -/ +@[inline] public def withRemote (remote : String) (rev : GitRev) : GitRev := + s!"{remote}/{rev}" + +end GitRev namespace GitRepo +public instance : Coe FilePath GitRepo := ⟨(⟨·⟩)⟩ +public instance : ToString GitRepo := ⟨(·.dir.toString)⟩ + public def cwd : GitRepo := ⟨"."⟩ @[inline] public def dirExists (repo : GitRepo) : BaseIO Bool := @@ -71,12 +102,18 @@ public def clone (url : String) (repo : GitRepo) : LogIO PUnit := public def quietInit (repo : GitRepo) : LogIO PUnit := repo.execGit #["init", "-q"] +public def bareInit (repo : GitRepo) : LogIO PUnit := + repo.execGit #["init", "--bare", "-q"] + public def insideWorkTree (repo : GitRepo) : BaseIO Bool := do repo.testGit #["rev-parse", "--is-inside-work-tree"] public def fetch (repo : GitRepo) (remote := Git.defaultRemote) : LogIO PUnit := repo.execGit #["fetch", "--tags", "--force", remote] +public def addWorktreeDetach (path : FilePath) (rev : GitRev) (repo : GitRepo) : LogIO PUnit := + repo.execGit #["worktree", "add", "--detach", path.toString, rev] + public def checkoutBranch (branch : String) (repo : GitRepo) : LogIO PUnit := repo.execGit #["checkout", "-B", branch] @@ -87,60 +124,80 @@ public def checkoutDetach (hash : String) (repo : GitRepo) : LogIO PUnit := public def clean (repo : GitRepo) : LogIO PUnit := repo.execGit #["clean", "-xf"] -public def resolveRevision? (rev : String) (repo : GitRepo) : BaseIO (Option String) := do +/-- Resolves the revision to a Git object name (SHA1 hash) which or may not exist in the repository. -/ +public def resolveRevision? (rev : GitRev) (repo : GitRepo) : BaseIO (Option GitRev) := do repo.captureGit? #["rev-parse", "--verify", "--end-of-options", rev] -public def resolveRevision (rev : String) (repo : GitRepo) : LogIO String := do - if Git.isFullObjectName rev then return rev +/-- Resolves the revision to a valid commit hash within the repository. -/ +public def findCommit? (rev : GitRev) (repo : GitRepo) : BaseIO (Option GitRev) := do + repo.captureGit? #["rev-parse", "--verify", "--end-of-options", rev ++ "^{commit}"] + +public def resolveRevision (rev : GitRev) (repo : GitRepo) : LogIO GitRev := do + if rev.isFullSha1 then return rev if let some rev ← repo.resolveRevision? rev then return rev error s!"{repo}: revision not found '{rev}'" -@[inline] public def getHeadRevision? (repo : GitRepo) : BaseIO (Option String) := - repo.resolveRevision? "HEAD" +@[inline] public def getHeadRevision? (repo : GitRepo) : BaseIO (Option GitRev) := + repo.resolveRevision? .head -public def getHeadRevision (repo : GitRepo) : LogIO String := do +public def getHeadRevision (repo : GitRepo) : LogIO GitRev := do if let some rev ← repo.getHeadRevision? then return rev error s!"{repo}: could not resolve 'HEAD' to a commit; \ the repository may be corrupt, so you may need to remove it and try again" -public def getHeadRevisions (repo : GitRepo) (n : Nat := 0) : LogIO (Array String) := do +public def fetchRevision? (repo : GitRepo) (remote : String) (rev : GitRev) : LogIO (Option GitRev) := do + if (← repo.testGit #["fetch", "--tags", "--force", "--refetch", "--filter=tree:0", remote, rev]) then + let some rev ← repo.resolveRevision? .fetchHead + | error s!"{repo}: could not resolve 'FETCH_HEAD' to a commit after fetching; \ + this may be an issue with Lake; please report it" + return rev + else + return none + +public def getHeadRevisions (repo : GitRepo) (n : Nat := 0) : LogIO (Array GitRev) := do let args := #["rev-list", "HEAD"] let args := if n != 0 then args ++ #["-n", toString n] else args let revs ← repo.captureGit args return revs.split '\n' |>.toStringArray -public def resolveRemoteRevision (rev : String) (remote := Git.defaultRemote) (repo : GitRepo) : LogIO String := do - if Git.isFullObjectName rev then return rev - if let some rev ← repo.resolveRevision? s!"{remote}/{rev}" then return rev +public def resolveRemoteRevision (rev : GitRev) (remote := Git.defaultRemote) (repo : GitRepo) : LogIO GitRev := do + if rev.isFullSha1 then return rev + if let some rev ← repo.resolveRevision? (rev.withRemote remote) then return rev if let some rev ← repo.resolveRevision? rev then return rev error s!"{repo}: revision not found '{rev}'" -public def findRemoteRevision (repo : GitRepo) (rev? : Option String := none) (remote := Git.defaultRemote) : LogIO String := do +public def findRemoteRevision (repo : GitRepo) (rev? : Option GitRev := none) (remote := Git.defaultRemote) : LogIO String := do repo.fetch remote; repo.resolveRemoteRevision (rev?.getD Git.upstreamBranch) remote -public def branchExists (rev : String) (repo : GitRepo) : BaseIO Bool := do +public def branchExists (rev : GitRev) (repo : GitRepo) : BaseIO Bool := do repo.testGit #["show-ref", "--verify", s!"refs/heads/{rev}"] -public def revisionExists (rev : String) (repo : GitRepo) : BaseIO Bool := do +public def revisionExists (rev : GitRev) (repo : GitRepo) : BaseIO Bool := do repo.testGit #["rev-parse", "--verify", rev ++ "^{commit}"] public def getTags (repo : GitRepo) : BaseIO (List String) := do let some out ← repo.captureGit? #["tag"] | return [] return out.split '\n' |>.toStringList -public def findTag? (rev : String := "HEAD") (repo : GitRepo) : BaseIO (Option String) := do +public def findTag? (rev : GitRev := .head) (repo : GitRepo) : BaseIO (Option String) := do repo.captureGit? #["describe", "--tags", "--exact-match", rev] public def getRemoteUrl? (remote := Git.defaultRemote) (repo : GitRepo) -: BaseIO (Option String) := do repo.captureGit? #["remote", "get-url", remote] +: BaseIO (Option String) := repo.captureGit? #["remote", "get-url", remote] + +public def addRemote (remote : String) (url : String) (repo : GitRepo) : LogIO Unit := + repo.execGit #["remote", "add", remote, url] + +public def setRemoteUrl (remote : String) (url : String) (repo : GitRepo) : LogIO Unit := + repo.execGit #["remote", "set-url", remote, url] public def getFilteredRemoteUrl? (remote := Git.defaultRemote) (repo : GitRepo) : BaseIO (Option String) := OptionT.run do Git.filterUrl? (← repo.getRemoteUrl? remote) public def hasNoDiff (repo : GitRepo) : BaseIO Bool := do - repo.testGit #["diff", "HEAD", "--exit-code"] + repo.testGit #["diff", "--exit-code", "HEAD"] @[inline] public def hasDiff (repo : GitRepo) : BaseIO Bool := do not <$> repo.hasNoDiff