CLI now uses configuration from package.lean'

Leanpkg2/Build.lean

@@ -118,17 +118,21 @@ def buildImports (pkg : Package) (deps : List Package) (imports leanArgs : List
     else
       buildModules (mkBuildConfig pkg deps leanArgs) localImports
 
+
+def doBuild (pkg : Package) (deps : List Package) (makeArgs leanArgs : List String := []) : IO Unit := do
+  if makeArgs != [] || (← FilePath.pathExists "Makefile") then
+    execMake pkg deps makeArgs leanArgs
+  else
+    buildModules (mkBuildConfig pkg deps leanArgs) [pkg.module]
+
 def buildDeps (pkg : Package) : IO (List Package) := do
   let deps ← solveDeps pkg
   for dep in deps do
     unless dep.dir == pkg.dir do
       -- build recursively
       -- TODO: share build of common dependencies
-      execCmd {
-        cwd := dep.dir
-        cmd := (← IO.appDir) / "lean" |>.toString
-        args := #["--run", "Package.lean"]
-      }
+      let depDeps ← solveDeps dep
+      doBuild dep depDeps ["lib"]
   return deps
 
 def configure (pkg : Package) : IO Unit := do
@@ -142,7 +146,4 @@ def printPaths (pkg : Package) (imports leanArgs : List String := []) : IO Unit
 
 def build (pkg : Package) (makeArgs leanArgs : List String := []) : IO Unit := do
   let deps ← buildDeps pkg
-  if makeArgs != [] || (← FilePath.pathExists "Makefile") then
-    execMake pkg deps makeArgs leanArgs
-  else
-    buildModules (mkBuildConfig pkg deps leanArgs) [pkg.module]
+  doBuild pkg deps makeArgs leanArgs

Leanpkg2/Cli.lean

@@ -5,7 +5,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Leanpkg2.Init
 import Leanpkg2.Build
-import Leanpkg2.TomlConfig
+import Leanpkg2.LeanConfig
 
 namespace Leanpkg2
 
@@ -62,7 +62,7 @@ This command creates a new Lean package with the given name in the current
 directory."
 
 def getRootPkg : IO Package := do
-  let cfg ← PackageConfig.fromTomlFile leanpkgToml
+  let cfg ← PackageConfig.fromLeanFile leanConfigFile
   if cfg.leanVersion ≠ leanVersionString then
     IO.eprintln $ "\nWARNING: Lean version mismatch: installed version is " ++
       leanVersionString ++ ", but package requires " ++ cfg.leanVersion ++ "\n"

Leanpkg2/LeanConfig.lean

@@ -0,0 +1,28 @@
+
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lean
+import Leanpkg2.Package
+
+open Lean Elab System
+
+namespace Leanpkg2
+
+def leanConfigFile : FilePath := "package.lean"
+
+namespace PackageConfig
+
+unsafe def fromLeanFileUnsafe (path : FilePath) : IO PackageConfig := do
+  let input ← IO.FS.readFile path
+  let (env, ok) ← runFrontend input Options.empty path.toString `package
+  if ok then
+    IO.ofExcept <| Id.run <| ExceptT.run <|
+      env.evalConstCheck PackageConfig Options.empty ``PackageConfig `package
+  else
+    throw <| IO.userError <| s!"package configuration (at {path}) has errors"
+
+@[implementedBy fromLeanFileUnsafe]
+constant fromLeanFile (path : FilePath) : IO PackageConfig

Leanpkg2/Resolve.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Leanpkg2.Git
-import Leanpkg2.TomlConfig
+import Leanpkg2.LeanConfig
 
 open System
 
@@ -69,7 +69,7 @@ def solveDepsCore (pkg : Package) : (maxDepth : Nat) → Solver Unit
     let newDeps ← pkg.dependencies.filterM (notYetAssigned ·.name)
     for dep in newDeps do
       let dir ← materialize pkg.dir dep
-      let cfg ← PackageConfig.fromTomlFile <| dir / leanpkgToml
+      let cfg ← PackageConfig.fromLeanFile <| dir / leanConfigFile
       modify (·.insert dep.name ⟨dir, cfg⟩)
     for dep in newDeps do
       let depPkg ← resolvedPackage dep.name

examples/hello/package.lean

@@ -1,17 +1,6 @@
-import Leanpkg2.Build
+import Leanpkg2.Package
 
-open Leanpkg2
-
-def package : PackageConfig := {
+def package : Leanpkg2.PackageConfig := {
   name := "hello",
   version := "1.0",
 }
-
-def configure : IO Unit :=
-  Leanpkg2.configure ⟨".", package⟩
-
-def build : IO Unit :=
-  Leanpkg2.build ⟨".", package⟩ ["bin"]
-
-def main : IO Unit :=
-  build

examples/hello/package.sh

@@ -1,2 +1,2 @@
 export LEAN_PATH=../../build
-lean --run Package.lean
+lean --run ../../Leanpkg2.lean build bin

examples/helloDeps/a/package.lean

@@ -1,14 +1,6 @@
-import Leanpkg2.Build
+import Leanpkg2.Package
 
-open Leanpkg2
-
-def package : PackageConfig := {
+def package : Leanpkg2.PackageConfig := {
   name := "a",
   version := "1.0",
 }
-
-def build : IO Unit :=
-  Leanpkg2.build ⟨".", package⟩ ["lib"]
-
-def main : IO Unit :=
-  build

examples/helloDeps/b/package.lean

@@ -9,9 +9,3 @@ def package : PackageConfig := {
     { name := "a", src := Source.path (FilePath.mk ".." / "a") }
   ]
 }
-
-def build : IO Unit := do
-  Leanpkg2.build ⟨".", package⟩ ["bin", "LINK_OPTS=../a/build/lib/libA.a"]
-
-def main : IO Unit :=
-  build

examples/helloDeps/package.sh

@@ -1,3 +1,3 @@
 cd b
 export LEAN_PATH=../../../build
-lean --run Package.lean
+lean --run ../../../Leanpkg2.lean build bin LINK_OPTS=../a/build/lib/libA.a