def Lake.Git.defaultRemote : String

def Lake.Git.upstreamBranch : String

def Lake.Git.filterUrl? (url : String) : Option String

Try to turn a remote URL into a URL that can be used to, e.g., make GitHub API requests. That is, do not accept SSH URLs and drop an ending .git.

@[deprecated Lake.GitRev.isFullSha1 (since := "2026-04-17")]

def Lake.Git.isFullObjectName (rev : String) : Bool

structure Lake.GitRepo : Type

• dir : System.FilePath

@[reducible, inline]

abbrev Lake.GitRev : Type

A commit-ish Git revision.

This can be SHA1 commit hash, a branch name, or one of Git's more complex specifiers.

def Lake.GitRev.head : GitRev

The head revision (i.e., HEAD).

def Lake.GitRev.fetchHead : GitRev

The revision fetched during the last git fetch (i.e., FETCH_HEAD).

def Lake.GitRev.isFullSha1 (rev : GitRev) : Bool

Returns whether this revision is a 40-digit hexadecimal (SHA1) commit hash.

@[inline]

def Lake.GitRev.withRemote (remote : String) (rev : GitRev) : GitRev

Scopes the revision by the remote.

@[implicit_reducible]

instance Lake.GitRepo.instCoeFilePath : Coe System.FilePath GitRepo

@[implicit_reducible]

instance Lake.GitRepo.instToString : ToString GitRepo

def Lake.GitRepo.cwd : GitRepo

@[inline]

def Lake.GitRepo.dirExists (repo : GitRepo) : BaseIO Bool

@[inline]

def Lake.GitRepo.captureGit (args : Array String) (repo : GitRepo) : LogIO String

@[inline]

def Lake.GitRepo.captureGit? (args : Array String) (repo : GitRepo) : BaseIO (Option String)

@[inline]

def Lake.GitRepo.execGit (args : Array String) (repo : GitRepo) : LogIO PUnit

@[inline]

def Lake.GitRepo.testGit (args : Array String) (repo : GitRepo) : BaseIO Bool

def Lake.GitRepo.clone (url : String) (repo : GitRepo) : LogIO PUnit

def Lake.GitRepo.quietInit (repo : GitRepo) : LogIO PUnit

def Lake.GitRepo.bareInit (repo : GitRepo) : LogIO PUnit

def Lake.GitRepo.insideWorkTree (repo : GitRepo) : BaseIO Bool

def Lake.GitRepo.fetch (repo : GitRepo) (remote : String := Git.defaultRemote) : LogIO PUnit

def Lake.GitRepo.addWorktreeDetach (path : System.FilePath) (rev : GitRev) (repo : GitRepo) : LogIO PUnit

def Lake.GitRepo.checkoutBranch (branch : String) (repo : GitRepo) : LogIO PUnit

def Lake.GitRepo.checkoutDetach (hash : String) (repo : GitRepo) : LogIO PUnit

def Lake.GitRepo.clean (repo : GitRepo) : LogIO PUnit

Remove untracked files from tracked folders in the repository.

def Lake.GitRepo.resolveRevision? (rev : GitRev) (repo : GitRepo) : BaseIO (Option GitRev)

Resolves the revision to a Git object name (SHA1 hash) which or may not exist in the repository.

def Lake.GitRepo.findCommit? (rev : GitRev) (repo : GitRepo) : BaseIO (Option GitRev)

Resolves the revision to a valid commit hash within the repository.

def Lake.GitRepo.resolveRevision (rev : GitRev) (repo : GitRepo) : LogIO GitRev

@[inline]

def Lake.GitRepo.getHeadRevision? (repo : GitRepo) : BaseIO (Option GitRev)

def Lake.GitRepo.getHeadRevision (repo : GitRepo) : LogIO GitRev

def Lake.GitRepo.fetchRevision? (repo : GitRepo) (remote : String) (rev : GitRev) : LogIO (Option GitRev)

def Lake.GitRepo.getHeadRevisions (repo : GitRepo) (n : Nat := 0) : LogIO (Array GitRev)

def Lake.GitRepo.resolveRemoteRevision (rev : GitRev) (remote : String := Git.defaultRemote) (repo : GitRepo) : LogIO GitRev

def Lake.GitRepo.findRemoteRevision (repo : GitRepo) (rev? : Option GitRev := none) (remote : String := Git.defaultRemote) : LogIO String

def Lake.GitRepo.branchExists (rev : GitRev) (repo : GitRepo) : BaseIO Bool

def Lake.GitRepo.revisionExists (rev : GitRev) (repo : GitRepo) : BaseIO Bool

def Lake.GitRepo.getTags (repo : GitRepo) : BaseIO (List String)

def Lake.GitRepo.findTag? (rev : GitRev := GitRev.head) (repo : GitRepo) : BaseIO (Option String)

def Lake.GitRepo.getRemoteUrl? (remote : String := Git.defaultRemote) (repo : GitRepo) : BaseIO (Option String)

def Lake.GitRepo.addRemote (remote url : String) (repo : GitRepo) : LogIO Unit

def Lake.GitRepo.setRemoteUrl (remote url : String) (repo : GitRepo) : LogIO Unit

def Lake.GitRepo.getFilteredRemoteUrl? (remote : String := Git.defaultRemote) (repo : GitRepo) : BaseIO (Option String)

def Lake.GitRepo.hasNoDiff (repo : GitRepo) : BaseIO Bool

@[inline]

def Lake.GitRepo.hasDiff (repo : GitRepo) : BaseIO Bool