Solver now returns Package

Leanpkg2/Manifest.lean

@@ -26,6 +26,7 @@ structure Manifest where
   path : Option FilePath := none
   module : String := name.capitalize
   dependencies : List Dependency := []
+  deriving Inhabited
 
 namespace Manifest
 
@@ -37,9 +38,16 @@ end Manifest
 structure Package where
   dir : FilePath
   manifest : Manifest
+  deriving Inhabited
 
 namespace Package
 
+def name (self : Package) : String :=
+  self.manifest.name
+
+def dependencies (self : Package) : List Dependency :=
+  self.manifest.dependencies
+
 def sourceDir (self : Package) : FilePath :=
   self.dir / self.manifest.effectivePath
 

Leanpkg2/Resolve.lean

@@ -6,12 +6,15 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 import Leanpkg2.Git
 import Leanpkg2.Proc
 import Leanpkg2.TomlManifest
+import Leanpkg2.BuildConfig
 
 open System
 
 namespace Leanpkg2
 
-def Assignment := List (String × FilePath)
+def depsPath := buildPath / "deps"
+
+def Assignment := List (String × Package)
 
 namespace Assignment
 def empty : Assignment := []
@@ -19,10 +22,10 @@ def empty : Assignment := []
 def contains (a : Assignment) (s : String) : Bool :=
   (a.lookup s).isSome
 
-def insert (a : Assignment) (k : String) (v : FilePath) : Assignment :=
+def insert (a : Assignment) (k : String) (v : Package) : Assignment :=
   if a.contains k then a else (k, v) :: a
 
-def fold {α} (i : α) (f : α → String → FilePath → α) : Assignment → α :=
+def fold {α} (i : α) (f : α → String → Package → α) : Assignment → α :=
   List.foldl (fun a ⟨k, v⟩ => f a k v) i
 
 end Assignment
@@ -32,18 +35,19 @@ abbrev Solver := StateT Assignment IO
 def notYetAssigned (d : String) : Solver Bool := do
   ¬ (← get).contains d
 
-def resolvedPath (d : String) : Solver FilePath := do
-  let some path ← pure ((← get).lookup d) | unreachable!
-  path
+def resolvedPackage (d : String) : Solver Package := do
+  let some pkg ← pure ((← get).lookup d) | unreachable!
+  pkg
 
-def materialize (relpath : FilePath) (dep : Dependency) : Solver Unit :=
+def materialize (relPath : FilePath) (dep : Dependency) : Solver Unit :=
   match dep.src with
   | Source.path dir => do
-    let depdir := dir / relpath
+    let depdir := dir / relPath
     IO.eprintln s!"{dep.name}: using local path {depdir}"
-    modify (·.insert dep.name depdir)
+    let m ← Manifest.fromTomlFile <| depdir / leanpkgToml
+    modify (·.insert dep.name ⟨depdir, m⟩)
   | Source.git url rev branch => do
-    let depdir := FilePath.mk "build" / "deps" / dep.name
+    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)
@@ -56,24 +60,20 @@ def materialize (relpath : FilePath) (dep : Dependency) : Solver Unit :=
       execCmd {cmd := "git", args := #["clone", url, depdir.toString]}
     let hash ← gitParseOriginRevision depdir rev
     execCmd {cmd := "git", args := #["checkout", "--detach", hash], cwd := depdir}
-    modify (·.insert dep.name depdir)
+    let m ← Manifest.fromTomlFile <| depdir / leanpkgToml
+    modify (·.insert dep.name ⟨depdir, m⟩)
 
-def solveDepsCore (relPath : FilePath) (d : Manifest) : (maxDepth : Nat) → Solver Unit
+def solveDepsCore (pkg : String) (relPath : FilePath) (deps : List Dependency) : (maxDepth : Nat) → Solver Unit
   | 0 => throw <| IO.userError "maximum dependency resolution depth reached"
   | maxDepth + 1 => do
-    let deps ← d.dependencies.filterM (notYetAssigned ·.name)
-    deps.forM (materialize relPath)
-    for dep in deps do
-      let p ← resolvedPath dep.name
-      let d' ← Manifest.fromTomlFile <| p / leanpkgToml
-      unless d'.name = dep.name do
-        throw <| IO.userError s!"{d.name} (in {relPath}) depends on {d'.name}, but resolved dependency has name {dep.name} (in {p})"
-      solveDepsCore p d' maxDepth
+    let newDeps ← deps.filterM (notYetAssigned ·.name)
+    newDeps.forM (materialize relPath)
+    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})"
+      solveDepsCore depPkg.name depPkg.dir depPkg.dependencies maxDepth
 
 def solveDeps (m : Manifest) : IO (List Package) := do
-  let (_, assg) ← (solveDepsCore ⟨"."⟩ m 1024).run <| Assignment.empty.insert m.name ⟨"."⟩
-  assg.reverse.mapM fun ⟨depname, dirname⟩ => do
-    if dirname == "." then
-      return ⟨ dirname, m ⟩
-    else
-      return ⟨ dirname, ← Manifest.fromTomlFile <| dirname / leanpkgToml ⟩
+  let (_, assg) ← (solveDepsCore m.name ⟨"."⟩ m.dependencies 1024).run <| Assignment.empty.insert m.name ⟨".", m⟩
+  assg.reverse.mapM (·.2)