def Lake.Git.defaultRemote : String

Equations

• Lake.Git.defaultRemote = "origin"

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.

Equations

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

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

structure Lake.GitRepo : Type

• dir : System.FilePath

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

Equations

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

instance Lake.instToStringGitRepo : ToString Lake.GitRepo

def Lake.GitRepo.cwd : Lake.GitRepo

Equations

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

@[inline]

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

@[inline]

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

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

Equations

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

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

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

Equations

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

@[inline]

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

@[inline]

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

@[inline]

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

Equations

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

@[inline]

def Lake.GitRepo.findTag? (rev : String := "HEAD") (repo : Lake.GitRepo) : BaseIO (Option String)

Equations

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

@[inline]

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

Equations

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

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

@[inline]

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

@[inline]

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

Equations

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