diff --git a/Lake/Build/Context.lean b/Lake/Build/Context.lean index 5fb2491661..3d4652e96f 100644 --- a/Lake/Build/Context.lean +++ b/Lake/Build/Context.lean @@ -38,7 +38,7 @@ instance : MonadLift IO BuildM := ⟨MonadError.runIO⟩ instance [Pure m] : MonadLift LakeM (BuildT m) where monadLift x := fun ctx => pure <| x.run ctx.toContext -instance : MonadLift (LogT IO) BuildM where +instance : MonadLift LogIO BuildM where monadLift x := fun ctx meths => liftM (n := BuildM) (x.run meths.lift) ctx meths def BuildM.run (logMethods : MonadLog BaseIO) (ctx : BuildContext) (self : BuildM α) : IO α := diff --git a/Lake/CLI/Init.lean b/Lake/CLI/Init.lean index d5a8128ce8..086be040e0 100644 --- a/Lake/CLI/Init.lean +++ b/Lake/CLI/Init.lean @@ -123,7 +123,7 @@ def InitTemplate.configFileContents (pkgName root : Name) : InitTemplate → Str instance : Inhabited InitTemplate := ⟨.std⟩ /-- Initialize a new Lake package in the given directory with the given name. -/ -def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) : LogT IO PUnit := do +def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) : LogIO PUnit := do let pkgName := name.decapitalize.toName -- determine the name to use for the root @@ -168,17 +168,18 @@ def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) : LogT IO PUni -- initialize a `.git` repository if none already unless (← FilePath.isDir <| dir / ".git") do + let repo := GitRepo.mk dir try - quietInit dir + repo.quietInit unless upstreamBranch = "master" do - checkoutBranch upstreamBranch dir + repo.checkoutBranch upstreamBranch catch _ => logWarning "failed to initialize git repository" -def init (pkgName : String) (tmp : InitTemplate) : LogT IO PUnit := +def init (pkgName : String) (tmp : InitTemplate) : LogIO PUnit := initPkg "." pkgName tmp -def new (pkgName : String) (tmp : InitTemplate) : LogT IO PUnit := do +def new (pkgName : String) (tmp : InitTemplate) : LogIO PUnit := do let dirName := pkgName.map fun chr => if chr == '.' then '-' else chr IO.FS.createDir dirName initPkg dirName pkgName tmp diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean index e9fd8b93cd..62bebbf0c0 100644 --- a/Lake/CLI/Main.lean +++ b/Lake/CLI/Main.lean @@ -35,11 +35,11 @@ structure LakeConfig where lakeInstall : LakeInstall args : List String := [] -def loadPkg (config : LakeConfig) : LogT IO Package := do +def loadPkg (config : LakeConfig) : LogIO Package := do setupLeanSearchPath config.leanInstall config.lakeInstall Package.load config.rootDir config.args (config.rootDir / config.configFile) -def loadManifestMap (manifestFile : FilePath) : LogT IO (Lean.NameMap PackageEntry) := do +def loadManifestMap (manifestFile : FilePath) : LogIO (Lean.NameMap PackageEntry) := do if let Except.ok contents ← IO.FS.readFile manifestFile |>.toBaseIO then match Json.parse contents with | Except.ok json => @@ -55,7 +55,7 @@ def loadManifestMap (manifestFile : FilePath) : LogT IO (Lean.NameMap PackageEnt else pure {} -def loadWorkspace (config : LakeConfig) (updateDeps := false) : LogT IO Workspace := do +def loadWorkspace (config : LakeConfig) (updateDeps := false) : LogIO Workspace := do let pkg ← loadPkg config let ws := Workspace.ofPackage pkg let manifestMap ← loadManifestMap ws.manifestFile @@ -221,7 +221,7 @@ def printPaths (config : LakeConfig) (imports : List String := []) : MainM PUnit def env (cmd : String) (args : Array String := #[]) : LakeT IO UInt32 := do IO.Process.spawn {cmd, args, env := ← getLeanEnv} >>= (·.wait) -def serve (config : LakeConfig) (args : Array String) : LogT IO UInt32 := do +def serve (config : LakeConfig) (args : Array String) : LogIO UInt32 := do let (extraEnv, moreServerArgs) ← try let ws ← loadWorkspace config diff --git a/Lake/Config/Load.lean b/Lake/Config/Load.lean index 9170af1ad3..fd1d0a4982 100644 --- a/Lake/Config/Load.lean +++ b/Lake/Config/Load.lean @@ -20,7 +20,7 @@ def defaultConfigFile : FilePath := "lakefile.lean" /-- Evaluate a `package` declaration to its respective `PackageConfig`. -/ unsafe def evalPackageDecl (env : Environment) (declName : Name) (dir : FilePath) (args : List String := []) (leanOpts := Options.empty) -: LogT IO PackageConfig := do +: LogIO PackageConfig := do let m := env.evalConstCheck IOPackager leanOpts ``IOPackager declName if let Except.ok ioPackager := m.run.run then logWarning "Support for IO in package declarations may be dropped. Raise an issue if you disagree." @@ -67,7 +67,7 @@ namespace Package /-- Unsafe implementation of `load`. -/ unsafe def loadUnsafe (dir : FilePath) (args : List String := []) (configFile := dir / defaultConfigFile) (leanOpts := Options.empty) -: LogT IO Package := do +: LogIO Package := do -- Read File & Initialize Environment let input ← IO.FS.readFile configFile @@ -145,4 +145,4 @@ the given directory with the given configuration file. -/ @[implementedBy loadUnsafe] opaque load (dir : FilePath) (args : List String := []) -(configFile := dir / defaultConfigFile) (leanOpts := Options.empty) : LogT IO Package +(configFile := dir / defaultConfigFile) (leanOpts := Options.empty) : LogIO Package diff --git a/Lake/Config/Resolve.lean b/Lake/Config/Resolve.lean index b2bf63ac41..3361e3714f 100644 --- a/Lake/Config/Resolve.lean +++ b/Lake/Config/Resolve.lean @@ -15,31 +15,28 @@ open Std System namespace Lake -section -open Git - -/-- Update the Git package in `dir` to `rev` if not already at it. -/ +/-- Update the Git package in `repo` to `rev` if not already at it. -/ def updateGitPkg (name : String) -(dir : FilePath) (rev? : Option String) : LogT IO PUnit := do +(repo : GitRepo) (rev? : Option String) : LogIO PUnit := do if let some rev := rev? then - if (← headRevision dir) == rev then return - logInfo s!"{name}: updating {dir} to revision {rev}" - unless ← revisionExists rev dir do fetch dir - checkoutDetach rev dir + if (← repo.headRevision) == rev then return + logInfo s!"{name}: updating {repo} to revision {rev}" + unless ← repo.revisionExists rev do repo.fetch + repo.checkoutDetach rev else - logInfo s!"{name}: updating {dir}" - pull dir + logInfo s!"{name}: updating {repo}" + repo.pull -/-- Clone the Git package as `dir`. -/ -def cloneGitPkg (name : String) (dir : FilePath) -(url : String) (rev? : Option String) : LogT IO PUnit := do - logInfo s!"{name}: cloning {url} to {dir}" - clone url dir +/-- Clone the Git package as `repo`. -/ +def cloneGitPkg (name : String) (repo : GitRepo) +(url : String) (rev? : Option String) : LogIO PUnit := do + logInfo s!"{name}: cloning {url} to {repo}" + repo.clone url if let some rev := rev? then - let hash ← parseOriginRevision rev dir - checkoutDetach hash dir + let hash ← repo.parseOriginRevision rev + repo.checkoutDetach hash -abbrev ResolveM := StateT (NameMap PackageEntry) <| LogT IO +abbrev ResolveM := StateT (NameMap PackageEntry) <| LogIO /-- Materializes a Git package in `dir`, cloning and/or updating it as necessary. @@ -50,39 +47,38 @@ and saves the result to the manifest. -/ def materializeGitPkg (name : String) (dir : FilePath) (url : String) (rev? : Option String) (shouldUpdate := true) : ResolveM PUnit := do + let repo := GitRepo.mk dir if let some entry := (← get).find? name then - if (← dir.isDir) then + if (← repo.dirExists) then if url = entry.url then if shouldUpdate then - updateGitPkg name dir rev? - let rev ← headRevision dir + updateGitPkg name repo rev? + let rev ← repo.headRevision modify (·.insert name {entry with rev}) else - updateGitPkg name dir entry.rev + updateGitPkg name repo entry.rev else if shouldUpdate then logInfo s!"{name}: URL changed, deleting {dir} and cloning again" IO.FS.removeDirAll dir - cloneGitPkg name dir url rev? - let rev ← headRevision dir + cloneGitPkg name repo url rev? + let rev ← repo.headRevision modify (·.insert name {entry with url, rev}) else if shouldUpdate then - cloneGitPkg name dir url rev? - let rev ← headRevision dir + cloneGitPkg name repo url rev? + let rev ← repo.headRevision modify (·.insert name {entry with url, rev}) else - cloneGitPkg name dir entry.url entry.rev + cloneGitPkg name repo entry.url entry.rev else - if (← dir.isDir) then - let rev ← headRevision dir + if (← repo.dirExists) then + let rev ← repo.headRevision modify (·.insert name {name, url, rev}) else - cloneGitPkg name dir url rev? - let rev ← headRevision dir + cloneGitPkg name repo url rev? + let rev ← repo.headRevision modify (·.insert name {name, url, rev}) -end - /-- Materializes a `Dependency` relative to the given `Package`, downloading and/or updating it as necessary. diff --git a/Lake/Util/Git.lean b/Lake/Util/Git.lean index de481ebbf8..ae37b5225d 100644 --- a/Lake/Util/Git.lean +++ b/Lake/Util/Git.lean @@ -3,9 +3,13 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone -/ +import Lake.Util.Log +import Lake.Util.Misc open System -namespace Lake.Git +namespace Lake + +namespace Git def upstreamBranch := "master" @@ -17,57 +21,81 @@ def defaultRevision : Option String → String | none => upstreamBranch | some branch => branch -def execGit (args : Array String) (repo : Option FilePath := none) : IO PUnit := do - let child ← IO.Process.spawn { - cmd := "git", args, cwd := repo, - stdout := IO.Process.Stdio.null, stderr := IO.Process.Stdio.null - } - let exitCode ← child.wait - if exitCode != 0 then - throw <| IO.userError <| "git exited with code " ++ toString exitCode - -def captureGit (args : Array String) (repo : Option FilePath := none) : IO String := do - let out ← IO.Process.output {cmd := "git", args, cwd := repo} +def capture (args : Array String) (wd : Option FilePath := none) : LogIO String := do + let out ← IO.Process.output {cmd := "git", args, cwd := wd} if out.exitCode != 0 then - throw <| IO.userError <| "git exited with code " ++ toString out.exitCode + logError s!"stdout:\n{out.stdout}\nstderr:\n{out.stderr}" + error <| "git exited with code " ++ toString out.exitCode return out.stdout -def clone (url : String) (dir : FilePath) := - execGit #["clone", url, dir.toString] +def exec (args : Array String) (wd : Option FilePath := none) : LogIO PUnit := do + discard <| capture args wd -def quietInit (repo : Option FilePath := none) := - execGit #["init", "-q"] repo +def test (args : Array String) (wd : Option FilePath := none) : LogT BaseIO Bool := + let act : IO _ := do + let child ← IO.Process.spawn {cmd := "git", args, cwd := wd} + return (← child.wait) == 0 + act.catchExceptions fun _ => pure false -def fetch (repo : Option FilePath := none) := - execGit #["fetch"] repo +end Git -def pull (repo : Option FilePath := none) := - execGit #["pull"] repo +structure GitRepo where + dir : FilePath -def checkoutBranch (branch : String) (repo : Option FilePath := none) := - execGit #["checkout", "-B", branch] repo +instance : ToString GitRepo := ⟨(·.dir.toString)⟩ -def checkoutDetach (hash : String) (repo : Option FilePath := none) := - execGit #["checkout", "--detach", hash] repo +namespace GitRepo -def parseRevision (rev : String) (repo : Option FilePath := none) : IO String := do - let rev ← captureGit #["rev-parse", "-q", "--verify", rev] repo +def cwd : GitRepo := ⟨"."⟩ + +def dirExists (repo : GitRepo) : BaseIO Bool := + repo.dir.isDir + +def captureGit (args : Array String) (repo : GitRepo) : LogIO String := + Git.capture args repo.dir + +def execGit (args : Array String) (repo : GitRepo) : LogIO PUnit := + Git.exec args repo.dir + +def testGit (args : Array String) (repo : GitRepo) : LogIO Bool := + Git.test args repo.dir + +def clone (url : String) (repo : GitRepo) : LogIO PUnit := + Git.exec #["clone", url, repo.dir.toString] + +def quietInit (repo : GitRepo) : LogIO PUnit := + repo.execGit #["init", "-q"] + +def fetch (repo : GitRepo) : LogIO PUnit := + repo.execGit #["fetch"] + +def pull (repo : GitRepo) : LogIO PUnit := + repo.execGit #["pull"] + +def checkoutBranch (branch : String) (repo : GitRepo) : LogIO PUnit := + repo.execGit #["checkout", "-B", branch] + +def checkoutDetach (hash : String) (repo : GitRepo) : LogIO PUnit := + repo.execGit #["checkout", "--detach", hash] + +def parseRevision (rev : String) (repo : GitRepo) : LogIO String := do + let rev ← repo.captureGit #["rev-parse", "--verify", rev] pure rev.trim -- remove newline at end -def headRevision (repo : Option FilePath := none) : IO String := +def headRevision (repo : GitRepo) : LogIO String := parseRevision "HEAD" repo -def parseOriginRevision (rev : String) (repo : Option FilePath := none) : IO String := do - if isFullObjectName rev then return rev - (parseRevision ("origin/" ++ rev) repo) <|> parseRevision rev repo - <|> throw (IO.userError s!"cannot find revision {rev} in repository {repo}") +def parseOriginRevision (rev : String) (repo : GitRepo) : LogIO String := do + if Git.isFullObjectName rev then return rev + repo.parseRevision ("origin/" ++ rev) <|> repo.parseRevision rev + <|> error s!"cannot find revision {rev} in repository {repo}" -def latestOriginRevision (branch : Option String) (repo : Option FilePath := none) : IO String := do - execGit #["fetch"] repo - parseOriginRevision (defaultRevision branch) repo +def latestOriginRevision (branch : Option String) (repo : GitRepo) : LogIO String := do + repo.execGit #["fetch"] + parseOriginRevision (Git.defaultRevision branch) repo -def revisionExists (rev : String) (repo : Option FilePath := none) : IO Bool := do - try - discard <| parseRevision (rev ++ "^{commit}") repo - pure true - catch _ => pure false +def branchExists (rev : String) (repo : GitRepo) : LogIO Bool := do + repo.testGit #["show-ref", "--verify", s!"refs/heads/{rev}"] + +def revisionExists (rev : String) (repo : GitRepo) : LogIO Bool := do + repo.testGit #["rev-parse", "--verify", rev ++ "^{commit}"] diff --git a/Lake/Util/Log.lean b/Lake/Util/Log.lean index 5d30207450..4b0fda4671 100644 --- a/Lake/Util/Log.lean +++ b/Lake/Util/Log.lean @@ -83,6 +83,9 @@ abbrev adaptMethods [Monad n] end MonadLogT +abbrev LogIO := + MonadLogT BaseIO IO + abbrev LogT (m : Type → Type) := MonadLogT m m diff --git a/Lake/Util/MainM.lean b/Lake/Util/MainM.lean index 7d408ad4c6..668eef89cb 100644 --- a/Lake/Util/MainM.lean +++ b/Lake/Util/MainM.lean @@ -75,4 +75,4 @@ protected def error (msg : String) (rc : ExitCode := 1) : MainM α := do instance : MonadError MainM := ⟨MainM.error⟩ instance [ToString ε] : MonadLift (EIO ε) MainM := ⟨MonadError.runEIO⟩ instance : MonadLift IO MainM := inferInstance -- necessary, but don't know why -instance : MonadLift (LogT IO) MainM := ⟨fun x => liftM <| x.run MonadLog.eio⟩ +instance : MonadLift LogIO MainM := ⟨fun x => liftM <| x.run MonadLog.eio⟩