Refactored away the old notion of a manifest
This commit is contained in:
Mac Malone
parent
3cc0c3e370
commit
6b999dcb21
14 changed files with 138 additions and 135 deletions
|
|
@ -7,7 +7,6 @@ import Lean.Data.Name
|
|||
import Lean.Elab.Import
|
||||
import Leanpkg2.Resolve
|
||||
import Leanpkg2.Package
|
||||
import Leanpkg2.BuildConfig
|
||||
import Leanpkg2.Make
|
||||
import Leanpkg2.Proc
|
||||
|
||||
|
|
@ -15,6 +14,22 @@ open Lean System
|
|||
|
||||
namespace Leanpkg2
|
||||
|
||||
structure BuildConfig where
|
||||
module : Name
|
||||
leanArgs : List String
|
||||
leanPath : String
|
||||
-- things like `leanpkg.toml` and olean roots of dependencies that should also trigger rebuilds
|
||||
moreDeps : List FilePath
|
||||
|
||||
def mkBuildConfig
|
||||
(pkg : Package) (deps : List Package) (leanArgs : List String)
|
||||
: BuildConfig := {
|
||||
leanArgs,
|
||||
module := pkg.module
|
||||
leanPath := SearchPath.toString <| deps.map (·.buildDir)
|
||||
moreDeps := deps.filter (·.dir != pkg.dir) |>.map (·.oleanRoot)
|
||||
}
|
||||
|
||||
structure BuildContext extends BuildConfig where
|
||||
parents : List Name := []
|
||||
moreDepsMTime : IO.FS.SystemTime
|
||||
|
|
@ -84,7 +99,7 @@ partial def buildModule (mod : Name) : BuildM Result := do
|
|||
modify fun st => { st with modTasks := st.modTasks.insert mod r }
|
||||
return r
|
||||
|
||||
def buildModules (manifest : Manifest) (cfg : BuildConfig) (mods : List Name) : IO Unit := do
|
||||
def buildModules (cfg : BuildConfig) (mods : List Name) : IO Unit := do
|
||||
let moreDepsMTime := (← cfg.moreDeps.mapM (·.metadata)).map (·.modified) |>.maximum? |>.getD ⟨0, 0⟩
|
||||
let rs ← mods.mapM buildModule |>.run { toBuildConfig := cfg, moreDepsMTime } |>.run' {}
|
||||
for r in rs do
|
||||
|
|
@ -92,44 +107,42 @@ def buildModules (manifest : Manifest) (cfg : BuildConfig) (mods : List Name) :
|
|||
-- actual error has already been printed above
|
||||
throw <| IO.userError "Build failed."
|
||||
|
||||
def buildImports (manifest : Manifest) (cfg : BuildConfig) (imports leanArgs : List String := []) : IO Unit := do
|
||||
def buildImports (pkg : Package) (deps : List Package) (imports leanArgs : List String := []) : IO Unit := do
|
||||
let imports := imports.map (·.toName)
|
||||
let localImports := imports.filter (·.getRoot == cfg.module)
|
||||
let localImports := imports.filter (·.getRoot == pkg.module)
|
||||
if localImports != [] then
|
||||
if ← FilePath.pathExists "Makefile" then
|
||||
let oleans := localImports.map fun i =>
|
||||
Lean.modToFilePath buildPath i "olean" |>.toString
|
||||
execMake manifest oleans cfg
|
||||
execMake pkg deps oleans leanArgs
|
||||
else
|
||||
buildModules manifest cfg localImports
|
||||
buildModules (mkBuildConfig pkg deps leanArgs) localImports
|
||||
|
||||
def buildDeps (manifest : Manifest) : IO (List Package) := do
|
||||
let pkgs ← solveDeps manifest
|
||||
for pkg in pkgs do
|
||||
unless pkg.dir.toString == "." do
|
||||
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 := pkg.dir
|
||||
cwd := dep.dir
|
||||
cmd := (← IO.appDir) / "lean" |>.toString
|
||||
args := #["--run", "Package.lean"]
|
||||
}
|
||||
return pkgs
|
||||
return deps
|
||||
|
||||
def configure (manifest : Manifest) : IO Unit := do
|
||||
discard <| buildDeps manifest
|
||||
def configure (pkg : Package) : IO Unit := do
|
||||
discard <| buildDeps pkg
|
||||
|
||||
def printPaths (manifest : Manifest) (imports leanArgs : List String := []) : IO Unit := do
|
||||
let pkgs ← buildDeps manifest
|
||||
let cfg := BuildConfig.fromPackages manifest.module leanArgs pkgs
|
||||
buildImports manifest cfg imports leanArgs
|
||||
IO.println cfg.leanPath
|
||||
IO.println <| SearchPath.toString <| pkgs.map (·.sourceDir)
|
||||
def printPaths (pkg : Package) (imports leanArgs : List String := []) : IO Unit := do
|
||||
let deps ← buildDeps pkg
|
||||
buildImports pkg deps imports leanArgs
|
||||
IO.println <| SearchPath.toString <| deps.map (·.buildDir)
|
||||
IO.println <| SearchPath.toString <| deps.map (·.sourceDir)
|
||||
|
||||
def build (manifest : Manifest) (makeArgs leanArgs : List String := []) : IO Unit := do
|
||||
let pkgs ← buildDeps manifest
|
||||
let cfg := BuildConfig.fromPackages manifest.module leanArgs pkgs
|
||||
def build (pkg : Package) (makeArgs leanArgs : List String := []) : IO Unit := do
|
||||
let deps ← buildDeps pkg
|
||||
if makeArgs != [] || (← FilePath.pathExists "Makefile") then
|
||||
execMake manifest makeArgs cfg
|
||||
execMake pkg deps makeArgs leanArgs
|
||||
else
|
||||
buildModules manifest cfg [manifest.module]
|
||||
buildModules (mkBuildConfig pkg deps leanArgs) [pkg.module]
|
||||
|
|
|
|||
|
|
@ -1,31 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2021 Sebastian Ullrich. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Ullrich, Mac Malone
|
||||
-/
|
||||
import Lean.Data.Name
|
||||
import Lean.Elab.Import
|
||||
import Leanpkg2.Package
|
||||
import Leanpkg2.Proc
|
||||
|
||||
open Lean System
|
||||
|
||||
namespace Leanpkg2
|
||||
|
||||
structure BuildConfig where
|
||||
module : Name
|
||||
leanArgs : List String
|
||||
leanPath : String
|
||||
-- things like `leanpkg.toml` and olean roots of dependencies that should also trigger rebuilds
|
||||
moreDeps : List FilePath
|
||||
|
||||
namespace 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")
|
||||
}
|
||||
|
|
@ -5,7 +5,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
|
|||
-/
|
||||
import Leanpkg2.Init
|
||||
import Leanpkg2.Build
|
||||
import Leanpkg2.TomlManifest
|
||||
import Leanpkg2.TomlConfig
|
||||
|
||||
namespace Leanpkg2
|
||||
|
||||
|
|
@ -61,11 +61,18 @@ Usage:
|
|||
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
|
||||
if cfg.leanVersion ≠ leanVersionString then
|
||||
IO.eprintln $ "\nWARNING: Lean version mismatch: installed version is " ++
|
||||
leanVersionString ++ ", but package requires " ++ cfg.leanVersion ++ "\n"
|
||||
return ⟨".", cfg⟩
|
||||
|
||||
def cli : (cmd : String) → (leanpkgArgs leanArgs : List String) → IO Unit
|
||||
| "init", [name], [] => init name
|
||||
| "configure", [], [] => do configure (← readManifest)
|
||||
| "print-paths", imports, leanArgs => do printPaths (← readManifest) imports leanArgs
|
||||
| "build", makeArgs, leanArgs => do build (← readManifest) makeArgs leanArgs
|
||||
| "configure", [], [] => do configure (← getRootPkg)
|
||||
| "print-paths", imports, leanArgs => do printPaths (← getRootPkg) imports leanArgs
|
||||
| "build", makeArgs, leanArgs => do build (← getRootPkg) makeArgs leanArgs
|
||||
| "help", ["init"], [] => IO.println helpInit
|
||||
| "help", ["configure"], [] => IO.println helpConfigure
|
||||
| "help", ["build"], [] => IO.println helpBuild
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
|
|||
-/
|
||||
import Leanpkg2.Git
|
||||
import Leanpkg2.Proc
|
||||
import Leanpkg2.TomlManifest
|
||||
import Leanpkg2.TomlConfig
|
||||
|
||||
namespace Leanpkg2
|
||||
|
||||
|
|
|
|||
|
|
@ -3,50 +3,58 @@ 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 Leanpkg2.Proc
|
||||
import Leanpkg2.Package
|
||||
import Leanpkg2.BuildConfig
|
||||
|
||||
open System
|
||||
|
||||
namespace Leanpkg2
|
||||
|
||||
def lockFileName : FilePath := ".leanpkg-lock"
|
||||
def lockfile : FilePath := ".leanpkg-lock"
|
||||
|
||||
partial def withLockFile (x : IO α) : IO α := do
|
||||
acquire
|
||||
try
|
||||
x
|
||||
finally
|
||||
IO.removeFile lockFileName
|
||||
IO.removeFile lockfile
|
||||
where
|
||||
acquire (firstTime := true) :=
|
||||
try
|
||||
-- TODO: lock file should ideally contain PID
|
||||
if !Platform.isWindows then
|
||||
discard <| IO.Prim.Handle.mk lockFileName "wx"
|
||||
discard <| IO.Prim.Handle.mk lockfile "wx"
|
||||
else
|
||||
-- `x` mode doesn't seem to work on Windows even though it's listed at
|
||||
-- https://docs.microsoft.com/en-us/cpp/c-runtime-library/reference/fopen-wfopen?view=msvc-160
|
||||
-- ...? Let's use the slightly racy approach then.
|
||||
if ← lockFileName.pathExists then
|
||||
if ← lockfile.pathExists then
|
||||
throw <| IO.Error.alreadyExists 0 ""
|
||||
discard <| IO.Prim.Handle.mk lockFileName "w"
|
||||
discard <| IO.Prim.Handle.mk lockfile "w"
|
||||
catch
|
||||
| IO.Error.alreadyExists _ _ => do
|
||||
if firstTime then
|
||||
IO.eprintln s!"Waiting for prior leanpkg invocation to finish... (remove '{lockFileName}' if stuck)"
|
||||
IO.eprintln s!"Waiting for prior leanpkg invocation to finish... (remove '{lockfile}' if stuck)"
|
||||
IO.sleep (ms := 300)
|
||||
acquire (firstTime := false)
|
||||
| e => throw e
|
||||
|
||||
def execMake (manifest : Manifest) (makeArgs : List String) (cfg : BuildConfig) : IO Unit := withLockFile do
|
||||
def execMake
|
||||
(pkg : Package) (deps : List Package) (makeArgs leanArgs : List String := [])
|
||||
: IO Unit := withLockFile do
|
||||
let timeoutArgs :=
|
||||
match manifest.timeout with
|
||||
match pkg.timeout with
|
||||
| some t => ["-T", toString t]
|
||||
| none => []
|
||||
let leanArgs := timeoutArgs ++ cfg.leanArgs
|
||||
let leanmake := (← IO.appDir) / "leanmake"
|
||||
let leanOptsStr := " ".intercalate <| timeoutArgs ++ leanArgs
|
||||
let leanPathStr := SearchPath.toString <| deps.map (·.buildDir)
|
||||
let makeArgsStr := " ".intercalate makeArgs
|
||||
let moreDepsStr := " ".intercalate $
|
||||
deps.filter (·.dir.toString != pkg.dir) |>.map (·.oleanRoot.toString)
|
||||
let mut spawnArgs := {
|
||||
cmd := "sh"
|
||||
args := #["-c", s!"\"{← IO.appDir}/leanmake\" PKG={cfg.module} LEAN_OPTS=\"{" ".intercalate leanArgs}\" LEAN_PATH=\"{cfg.leanPath}\" {" ".intercalate makeArgs} MORE_DEPS+=\"{" ".intercalate (cfg.moreDeps.map toString)}\" >&2"]
|
||||
cwd := pkg.dir
|
||||
args := #["-c", s!"\"{leanmake}\" PKG={pkg.module} LEAN_OPTS=\"{leanOptsStr}\" LEAN_PATH=\"{leanPathStr}\" {makeArgsStr} MORE_DEPS+=\"{moreDepsStr}\" >&2"]
|
||||
}
|
||||
execCmd spawnArgs
|
||||
|
|
|
|||
|
|
@ -22,38 +22,47 @@ structure Dependency where
|
|||
name : String
|
||||
src : Source
|
||||
|
||||
structure Manifest where
|
||||
structure PackageConfig where
|
||||
name : String
|
||||
version : String
|
||||
leanVersion : String := leanVersionString
|
||||
timeout : Option Nat := none
|
||||
module : String := name.capitalize
|
||||
module : Name := name.capitalize
|
||||
dependencies : List Dependency := []
|
||||
deriving Inhabited
|
||||
|
||||
structure Package where
|
||||
dir : FilePath
|
||||
manifest : Manifest
|
||||
config : PackageConfig
|
||||
deriving Inhabited
|
||||
|
||||
namespace Package
|
||||
|
||||
def name (self : Package) : String :=
|
||||
self.manifest.name
|
||||
def name (self : Package) :=
|
||||
self.config.name
|
||||
|
||||
def dependencies (self : Package) : List Dependency :=
|
||||
self.manifest.dependencies
|
||||
def module (self : Package) :=
|
||||
self.config.module
|
||||
|
||||
def sourceDir (self : Package) : FilePath :=
|
||||
def dependencies (self : Package) :=
|
||||
self.config.dependencies
|
||||
|
||||
def timeout (self : Package) :=
|
||||
self.config.timeout
|
||||
|
||||
def sourceDir (self : Package) :=
|
||||
self.dir
|
||||
|
||||
def sourceRoot (self : Package) : FilePath :=
|
||||
self.sourceDir / self.manifest.module
|
||||
def sourceRoot (self : Package) :=
|
||||
self.sourceDir / self.config.module.toString
|
||||
|
||||
def buildDir (self : Package) : FilePath :=
|
||||
def buildDir (self : Package) :=
|
||||
self.dir / Leanpkg2.buildPath
|
||||
|
||||
def buildRoot (self : Package) : FilePath :=
|
||||
self.buildDir / self.manifest.module
|
||||
def buildRoot (self : Package) :=
|
||||
self.buildDir / self.config.module.toString
|
||||
|
||||
def oleanRoot (self : Package) :=
|
||||
self.buildRoot.withExtension "olean"
|
||||
|
||||
end Package
|
||||
|
|
|
|||
|
|
@ -4,9 +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.Proc
|
||||
import Leanpkg2.TomlManifest
|
||||
import Leanpkg2.BuildConfig
|
||||
import Leanpkg2.TomlConfig
|
||||
|
||||
open System
|
||||
|
||||
|
|
@ -28,14 +26,14 @@ def materializeGit
|
|||
let hash ← parseOriginRevision rev dir
|
||||
checkoutDetach hash dir
|
||||
|
||||
def materialize (relPath : FilePath) (dep : Dependency) : IO FilePath :=
|
||||
def materialize (pkgDir : FilePath) (dep : Dependency) : IO FilePath :=
|
||||
match dep.src with
|
||||
| Source.path dir => do
|
||||
let depdir := relPath / dir
|
||||
let depdir := pkgDir / dir
|
||||
IO.eprintln s!"{dep.name}: using local path {depdir}"
|
||||
depdir
|
||||
| Source.git url rev branch => do
|
||||
let depdir := depsPath / dep.name
|
||||
let depdir := pkgDir / depsPath / dep.name
|
||||
materializeGit dep.name depdir url rev branch
|
||||
depdir
|
||||
|
||||
|
|
@ -65,23 +63,29 @@ def resolvedPackage (d : String) : Solver Package := do
|
|||
let some pkg ← pure ((← get).lookup d) | unreachable!
|
||||
pkg
|
||||
|
||||
def solveDepsCore
|
||||
(pkgName : String) (relPath : FilePath) (deps : List Dependency)
|
||||
: (maxDepth : Nat) → Solver Unit
|
||||
def solveDepsCore (pkg : Package) : (maxDepth : Nat) → Solver Unit
|
||||
| 0 => throw <| IO.userError "maximum dependency resolution depth reached"
|
||||
| maxDepth + 1 => do
|
||||
let newDeps ← deps.filterM (notYetAssigned ·.name)
|
||||
let newDeps ← pkg.dependencies.filterM (notYetAssigned ·.name)
|
||||
for dep in newDeps do
|
||||
let dir ← materialize relPath dep
|
||||
let m ← Manifest.fromTomlFile <| dir / leanpkgToml
|
||||
modify (·.insert dep.name ⟨dir, m⟩)
|
||||
let dir ← materialize pkg.dir dep
|
||||
let cfg ← PackageConfig.fromTomlFile <| dir / leanpkgToml
|
||||
modify (·.insert dep.name ⟨dir, cfg⟩)
|
||||
for dep in newDeps do
|
||||
let depPkg ← resolvedPackage dep.name
|
||||
unless depPkg.name = dep.name do
|
||||
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
|
||||
throw <| IO.userError <|
|
||||
s!"{pkg.name} (in {pkg.dir}) depends on {dep.name}, " ++
|
||||
s!"but resolved dependency has name {depPkg.name} (in {depPkg.dir})"
|
||||
solveDepsCore depPkg maxDepth
|
||||
|
||||
def solveDeps (m : Manifest) : IO (List Package) := do
|
||||
let solver := solveDepsCore m.name ⟨"."⟩ m.dependencies 1024
|
||||
let (_, assg) ← solver.run (Assignment.empty.insert m.name ⟨".", m⟩)
|
||||
/--
|
||||
Resolves the dependency tree for the given package,
|
||||
downloading and/or updating missing dependencies as necessary.
|
||||
|
||||
Note that resulting list of dependencies *will* include the given package.
|
||||
-/
|
||||
def solveDeps (pkg : Package) : IO (List Package) := do
|
||||
let solver := solveDepsCore pkg 1024
|
||||
let (_, assg) ← solver.run (Assignment.empty.insert pkg.name ⟨pkg.dir, pkg.config⟩)
|
||||
assg.reverse.mapM (·.2)
|
||||
|
|
|
|||
|
|
@ -11,6 +11,8 @@ open System
|
|||
|
||||
namespace Leanpkg2
|
||||
|
||||
def leanpkgToml : FilePath := "leanpkg.toml"
|
||||
|
||||
namespace Source
|
||||
|
||||
def fromToml? (v : Toml.Value) : Option Source :=
|
||||
|
|
@ -32,9 +34,9 @@ def toToml : Source → Toml.Value
|
|||
|
||||
end Source
|
||||
|
||||
namespace Manifest
|
||||
namespace PackageConfig
|
||||
|
||||
def fromToml? (t : Toml.Value) : Option Manifest := OptionM.run do
|
||||
def fromToml? (t : Toml.Value) : Option PackageConfig := OptionM.run do
|
||||
let pkg ← t.lookup "package"
|
||||
let Toml.Value.str name ← pkg.lookup "name" | none
|
||||
let Toml.Value.str version ← pkg.lookup "version" | none
|
||||
|
|
@ -54,24 +56,15 @@ def fromToml? (t : Toml.Value) : Option Manifest := OptionM.run do
|
|||
let dependencies ← deps.mapM fun ⟨n, src⟩ => do Dependency.mk n (← Source.fromToml? src)
|
||||
return { name, module, version, leanVersion, dependencies, timeout }
|
||||
|
||||
def fromTomlString? (str : String) : IO (Option Manifest) := do
|
||||
def fromTomlString? (str : String) : IO (Option PackageConfig) := do
|
||||
fromToml? (← Toml.parse str)
|
||||
|
||||
def fromTomlFile? (path : FilePath) : IO (Option Manifest) := do
|
||||
def fromTomlFile? (path : FilePath) : IO (Option PackageConfig) := do
|
||||
fromTomlString? (← IO.FS.readFile path)
|
||||
|
||||
def fromTomlFile (path : FilePath) : IO Manifest := do
|
||||
let some manifest ← fromTomlFile? path
|
||||
| throw <| IO.userError s!"manifest (at {path}) is ill-formed"
|
||||
manifest
|
||||
def fromTomlFile (path : FilePath) : IO PackageConfig := do
|
||||
let some config ← fromTomlFile? path
|
||||
| throw <| IO.userError s!"configuration (at {path}) is ill-formed"
|
||||
config
|
||||
|
||||
end Manifest
|
||||
|
||||
def leanpkgToml : FilePath := "leanpkg.toml"
|
||||
|
||||
def readManifest : IO Manifest := do
|
||||
let m ← Manifest.fromTomlFile leanpkgToml
|
||||
if m.leanVersion ≠ leanVersionString then
|
||||
IO.eprintln $ "\nWARNING: Lean version mismatch: installed version is " ++ leanVersionString
|
||||
++ ", but package requires " ++ m.leanVersion ++ "\n"
|
||||
return m
|
||||
end PackageConfig
|
||||
|
|
@ -2,16 +2,16 @@ import Leanpkg2.Build
|
|||
|
||||
open Leanpkg2
|
||||
|
||||
def manifest : Manifest := {
|
||||
def package : PackageConfig := {
|
||||
name := "hello",
|
||||
version := "1.0",
|
||||
}
|
||||
|
||||
def configure : IO Unit :=
|
||||
Leanpkg2.configure manifest
|
||||
Leanpkg2.configure ⟨".", package⟩
|
||||
|
||||
def build : IO Unit :=
|
||||
Leanpkg2.build manifest ["bin"]
|
||||
Leanpkg2.build ⟨".", package⟩ ["bin"]
|
||||
|
||||
def main : IO Unit :=
|
||||
build
|
||||
|
|
|
|||
|
|
@ -2,16 +2,16 @@ import Leanpkg2.Build
|
|||
|
||||
open Leanpkg2
|
||||
|
||||
def manifest : Manifest := {
|
||||
def package : PackageConfig := {
|
||||
name := "hello",
|
||||
version := "1.0",
|
||||
}
|
||||
|
||||
def configure : IO Unit :=
|
||||
Leanpkg2.configure manifest
|
||||
Leanpkg2.configure ⟨".", package⟩
|
||||
|
||||
def build : IO Unit :=
|
||||
Leanpkg2.build manifest ["bin"]
|
||||
Leanpkg2.build ⟨".", package⟩ ["bin"]
|
||||
|
||||
def main : IO Unit :=
|
||||
build
|
||||
|
|
|
|||
|
|
@ -2,13 +2,13 @@ import Leanpkg2.Build
|
|||
|
||||
open Leanpkg2
|
||||
|
||||
def manifest : Manifest := {
|
||||
def package : PackageConfig := {
|
||||
name := "a",
|
||||
version := "1.0",
|
||||
}
|
||||
|
||||
def build : IO Unit :=
|
||||
Leanpkg2.build manifest ["lib"]
|
||||
Leanpkg2.build ⟨".", package⟩ ["lib"]
|
||||
|
||||
def main : IO Unit :=
|
||||
build
|
||||
|
|
|
|||
|
|
@ -2,13 +2,13 @@ import Leanpkg2.Build
|
|||
|
||||
open Leanpkg2
|
||||
|
||||
def manifest : Manifest := {
|
||||
def package : PackageConfig := {
|
||||
name := "a",
|
||||
version := "1.0",
|
||||
}
|
||||
|
||||
def build : IO Unit :=
|
||||
Leanpkg2.build manifest ["lib"]
|
||||
Leanpkg2.build ⟨".", package⟩ ["lib"]
|
||||
|
||||
def main : IO Unit :=
|
||||
build
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@ import Leanpkg2.Build
|
|||
|
||||
open Leanpkg2 System
|
||||
|
||||
def manifest : Manifest := {
|
||||
def package : PackageConfig := {
|
||||
name := "b",
|
||||
version := "1.0",
|
||||
dependencies := [
|
||||
|
|
@ -11,7 +11,7 @@ def manifest : Manifest := {
|
|||
}
|
||||
|
||||
def build : IO Unit := do
|
||||
Leanpkg2.build manifest ["bin", "LINK_OPTS=../a/build/lib/libA.a"]
|
||||
Leanpkg2.build ⟨".", package⟩ ["bin", "LINK_OPTS=../a/build/lib/libA.a"]
|
||||
|
||||
def main : IO Unit :=
|
||||
build
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@ import Leanpkg2.Build
|
|||
|
||||
open Leanpkg2 System
|
||||
|
||||
def manifest : Manifest := {
|
||||
def package : PackageConfig := {
|
||||
name := "b",
|
||||
version := "1.0",
|
||||
dependencies := [
|
||||
|
|
@ -11,7 +11,7 @@ def manifest : Manifest := {
|
|||
}
|
||||
|
||||
def build : IO Unit := do
|
||||
Leanpkg2.build manifest ["bin", "LINK_OPTS=../a/build/lib/libA.a"]
|
||||
Leanpkg2.build ⟨".", package⟩ ["bin", "LINK_OPTS=../a/build/lib/libA.a"]
|
||||
|
||||
def main : IO Unit :=
|
||||
build
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue