diff --git a/Leanpkg2/BuildConfig.lean b/Leanpkg2/BuildConfig.lean index de71b456fc..009ec6b06f 100644 --- a/Leanpkg2/BuildConfig.lean +++ b/Leanpkg2/BuildConfig.lean @@ -1,15 +1,14 @@ /- Copyright (c) 2021 Sebastian Ullrich. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Sebastian Ullrich +Authors: Sebastian Ullrich, Mac Malone -/ import Lean.Data.Name import Lean.Elab.Import import Leanpkg2.Package import Leanpkg2.Proc -open Lean -open System +open Lean System namespace Leanpkg2 @@ -22,8 +21,11 @@ structure BuildConfig where namespace BuildConfig -def fromPackages (module : Name) (leanArgs : List String) (pkgs : List Package) : BuildConfig := { +def fromPackages +(module : Name) (leanArgs : List String) (pkgs : List Package) +: BuildConfig := { module, leanArgs, leanPath := SearchPath.toString <| pkgs.map (·.buildDir) - moreDeps := pkgs.filter (·.dir.toString != ".") |>.map (·.buildRoot.withExtension "olean") + moreDeps := pkgs.filter (·.dir.toString != ".") |>.map + (·.buildRoot.withExtension "olean") } diff --git a/Leanpkg2/Resolve.lean b/Leanpkg2/Resolve.lean index e141405b63..cd20d1d4aa 100644 --- a/Leanpkg2/Resolve.lean +++ b/Leanpkg2/Resolve.lean @@ -42,6 +42,7 @@ def materialize (relPath : FilePath) (dep : Dependency) : IO FilePath := def Assignment := List (String × Package) namespace Assignment + def empty : Assignment := [] def contains (a : Assignment) (s : String) : Bool := @@ -65,7 +66,7 @@ def resolvedPackage (d : String) : Solver Package := do pkg def solveDepsCore - (pkgName : String) (relPath : FilePath) (deps : List Dependency) +(pkgName : String) (relPath : FilePath) (deps : List Dependency) : (maxDepth : Nat) → Solver Unit | 0 => throw <| IO.userError "maximum dependency resolution depth reached" | maxDepth + 1 => do