feat: basic port of leanpkg

nix/bootstrap.nix

@@ -1,5 +1,5 @@
 { debug ? false, extraCMakeFlags ? [],
-  stdenv, lib, cmake, gmp, buildLeanPackage, writeShellScriptBin, runCommand,
+  stdenv, lib, cmake, gmp, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin,
   ... } @ args:
 rec {
   inherit stdenv;
@@ -17,7 +17,7 @@ rec {
   } // args // {
     src = args.realSrc or (lib.sourceByRegex args.src [ "[a-z].*" "CMakeLists\.txt" ]);
   });
-  leanc = buildCMake {
+  leanc-unwrapped = buildCMake {
     name = "leanc";
     src = ../src;
     dontBuild = true;
@@ -61,6 +61,7 @@ rec {
       desc = "stage${toString stage}";
       build = args: buildLeanPackage.override {
         lean = prevStage;
+        leanc = leanc-unwrapped;
         # use same stage for retrieving dependencies
         lean-leanDeps = stage0;
         lean-final = self;
@@ -72,18 +73,25 @@ rec {
       Init = build { name = "Init"; src = ../src; deps = []; };
       Std  = build { name = "Std";  src = ../src; deps = [ Init ]; };
       Lean = build { name = "Lean"; src = ../src; deps = [ Init Std ]; };
+      Leanpkg = build { name = "Leanpkg"; src = ../src; deps = [ Init Std Lean ]; };
       inherit (Lean) emacs-dev emacs-package;
       mods = Init.mods // Std.mods // Lean.mods;
+      leanc = writeShellScriptBin "leanc" ''
+        ${leanc-unwrapped}/bin/leanc -L${gmp}/lib -L${Init.staticLib} -L${Std.staticLib} -L${Lean.staticLib} -L${leancpp}/lib/lean "$@"
+      '';
       lean = wrapStage(stdenv.mkDerivation {
         name = "lean-${desc}";
         buildCommand = ''
           mkdir -p $out/bin $out/lib/lean
-          ln -sf ${leancpp}/lib/lean/* ${Init.staticLib}/* ${Init.modRoot}/* ${Lean.staticLib}/* ${Lean.modRoot}/* ${Std.staticLib}/* ${Std.modRoot}/* $out/lib/lean/
-          ${leanc}/bin/leanc -x none -rdynamic -L${gmp}/lib -L$out/lib/lean -L${leancpp}/lib/lean -o $out/bin/lean
+          ln -sf ${leancpp}/lib/lean/* ${Leanpkg.modRoot}/* ${Lean.staticLib}/* ${Lean.modRoot}/* ${Std.staticLib}/* ${Std.modRoot}/* ${Init.staticLib}/* ${Init.modRoot}/* $out/lib/lean/
+          ${leanc}/bin/leanc -x none -rdynamic -o $out/bin/lean
+          ${leanc}/bin/leanc -x none -rdynamic ${Leanpkg.staticLib}/* -o $out/bin/leanpkg
           ln -s ${leanc}/bin/leanc $out/bin/
           ln -s ${leanc}/include $out/
         '';
       });
+      leanpkg = Leanpkg.executable "leanpkg";
+      # lean = symlinkJoin { name = "lean"; paths = [ leanWithoutLeanpkg leanpkg ]; };
       test = buildCMake {
         name = "lean-test-${desc}";
         realSrc = lib.sourceByRegex ../. [ "src.*" "tests.*" ];

nix/buildLeanPackage.nix

@@ -126,6 +126,10 @@ in rec {
     mkdir $out
     ar Trcs $out/lib${name}.a ${lib.concatStringsSep " " (map (drv: "${drv}/${drv.oPath}") (attrValues objects))}
   '';
+  executable = name: runCommand name {} ''
+    mkdir -p $out/bin
+    ${leanc}/bin/leanc -x none -L${staticLib} -o $out/bin/${name}
+  '';
 
   lean-package = writeShellScriptBin "lean" ''
     LEAN_PATH=${modRoot}:$LEAN_PATH ${lean-final}/bin/lean $@

nix/packages.nix

@@ -81,7 +81,7 @@ let
 in {
   inherit cc lean4-mode buildLeanPackage llvmPackages;
   lean = lean.stage1;
-  stage0check-mod = (lean.stage1.Lean.overrideArgs { lean-final = lean.stage0; }).check-mod;
+  stage0check-mod = (lean.stage1.Leanpkg.overrideArgs { lean-final = lean.stage0; }).check-mod;
   HEAD-as-stage0 = (lean.stage1.Lean.overrideArgs { srcCheckTarget = "$root#stage0-from-input.stage0check-mod"; srcCheckArgs = "(--override-input lean-stage0 $root\?rev=$(git rev-parse HEAD) -- -Dinterpreter.prefer_native=false \"$@\")"; });
   HEAD-as-stage1 = (lean.stage1.Lean.overrideArgs { srcCheckTarget = "$root\?rev=$(git rev-parse HEAD)#stage0check-mod"; });
   temci = (import temci {}).override { doCheck = false; };

src/Leanpkg.lean

@@ -0,0 +1,135 @@
+/-
+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
+-/
+import Leanpkg.Resolve
+import Leanpkg.Git
+
+namespace Leanpkg
+
+def readManifest : IO Manifest := do
+  let m ← Manifest.fromFile leanpkgTomlFn
+  if m.leanVersion ≠ leanVersionString then
+    IO.eprintln $ "\nWARNING: Lean version mismatch: installed version is " ++ leanVersionString
+       ++ ", but package requires " ++ m.leanVersion ++ "\n"
+  return m
+
+def writeManifest (manifest : Lean.Syntax) (fn : String) : IO Unit := do
+  IO.FS.writeFile fn manifest.reprint.get!
+
+def configure : IO String := do
+  let d ← readManifest
+  IO.eprintln $ "configuring " ++ d.name ++ " " ++ d.version
+  let assg ← solveDeps d
+  let paths ← constructPath assg
+  for path in paths do
+    unless path == "./." do
+      -- TODO: share build of common dependencies
+      execCmd {
+        cmd := "leanpkg"
+        cwd := path
+        args := #["build"]
+      }
+  System.FilePath.searchPathSeparator.toString.intercalate <| paths.map (· ++ "/build")
+
+def build (leanArgs : List String) : IO Unit := do
+  let manifest ← readManifest
+  let path ← configure
+  let leanArgs := (match manifest.timeout with | some t => ["-T", toString t] | none => []) ++ leanArgs
+  execCmd {
+    cmd := "leanmake"
+    cwd := manifest.effectivePath
+    args := #[s!"LEAN_OPTS={" ".intercalate leanArgs}", s!"LEAN_PATH={path}"]
+  }
+
+def initGitignoreContents :=
+  "/build
+"
+
+def initPkg (n : String) (fromNew : Bool) : IO Unit := do
+  IO.FS.writeFile leanpkgTomlFn s!"[package]
+name = \"{n}\"
+version = \"0.1\"
+"
+  IO.FS.writeFile s!"{n.capitalize}.lean" "def main : IO Unit :=
+  IO.println \"Hello, world!\"
+"
+  let h ← IO.FS.Handle.mk ".gitignore" IO.FS.Mode.append (bin := false)
+  h.putStr initGitignoreContents
+  let gitEx ← IO.isDir ".git"
+  unless gitEx do
+    (do
+      execCmd {cmd := "git", args := #["init", "-q"]}
+      unless upstreamGitBranch = "master" do
+        execCmd {cmd := "git", args := #["checkout", "-B", upstreamGitBranch]}
+    ) <|> IO.println "WARNING: failed to initialize git repository"
+
+def init (n : String) := initPkg n false
+
+def usage :=
+  "Lean package manager, version " ++ uiLeanVersionString ++ "
+
+Usage: leanpkg <command>
+
+configure              download dependencies
+build [-- <Lean-args>] download dependencies and build *.olean files
+init <name>            create a Lean package in the current directory
+
+See `leanpkg help <command>` for more information on a specific command."
+
+def main : (cmd : String) → (leanpkgArgs leanArgs : List String) → IO Unit
+  | "configure", [],     []        => discard <| configure
+  | "build",     _,      leanArgs  => build leanArgs
+  | "init",      [Name], []        => init Name
+  | "help",      ["configure"], [] => IO.println "Download dependencies
+
+Usage:
+  leanpkg configure
+
+This command sets up the `build/deps` directory.
+
+For each (transitive) git dependency, the specified commit is checked out
+into a sub-directory of `build/deps`. If there are dependencies on multiple
+versions of the same package, the version materialized is undefined. No copy
+is made of local dependencies."
+  | "help",       ["build"], []    => IO.println "download dependencies and build *.olean files
+
+Usage:
+  leanpkg build [-- <lean-args>]
+
+This command invokes `Leanpkg configure` followed by
+`Leanmake <lean-args>`, building the package's Lean files as well as
+(transitively) imported files of dependencies. If defined, the `package.timeout`
+configuration value is passed to Lean via its `-T` parameter."
+  | "help",       ["init"], []     => IO.println "Create a new Lean package in the current directory
+
+Usage:
+  leanpkg init <name>
+
+This command creates a new Lean package with the given name in the current
+directory."
+  | "help",       _,     []        => IO.println usage
+  | _,            _,     _         => throw <| IO.userError usage
+
+private def splitCmdlineArgsCore : List String → List String × List String
+  | []           => ([], [])
+  | (arg::args)  => if arg == "--"
+                    then ([], args)
+                    else
+                      let (outerArgs, innerArgs) := splitCmdlineArgsCore args
+                      (arg::outerArgs, innerArgs)
+
+def splitCmdlineArgs : List String → IO (String × List String × List String)
+| [] => throw <| IO.userError usage
+| [cmd] => return (cmd, [], [])
+| (cmd::rest) =>
+  let (outerArgs, innerArgs) := splitCmdlineArgsCore rest
+  return (cmd, outerArgs, innerArgs)
+
+end Leanpkg
+
+def main (args : List String) : IO Unit := do
+  Lean.initSearchPath none  -- HACK
+  let (cmd, outerArgs, innerArgs) ← Leanpkg.splitCmdlineArgs args
+  Leanpkg.main cmd outerArgs innerArgs

src/Leanpkg/.gitignore

@@ -0,0 +1 @@
+/leanpkg/config_vars.lean

src/Leanpkg/Git.lean

@@ -0,0 +1,41 @@
+/-
+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
+-/
+import Leanpkg.LeanVersion
+
+namespace Leanpkg
+
+def upstreamGitBranch :=
+  if Lean.version.isRelease then
+    "Lean-" ++ leanVersionStringCore
+  else
+    "master"
+
+def gitdefaultRevision : Option String → String
+  | none => upstreamGitBranch
+  | some branch => branch
+
+def gitParseRevision (gitRepoDir : String) (rev : String) : IO String := do
+  let rev ← IO.Process.run {cmd := "git", args := #["rev-parse", "-q", "--verify", rev], cwd := gitRepoDir}
+  rev.trim -- remove newline at end
+
+def gitHeadRevision (gitRepoDir : String) : IO String :=
+  gitParseRevision gitRepoDir "HEAD"
+
+def gitParseOriginRevision (gitRepoDir : String) (rev : String) : IO String :=
+  (gitParseRevision gitRepoDir $ "origin/" ++ rev) <|> gitParseRevision gitRepoDir rev
+    <|> throw (IO.userError s!"cannot find revision {rev} in repository {gitRepoDir}")
+
+def gitLatestOriginRevision (gitRepoDir : String) (branch : Option String) : IO String := do
+  discard <| IO.Process.run {cmd := "git", args := #["fetch"], cwd := gitRepoDir}
+  gitParseOriginRevision gitRepoDir (gitdefaultRevision branch)
+
+def gitRevisionExists (gitRepoDir : String) (rev : String) : IO Bool := do
+  try
+    discard <| gitParseRevision gitRepoDir (rev ++ "^{commit}")
+    true
+  catch _ => false
+
+end Leanpkg

src/Leanpkg/LeanVersion.lean

@@ -0,0 +1,27 @@
+/-
+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
+-/
+namespace Leanpkg
+
+def leanVersionStringCore :=
+  s!"{Lean.version.major}.{Lean.version.minor}.{Lean.version.patch}"
+
+def leanVersionString :=
+  if Lean.version.isRelease then
+      s!"leanprover/lean:{leanVersionStringCore}"
+  else if Lean.version.specialDesc ≠ "" then
+      Lean.version.specialDesc
+  else
+      "master"
+
+def uiLeanVersionString :=
+if Lean.version.isRelease then
+    leanVersionStringCore
+else if Lean.version.specialDesc ≠ "" then
+    Lean.version.specialDesc
+else
+    s!"master ({leanVersionStringCore})"
+
+end Leanpkg

src/Leanpkg/Manifest.lean

@@ -0,0 +1,85 @@
+/-
+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
+-/
+import Leanpkg.Toml
+import Leanpkg.LeanVersion
+
+namespace Leanpkg
+
+inductive Source where
+  | path (dirName : String) : Source
+  | git (url rev : String) (branch : Option String) : Source
+
+namespace Source
+
+def fromToml (v : Toml.Value) : Option Source :=
+  (do let Toml.Value.str dirName ← v.lookup "path" | none
+      path dirName) <|>
+  (do let Toml.Value.str url ← v.lookup "git" | none
+      let Toml.Value.str rev ← v.lookup "rev" | none
+      match v.lookup "branch" with
+      | none                         => git url rev none
+      | some (Toml.Value.str branch) => git url rev (some branch)
+      | _ => none)
+
+def toToml : Source → Toml.Value
+  | path dirName => Toml.Value.table [("path", Toml.Value.str dirName)]
+  | git url rev none =>
+    Toml.Value.table [("git", Toml.Value.str url), ("rev", Toml.Value.str rev)]
+  | git url rev (some branch) =>
+    Toml.Value.table [("git", Toml.Value.str url), ("branch", Toml.Value.str branch), ("rev", Toml.Value.str rev)]
+
+end Source
+
+structure Dependency where
+  name : String
+  src : Source
+
+structure Manifest where
+  name : String
+  version : String
+  leanVersion : String := leanVersionString
+  timeout : Option Nat := none
+  path : Option String := none
+  dependencies : List Dependency := []
+
+namespace Manifest
+
+def effectivePath (m : Manifest) : String :=
+  m.path.getD "."
+
+def fromToml (t : Toml.Value) : Option Manifest := do
+  let pkg ← t.lookup "package"
+  let Toml.Value.str n ← pkg.lookup "name" | none
+  let Toml.Value.str ver ← pkg.lookup "version" | none
+  let leanVer ← match pkg.lookup "lean_version" with
+    | some (Toml.Value.str leanVer) => some leanVer
+    | none => some leanVersionString
+    | _ => none
+  let tm ← match pkg.lookup "timeout" with
+    | some (Toml.Value.nat timeout) => some (some timeout)
+    | none => some none
+    | _ => none
+  let path ← match pkg.lookup "path" with
+    | some (Toml.Value.str path) => some (some path)
+    | none => some none
+    | _ => none
+  let Toml.Value.table deps ← t.lookup "dependencies" <|> some (Toml.Value.table []) | none
+  let deps ← deps.mapM fun ⟨n, src⟩ => do Dependency.mk n (← Source.fromToml src)
+  return { name := n, version := ver, leanVersion := leanVer,
+           path := path, dependencies := deps, timeout := tm }
+
+def fromFile (fn : String) : IO Manifest := do
+  let cnts ← IO.FS.readFile fn
+  let toml ← Toml.parse cnts
+  let some manifest ← pure (fromToml toml)
+    | throw <| IO.userError s!"cannot read manifest from {fn}"
+  manifest
+
+end Manifest
+
+def leanpkgTomlFn := "leanpkg.toml"
+
+end Leanpkg

src/Leanpkg/Proc.lean

@@ -0,0 +1,20 @@
+/-
+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
+-/
+namespace Leanpkg
+
+def execCmd (args : IO.Process.SpawnArgs) : IO Unit := do
+  let envstr := String.join <| args.env.toList.map fun (k, v) => s!"{k}={v.getD ""} "
+  let cmdstr := " ".intercalate (args.cmd :: args.args.toList)
+  IO.println <| "> " ++ envstr ++
+    match args.cwd with
+    | some cwd => cmdstr ++ "    # in directory " ++ cwd
+    | none     => cmdstr
+  let child ← IO.Process.spawn args
+  let exitCode ← child.wait
+  if exitCode != 0 then
+    throw <| IO.userError <| s!"external command exited with status {exitCode}"
+
+end Leanpkg

src/Leanpkg/Resolve.lean

@@ -0,0 +1,91 @@
+/-
+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
+-/
+import Leanpkg.Manifest
+import Leanpkg.Proc
+import Leanpkg.Git
+
+namespace Leanpkg
+
+def Assignment := List (String × String)
+
+namespace Assignment
+def empty : Assignment := []
+
+def contains (a : Assignment) (s : String) : Bool :=
+  (a.lookup s).isSome
+
+def insert (a : Assignment) (k v : String) : Assignment :=
+  if a.contains k then a else (k, v) :: a
+
+def fold {α} (i : α) (f : α → String → String → α) : Assignment → α :=
+  List.foldl (fun a ⟨k, v⟩ => f a k v) i
+
+end Assignment
+
+abbrev Solver := StateT Assignment IO
+
+def notYetAssigned (d : String) : Solver Bool := do
+  ¬ (← get).contains d
+
+def resolvedPath (d : String) : Solver String := do
+  let some path ← pure ((← get).lookup d) | unreachable!
+  path
+
+-- TODO(gabriel): windows?
+def resolveDir (absOrRel : String) (base : String) : String :=
+  if absOrRel.front = '/' then
+    absOrRel -- absolute
+  else
+    base ++ "/" ++ absOrRel
+
+def materialize (relpath : String) (dep : Dependency) : Solver Unit :=
+  match dep.src with
+  | Source.path dir => do
+    let depdir := resolveDir dir relpath
+    IO.println s!"{dep.name}: using local path {depdir}"
+    modify (·.insert dep.name depdir)
+  | Source.git url rev branch => do
+    let depdir := "build/deps/" ++ dep.name
+    let alreadyThere ← IO.isDir depdir
+    if alreadyThere then
+      IO.print s!"{dep.name}: trying to update {depdir} to revision {rev}"
+      IO.println (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.println s!"{dep.name}: cloning {url} to {depdir}"
+      execCmd {cmd := "git", args := #["clone", url, depdir]}
+    let hash ← gitParseOriginRevision depdir rev
+    execCmd {cmd := "git", args := #["checkout", "--detach", hash], cwd := depdir}
+    modify (·.insert dep.name depdir)
+
+def solveDepsCore (relPath : String) (d : Manifest) : (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.fromFile $ p ++ "/" ++ "leanpkg.toml"
+      unless d'.name = dep.name do
+        throw <| IO.userError <| d.name ++ " (in " ++ relPath ++ ") depends on " ++ d'.name ++
+          ", but resolved dependency has name " ++ dep.name ++ " (in " ++ p ++ ")"
+      solveDepsCore p d' maxDepth
+
+def solveDeps (d : Manifest) : IO Assignment := do
+  let (_, assg) ← (solveDepsCore "." d 1024).run <| Assignment.empty.insert d.name "."
+  assg
+
+def constructPathCore (depname : String) (dirname : String) : IO String := do
+  let path ← Manifest.effectivePath (← Manifest.fromFile $ dirname ++ "/" ++ leanpkgTomlFn)
+  return dirname ++ "/" ++ path
+
+def constructPath (assg : Assignment) : IO (List String) := do
+  assg.reverse.mapM fun ⟨depname, dirname⟩ => constructPathCore depname dirname
+
+end Leanpkg

src/Leanpkg/Toml.lean

@@ -0,0 +1,72 @@
+/-
+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
+-/
+import Lean.Parser
+
+namespace Toml
+
+inductive Value : Type where
+  | str : String → Value
+  | nat : Nat → Value
+  | bool : Bool → Value
+  | table : List (String × Value) → Value
+  deriving Inhabited
+
+def Value.lookup : Value → String → Option Value
+  | Value.table cs, k => cs.lookup k
+  | _, _ => none
+
+-- TODO: custom whitespace and other inaccuracies
+declare_syntax_cat val
+syntax "True" : val
+syntax "False" : val
+syntax str : val
+syntax num : val
+syntax bareKey := ident  -- TODO
+syntax key := bareKey <|> str
+declare_syntax_cat keyCat @[keyCatParser] def key' := key  -- HACK: for the antiquotation
+syntax keyVal := key " = " val
+syntax table := "[" key "]" keyVal*
+syntax inlineTable := "{" keyVal,* "}"
+syntax inlineTable : val
+syntax file := table*
+declare_syntax_cat fileCat @[fileCatParser] def file' := file  -- HACK: for the antiquotation
+
+open Lean
+
+partial def ofSyntax : Syntax → Value
+  | `(val|True) => Value.bool true
+  | `(val|False) => Value.bool false
+  | `(val|$s:strLit) => Value.str <| s.isStrLit?.get!
+  | `(val|$n:numLit) => Value.nat <| n.isNatLit?.get!
+  | `(val|{$[$keys:key = $values],*}) => toTable keys (values.map ofSyntax)
+  | `(fileCat|$[[$keys] $kvss*]*) => toTable keys <| kvss.map fun kvs => ofSyntax <| Lean.Unhygienic.run `(val|{$kvs,*})
+  | stx => unreachable!
+  where
+    toKey : Syntax → String
+      | `(keyCat|$key:ident)  => key.getId.toString
+      | `(keyCat|$key:strLit) => key.isStrLit?.get!
+      | _                     => unreachable!
+    toTable (keys : Array Syntax) (vals : Array Value) : Value :=
+      Value.table <| Array.toList <| keys.zipWith vals fun k v => (toKey k, v)
+
+open Lean.Parser
+
+def parse (input : String) : IO Value := do
+  -- HACKHACKHACK
+  let env ← importModules [{ module := `Leanpkg.Toml }] {}
+  let fileParser ← compileParserDescr (parserExtension.getState env).categories file { env := env, opts := {} }
+  let c := mkParserContext (mkInputContext input "") { env := env, options := {} }
+  let s := mkParserState input
+  let s := whitespace c s
+  let s := fileParser.fn c s
+  if s.hasError then
+    throw <| IO.userError (s.toErrorMsg c)
+  else if input.atEnd s.pos then
+    ofSyntax s.stxStack.back
+  else
+    throw <| IO.userError ((s.mkError "end of input").toErrorMsg c)
+
+end Toml

src/lean.mk.in

@@ -34,7 +34,7 @@ SHELL = /usr/bin/env bash -eo pipefail
 
 all: $(OBJS)
 
-bin: $(BIN_OUT)/$(PKG)
+bin: $(BIN_OUT)/$(BIN_NAME)
 
 lib: $(LIB_OUT)/$(STATIC_LIB_NAME)
 

src/shell/CMakeLists.txt

@@ -112,3 +112,7 @@ FOREACH(T ${LEANTESTS})
              COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}")
   endif()
 ENDFOREACH(T)
+
+add_test(NAME leanpkgtest
+         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/b"
+         COMMAND bash -c "PATH=${LEAN_BIN}:$PATH leanpkg build")

src/stdlib.make.in

@@ -7,6 +7,7 @@ LEANMAKE_OPTS=\
 	OUT="${LIB}"\
 	LIB_OUT="${LIB}/lean"\
 	OLEAN_OUT="${LIB}/lean"\
+	BIN_OUT="${CMAKE_BINARY_DIR}/bin"\
 	LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -Dinterpreter.prefer_native=false"\
 	LEANC_OPTS+="${LEANC_OPTS}"\
 	MORE_DEPS+="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\
@@ -17,3 +18,4 @@ stdlib:
 	+"${LEAN_BIN}/leanmake" lib PKG=Init $(LEANMAKE_OPTS)
 	+"${LEAN_BIN}/leanmake" lib PKG=Std $(LEANMAKE_OPTS)
 	+"${LEAN_BIN}/leanmake" lib PKG=Lean $(LEANMAKE_OPTS)
+	+"${LEAN_BIN}/leanmake" bin PKG=Leanpkg BIN_NAME=leanpkg $(LEANMAKE_OPTS) LINK_OPTS="${CMAKE_EXE_LINKER_FLAGS}"

tests/leanpkg/a/.gitignore

@@ -0,0 +1 @@
+/build

tests/leanpkg/a/A.lean

@@ -0,0 +1 @@
+def name := "world"

tests/leanpkg/a/leanpkg.toml

@@ -0,0 +1,3 @@
+[package]
+name = "a"
+version = "0.1"

tests/leanpkg/b/.gitignore

@@ -0,0 +1 @@
+/build

tests/leanpkg/b/B.lean

@@ -0,0 +1,4 @@
+import A
+
+def main : IO Unit :=
+  IO.println "Hello, {name}!"

tests/leanpkg/b/leanpkg.toml

@@ -0,0 +1,6 @@
+[package]
+name = "b"
+version = "0.1"
+
+[dependencies]
+a = { path = "../a" }