Lake.Util.Git

source

def Lake.Git.defaultRemote :

String

Equations

Instances For

source

def Lake.Git.upstreamBranch :

String

Equations

Instances For

source

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

Instances For

source

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

Bool

Equations

Instances For

source

structure Lake.GitRepo :

Type

dir : System.FilePath

Instances For

source

instance Lake.instCoeFilePathGitRepo :

Coe System.FilePath GitRepo

Equations

source

instance Lake.instToStringGitRepo :

ToString GitRepo

Equations

source

def Lake.GitRepo.cwd :

GitRepo

Equations

Instances For

source

@[inline]

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

BaseIO Bool

Equations

Instances For

source

@[inline]

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

LogIO String

Equations

Instances For

source

@[inline]

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

BaseIO (Option String)

Equations

Instances For

source

@[inline]

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

LogIO PUnit

Equations

Instances For

source

@[inline]

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

BaseIO Bool

Equations

Instances For

source

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

LogIO PUnit

Equations

Instances For

source

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

LogIO PUnit

Equations

Instances For

source

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

BaseIO Bool

Equations

Instances For

source

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

LogIO PUnit

Equations

Instances For

source

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

LogIO PUnit

Equations

Instances For

source

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

LogIO PUnit

Equations

Instances For

source

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

BaseIO (Option String)

Equations

Instances For

source

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

LogIO String

Equations

Instances For

source

@[inline]

def Lake.GitRepo.getHeadRevision? (repo : GitRepo) :

BaseIO (Option String)

Equations

Instances For

source

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

LogIO String

Equations

Instances For

source

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

LogIO (Array String)

Equations

Instances For

source

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

LogIO String

Equations

Instances For

source

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

LogIO String

Equations

Instances For

source

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

BaseIO Bool

Equations

Instances For

source

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

BaseIO Bool

Equations

Instances For

source

def Lake.GitRepo.getTags (repo : GitRepo) :

BaseIO (List String)

Equations

Instances For

source

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

BaseIO (Option String)

Equations

Instances For

source

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

BaseIO (Option String)

Equations

Instances For

source

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

BaseIO (Option String)

Equations

Instances For

source

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

BaseIO Bool

Equations

Instances For

source

@[inline]

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

BaseIO Bool

Equations

Instances For