diff --git a/Leanpkg2/Git.lean b/Leanpkg2/Git.lean index fb8ca06de2..59eb4500ba 100644 --- a/Leanpkg2/Git.lean +++ b/Leanpkg2/Git.lean @@ -1,38 +1,54 @@ /- 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 +Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone -/ +import Leanpkg2.Proc import Leanpkg2.LeanVersion open System -namespace Leanpkg2 +namespace Leanpkg2.Git -def upstreamGitBranch := +def upstreamBranch := "master" -def gitdefaultRevision : Option String → String - | none => upstreamGitBranch +def defaultRevision : Option String → String + | none => upstreamBranch | some branch => branch -def gitParseRevision (gitRepo : FilePath) (rev : String) : IO String := do - let rev ← IO.Process.run {cmd := "git", args := #["rev-parse", "-q", "--verify", rev], cwd := gitRepo} +def clone (url : String) (dir : FilePath) := + execCmd {cmd := "git", args := #["clone", url, dir.toString]} + +def quietInit (repo : Option FilePath := none) := + execCmd {cmd := "git", args := #["init", "-q"]} + +def fetch (repo : Option FilePath := none) := + execCmd {cmd := "git", args := #["fetch"], cwd := repo} + +def checkoutBranch (branch : String) (repo : Option FilePath := none) := + execCmd {cmd := "git", args := #["checkout", "-B", branch]} + +def checkoutDetach (hash : String) (repo : Option FilePath := none) := + execCmd {cmd := "git", args := #["checkout", "--detach", hash], cwd := repo} + +def parseRevision (rev : String) (repo : Option FilePath := none) : IO String := do + let rev ← IO.Process.run {cmd := "git", args := #["rev-parse", "-q", "--verify", rev], cwd := repo} rev.trim -- remove newline at end -def gitHeadRevision (gitRepo : FilePath) : IO String := - gitParseRevision gitRepo "HEAD" +def headRevision (repo : Option FilePath := none) : IO String := + parseRevision "HEAD" repo -def gitParseOriginRevision (gitRepo : FilePath) (rev : String) : IO String := - (gitParseRevision gitRepo $ "origin/" ++ rev) <|> gitParseRevision gitRepo rev - <|> throw (IO.userError s!"cannot find revision {rev} in repository {gitRepo}") +def parseOriginRevision (rev : String) (repo : Option FilePath := none) : IO String := + (parseRevision ("origin/" ++ rev) repo) <|> parseRevision rev repo + <|> throw (IO.userError s!"cannot find revision {rev} in repository {repo}") -def gitLatestOriginRevision (gitRepo : FilePath) (branch : Option String) : IO String := do - discard <| IO.Process.run {cmd := "git", args := #["fetch"], cwd := gitRepo} - gitParseOriginRevision gitRepo (gitdefaultRevision branch) +def latestOriginRevision (branch : Option String) (repo : Option FilePath := none) : IO String := do + discard <| IO.Process.run {cmd := "git", args := #["fetch"], cwd := repo} + parseOriginRevision (defaultRevision branch) repo -def gitRevisionExists (gitRepo : FilePath) (rev : String) : IO Bool := do +def revisionExists (rev : String) (repo : Option FilePath := none) : IO Bool := do try - discard <| gitParseRevision gitRepo (rev ++ "^{commit}") + discard <| parseRevision (rev ++ "^{commit}") repo true catch _ => false diff --git a/Leanpkg2/Init.lean b/Leanpkg2/Init.lean index bf26c46b1e..97026ba820 100644 --- a/Leanpkg2/Init.lean +++ b/Leanpkg2/Init.lean @@ -25,6 +25,7 @@ version = \"0.1\" lean_version = \"{leanVersionString}\" " +open Git in def initPkg (pkgName : String) (fromNew : Bool) : IO Unit := do IO.FS.writeFile leanpkgToml (leanpkgFileContents pkgName) IO.FS.writeFile ⟨s!"{pkgName.capitalize}.lean"⟩ mainFileContents @@ -32,9 +33,10 @@ def initPkg (pkgName : String) (fromNew : Bool) : IO Unit := do h.putStr initGitignoreContents unless ← System.FilePath.isDir ⟨".git"⟩ do (do - execCmd {cmd := "git", args := #["init", "-q"]} - unless upstreamGitBranch = "master" do - execCmd {cmd := "git", args := #["checkout", "-B", upstreamGitBranch]} - ) <|> IO.eprintln "WARNING: failed to initialize git repository" + quietInit + unless upstreamBranch = "master" do + checkoutBranch upstreamBranch + ) <|> + IO.eprintln "WARNING: failed to initialize git repository" def init (pkgName : String) := initPkg pkgName false diff --git a/Leanpkg2/Resolve.lean b/Leanpkg2/Resolve.lean index f4152b5d0f..780644cfb4 100644 --- a/Leanpkg2/Resolve.lean +++ b/Leanpkg2/Resolve.lean @@ -12,6 +12,33 @@ open System namespace Leanpkg2 +open Git in +def materializeGit + (name : String) (dir : FilePath) (url rev : String) (branch : Option String) +: IO Unit := do + if ← dir.isDir then + IO.eprint s!"{name}: trying to update {dir} to revision {rev}" + IO.eprintln (match branch with | none => "" | some branch => "@" ++ branch) + let hash ← parseOriginRevision rev dir + unless ← revisionExists hash dir do fetch dir + checkoutDetach hash dir + else + IO.eprintln s!"{name}: cloning {url} to {dir}" + clone url dir + let hash ← parseOriginRevision rev dir + checkoutDetach hash dir + +def materialize (relPath : FilePath) (dep : Dependency) : IO FilePath := + match dep.src with + | Source.path dir => do + let depdir := dir / relPath + IO.eprintln s!"{dep.name}: using local path {depdir}" + depdir + | Source.git url rev branch => do + let depdir := depsPath / dep.name + materializeGit dep.name depdir url rev branch + depdir + def Assignment := List (String × Package) namespace Assignment @@ -37,41 +64,23 @@ def resolvedPackage (d : String) : Solver Package := do let some pkg ← pure ((← get).lookup d) | unreachable! pkg -def materialize (relPath : FilePath) (dep : Dependency) : Solver Unit := - match dep.src with - | Source.path dir => do - let depdir := dir / relPath - IO.eprintln s!"{dep.name}: using local path {depdir}" - let m ← Manifest.fromTomlFile <| depdir / leanpkgToml - modify (·.insert dep.name ⟨depdir, m⟩) - | Source.git url rev branch => do - let depdir := depsPath / dep.name - if ← depdir.isDir then - IO.eprint s!"{dep.name}: trying to update {depdir} to revision {rev}" - IO.eprintln (match branch with | none => "" | some branch => "@" ++ branch) - let hash ← gitParseOriginRevision depdir rev - let revEx ← gitRevisionExists depdir hash - unless revEx do - execCmd {cmd := "git", args := #["fetch"], cwd := depdir} - else - IO.eprintln s!"{dep.name}: cloning {url} to {depdir}" - execCmd {cmd := "git", args := #["clone", url, depdir.toString]} - let hash ← gitParseOriginRevision depdir rev - execCmd {cmd := "git", args := #["checkout", "--detach", hash], cwd := depdir} - let m ← Manifest.fromTomlFile <| depdir / leanpkgToml - modify (·.insert dep.name ⟨depdir, m⟩) - -def solveDepsCore (pkg : String) (relPath : FilePath) (deps : List Dependency) : (maxDepth : Nat) → Solver Unit +def solveDepsCore + (pkgName : String) (relPath : FilePath) (deps : List Dependency) +: (maxDepth : Nat) → Solver Unit | 0 => throw <| IO.userError "maximum dependency resolution depth reached" | maxDepth + 1 => do let newDeps ← deps.filterM (notYetAssigned ·.name) - newDeps.forM (materialize relPath) + for dep in newDeps do + let dir ← materialize relPath dep + let m ← Manifest.fromTomlFile <| dir / leanpkgToml + modify (·.insert dep.name ⟨dir, m⟩) for dep in newDeps do let depPkg ← resolvedPackage dep.name unless depPkg.name = dep.name do - throw <| IO.userError s!"{pkg} (in {relPath}) depends on {depPkg.name}, but resolved dependency has name {dep.name} (in {depPkg.dir})" + throw <| IO.userError s!"{pkgName} (in {relPath}) depends on {depPkg.name}, but resolved dependency has name {dep.name} (in {depPkg.dir})" solveDepsCore depPkg.name depPkg.dir depPkg.dependencies maxDepth def solveDeps (m : Manifest) : IO (List Package) := do - let (_, assg) ← (solveDepsCore m.name ⟨"."⟩ m.dependencies 1024).run <| Assignment.empty.insert m.name ⟨".", m⟩ + let solver := solveDepsCore m.name ⟨"."⟩ m.dependencies 1024 + let (_, assg) ← solver.run (Assignment.empty.insert m.name ⟨".", m⟩) assg.reverse.mapM (·.2)