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 String.startsWith url "git" = true then none else if String.endsWith url ".git" = true then some (String.dropRight url 4) else some url

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

Equations

• Lake.Git.isFullObjectName rev = (String.length rev == 40 && String.all rev fun (c : Char) => Char.isDigit c || decide (Char.ofNat 97 ≤ c) && decide (c ≤ Char.ofNat 102))

structure Lake.GitRepo : Type

• dir : Lake.FilePath

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

• Lake.GitRepo.dirExists repo = System.FilePath.isDir repo.dir

@[inline]

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

Equations

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

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

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

@[inline]

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

Equations

• Lake.GitRepo.fetch repo remote = Lake.GitRepo.execGit #["fetch", 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", rev] repo

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

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

• Lake.GitRepo.findRemoteRevision repo rev? remote = do Lake.GitRepo.fetch repo remote Lake.GitRepo.resolveRemoteRevision (Option.getD rev? 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.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 = OptionT.run do let __do_lift ← Lake.GitRepo.getRemoteUrl? remote repo liftM (Lake.Git.filterUrl? __do_lift)

@[inline]

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

Equations

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

@[inline]

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

Equations

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