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.dropRight 4) else some url

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

Equations

• Lake.Git.isFullObjectName rev = (rev.length == 40 && rev.all fun (c : Char) => c.isDigit || decide ('a' ≤ c) && decide (c ≤ 'f'))

structure Lake.GitRepo : Type

• dir : Lake.FilePath

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

Equations

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

instance Lake.instToStringGitRepo : ToString Lake.GitRepo

Equations

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

def Lake.GitRepo.cwd : Lake.GitRepo

Equations

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

@[inline]

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

Equations

• repo.dirExists = repo.dir.isDir

@[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.fetch (repo : Lake.GitRepo) (remote : optParam String Lake.Git.defaultRemote) : Lake.LogIO PUnit

Equations

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

@[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)

Equations

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

@[inline]

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

Equations

• repo.getHeadRevision? = Lake.GitRepo.resolveRevision? "HEAD" repo

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 : optParam String Lake.Git.defaultRemote) (repo : Lake.GitRepo) : Lake.LogIO String

Equations

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

def Lake.GitRepo.findRemoteRevision (repo : Lake.GitRepo) (rev? : optParam (Option String) none) (remote : optParam 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

Equations

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

@[inline]

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

Equations

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

@[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 : optParam 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 : optParam 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 : optParam String Lake.Git.defaultRemote) (repo : Lake.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

@[inline]

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

Equations

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

@[inline]

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

Equations

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