def Lake.Git.defaultRemote : String

Equations

• Lake.Git.defaultRemote = "origin"

def Lake.Git.upstreamBranch : String

Equations

• Lake.Git.upstreamBranch = "master"

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.

Equations

• Lake.Git.filterUrl? url = if url.startsWith "git" = true then none else if url.endsWith ".git" = true then some (url.dropEnd 4).copy else some url

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

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

Equations

• Lake.Git.isFullObjectName rev = (rev.utf8ByteSize == 40 && Lake.isHex rev)

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.

Equations

• Lake.GitRev = String

def Lake.GitRev.head : GitRev

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

Equations

• Lake.GitRev.head = "HEAD"

def Lake.GitRev.fetchHead : GitRev

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

Equations

• Lake.GitRev.fetchHead = "FETCH_HEAD"

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

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

Equations

• rev.isFullSha1 = (String.utf8ByteSize rev == 40 && Lake.isHex rev)

@[inline]

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

Scopes the revision by the remote.

Equations

• Lake.GitRev.withRemote remote rev = toString remote ++ toString "/" ++ toString rev

@[implicit_reducible]

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

Equations

• Lake.GitRepo.instCoeFilePath = { coe := fun (x : System.FilePath) => { dir := x } }

@[implicit_reducible]

instance Lake.GitRepo.instToString : ToString GitRepo

Equations

• Lake.GitRepo.instToString = { toString := fun (x : Lake.GitRepo) => x.dir.toString }

def Lake.GitRepo.cwd : GitRepo

Equations

• Lake.GitRepo.cwd = { dir := { toString := "." } }

@[inline]

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

Equations

• repo.dirExists = repo.dir.isDir

@[inline]

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

Equations

• Lake.GitRepo.captureGit args repo = Lake.captureProc { cmd := "git", args := args, cwd := some repo.dir }

@[inline]

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

Equations

• Lake.GitRepo.captureGit? args repo = Lake.captureProc? { cmd := "git", args := args, cwd := some repo.dir }

@[inline]

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

Equations

• Lake.GitRepo.execGit args repo = Lake.proc { cmd := "git", args := args, cwd := some repo.dir } true

@[inline]

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

Equations

• Lake.GitRepo.testGit args repo = Lake.testProc { cmd := "git", args := args, cwd := some repo.dir }

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

Equations

• Lake.GitRepo.clone url repo = Lake.proc { cmd := "git", args := #["clone", url, repo.dir.toString] } true

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

Equations

• repo.quietInit = Lake.GitRepo.execGit #["init", "-q"] repo

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

Equations

• repo.bareInit = Lake.GitRepo.execGit #["init", "--bare", "-q"] repo

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

Equations

• repo.insideWorkTree = Lake.GitRepo.testGit #["rev-parse", "--is-inside-work-tree"] repo

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

Equations

• repo.fetch remote = Lake.GitRepo.execGit #["fetch", "--tags", "--force", remote] repo

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

Equations

• Lake.GitRepo.addWorktreeDetach path rev repo = Lake.GitRepo.execGit #["worktree", "add", "--detach", path.toString, rev] repo

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

Equations

• Lake.GitRepo.checkoutBranch branch repo = Lake.GitRepo.execGit #["checkout", "-B", branch] repo

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

Equations

• Lake.GitRepo.checkoutDetach hash repo = Lake.GitRepo.execGit #["checkout", "--detach", hash, "--"] repo

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

Remove untracked files from tracked folders in the repository.

Equations

• repo.clean = Lake.GitRepo.execGit #["clean", "-xf"] repo

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.

Equations

• Lake.GitRepo.resolveRevision? rev repo = Lake.GitRepo.captureGit? #["rev-parse", "--verify", "--end-of-options", rev] repo

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

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

Equations

• Lake.GitRepo.findCommit? rev repo = Lake.GitRepo.captureGit? #["rev-parse", "--verify", "--end-of-options", rev ++ "^{commit}"] repo

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

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

Equations

• repo.getHeadRevision? = Lake.GitRepo.resolveRevision? Lake.GitRev.head repo

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• repo.findRemoteRevision rev? remote = do repo.fetch remote Lake.GitRepo.resolveRemoteRevision (rev?.getD Lake.Git.upstreamBranch) remote repo

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

Equations

• Lake.GitRepo.branchExists rev repo = Lake.GitRepo.testGit #["show-ref", "--verify", toString "refs/heads/" ++ toString rev] repo

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

Equations

• Lake.GitRepo.revisionExists rev repo = Lake.GitRepo.testGit #["rev-parse", "--verify", rev ++ "^{commit}"] repo

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

Equations

• repo.getTags = do let __x ← Lake.GitRepo.captureGit? #["tag"] repo match __x with | some out => pure (out.split '\n').toStringList | x => pure []

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

Equations

• Lake.GitRepo.findTag? rev repo = Lake.GitRepo.captureGit? #["describe", "--tags", "--exact-match", rev] repo

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

Equations

• Lake.GitRepo.getRemoteUrl? remote repo = Lake.GitRepo.captureGit? #["remote", "get-url", remote] repo

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

Equations

• Lake.GitRepo.addRemote remote url repo = Lake.GitRepo.execGit #["remote", "add", remote, url] repo

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

Equations

• Lake.GitRepo.setRemoteUrl remote url repo = Lake.GitRepo.execGit #["remote", "set-url", remote, url] repo

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

Equations

• Lake.GitRepo.getFilteredRemoteUrl? remote repo = (do let __do_lift ← Lake.GitRepo.getRemoteUrl? remote repo liftM (Lake.Git.filterUrl? __do_lift)).run

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

Equations

• repo.hasNoDiff = Lake.GitRepo.testGit #["diff", "--exit-code", "HEAD"] repo

@[inline]

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

Equations

• repo.hasDiff = not <$> repo.hasNoDiff