diff --git a/bin/leanpkg b/bin/leanpkg
new file mode 100755
index 0000000000..2f38da45f3
--- /dev/null
+++ b/bin/leanpkg
@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+leandir=$(dirname $(readlink -f $0))/..
+leandir=$(readlink -f $leandir)
+
+LEAN_PATH=$leandir/library:$leandir/lib/lean/library:$leandir/leanpkg \
+  PATH=$leandir/bin:$PATH \
+  exec lean --run $leandir/leanpkg/leanpkg/main.lean "$@"
diff --git a/leanpkg/.project b/leanpkg/.project
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/leanpkg/leanpkg.path b/leanpkg/leanpkg.path
new file mode 100644
index 0000000000..2cbfd2b51b
--- /dev/null
+++ b/leanpkg/leanpkg.path
@@ -0,0 +1,2 @@
+builtin_path
+path .
diff --git a/leanpkg/leanpkg.toml b/leanpkg/leanpkg.toml
new file mode 100644
index 0000000000..66053b0be8
--- /dev/null
+++ b/leanpkg/leanpkg.toml
@@ -0,0 +1,3 @@
+[package]
+name = "leanpkg"
+version = "0.1"
diff --git a/leanpkg/leanpkg/desc.lean b/leanpkg/leanpkg/desc.lean
new file mode 100644
index 0000000000..c2d3fc2339
--- /dev/null
+++ b/leanpkg/leanpkg/desc.lean
@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Gabriel Ebner
+-/
+import leanpkg.toml system.io
+
+namespace leanpkg
+
+inductive source
+| path (dir_name : string) : source
+| git (url rev : string) : source
+
+namespace source
+
+def from_toml (v : toml.value) : option source :=
+(do toml.value.str dir_name ← v.lookup "path" | none,
+    return $ path dir_name) <|>
+(do toml.value.str url ← v.lookup "git" | none,
+    toml.value.str rev ← (v.lookup "rev") | none,
+    return $ git url rev) <|>
+(do toml.value.str url ← v.lookup "git" | none,
+    return $ git url "master")
+
+def to_toml : ∀ (s : source), toml.value
+| (path dir_name) := toml.value.table [("path", toml.value.str dir_name)]
+| (git url "master") :=
+  toml.value.table [("git", toml.value.str url)]
+| (git url rev) :=
+  toml.value.table [("git", toml.value.str url), ("rev", toml.value.str rev)]
+
+instance : has_to_string source :=
+⟨λ s, s.to_toml.to_string⟩
+
+end source
+
+structure dependency :=
+(name : string) (src : source)
+
+namespace dependency
+instance : has_to_string dependency :=
+⟨λ d, d.name ++ " = " ++ to_string d.src⟩
+end dependency
+
+structure desc :=
+(name : string) (version : string)
+(dependencies : list dependency)
+
+namespace desc
+
+def from_toml (t : toml.value) : option desc := do
+pkg ← t.lookup "package",
+toml.value.str n ← pkg.lookup "name" | none,
+toml.value.str ver ← pkg.lookup "version" | none,
+toml.value.table deps ← t.lookup "dependencies" <|> some (toml.value.table []) | none,
+deps ← monad.for deps (λ ⟨n, src⟩, do src ← source.from_toml src,
+                                      return $ dependency.mk n src),
+return { name := n, version := ver, dependencies := deps }
+
+def to_toml (d : desc) : toml.value :=
+let pkg := toml.value.table [("name", toml.value.str d.name),
+                             ("version", toml.value.str d.version)],
+    deps := toml.value.table $ d.dependencies.for $ λ dep, (dep.name, dep.src.to_toml) in
+toml.value.table [("package", pkg), ("dependencies", deps)]
+
+instance : has_to_string desc :=
+⟨λ d, d.to_toml.to_string⟩
+
+def from_string (s : string) : option desc :=
+match parser.run_string toml.File s with
+| sum.inr toml := from_toml toml
+| sum.inl _ := none
+end
+
+def from_file [io.interface] (fn : string) : io desc := do
+cnts ← io.fs.read_file fn,
+toml ←
+  (match parser.run toml.File cnts with
+  | sum.inl err :=
+    io.fail $ "toml parse error in " ++ fn ++ "\n\n" ++ err
+  | sum.inr res := return res
+  end),
+some desc ← return (from_toml toml)
+  | io.fail ("cannot read description from " ++ fn ++ "\n\n" ++ toml.to_string),
+return desc
+
+end desc
+
+end leanpkg
diff --git a/leanpkg/leanpkg/main.lean b/leanpkg/leanpkg/main.lean
new file mode 100644
index 0000000000..d50ba67ad9
--- /dev/null
+++ b/leanpkg/leanpkg/main.lean
@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Gabriel Ebner
+-/
+import leanpkg.resolve
+variable [io.interface]
+
+namespace leanpkg
+
+def leanpkg_toml_fn := "leanpkg.toml"
+
+def read_desc : io desc :=
+desc.from_file leanpkg_toml_fn
+
+def write_desc (d : desc) (fn := leanpkg_toml_fn) : io unit := do
+h ← io.mk_file_handle fn io.mode.write,
+io.fs.write h (to_string d).to_char_buffer,
+io.fs.close h
+
+-- TODO(gabriel): implement a cross-platform api
+def get_dot_lean_dir : io string :=
+io.cmd "bash" ["-c", "echo -n ~/.lean"]
+
+-- TODO(gabriel): file existence testing
+def exists_file (f : string) : io bool := do
+ch ← io.proc.spawn { cmd := "test", args := ["-f", f] },
+ev ← io.proc.wait ch,
+return $ ev = 0
+
+def mk_path_file (assg : assignment) : string :=
+let paths := assg.fold ["."] (λ xs _ x, x :: xs),
+    lines := "builtin_path" :: paths.map (λ p, "path " ++ p) in
+lines.foldr (λ x xs, x ++ "\n" ++ xs) ""
+
+def configure : io unit := do
+d ← read_desc,
+io.put_str_ln $ "configuring " ++ d.name ++ " " ++ d.version,
+assg ← solve_deps d,
+let path_file_cnts := mk_path_file assg,
+path_file_h ← io.mk_file_handle "leanpkg.path" io.mode.write,
+io.fs.write path_file_h $ buffer.nil.append_list path_file_cnts.reverse,
+io.fs.close path_file_h
+
+def make : io unit :=
+exec_cmd "lean" ["--make"]
+
+def build := configure >> make
+
+def add (dep : dependency) : io unit := do
+d ← read_desc,
+let d' := { d with dependencies := d.dependencies.filter (λ old_dep, old_dep.name ≠ dep.name) ++ [dep] },
+write_desc d'
+
+def init_pkg (n : string) (dir : string) : io unit := do
+write_desc { name := n, version := "0.1", dependencies := [] }
+  (dir ++ "/" ++ leanpkg_toml_fn),
+h ← io.mk_file_handle (dir ++ "/.gitignore") io.mode.append,
+io.fs.write h "*.olean\n/_target\n/leanpkg.path\n".to_char_buffer,
+io.fs.close h
+
+def init (n : string) := init_pkg n "."
+
+-- TODO(gabriel): windows
+def basename : ∀ (fn : string), string
+| []          := []
+| (c :: rest) :=
+  if c = #"/" then [] else c :: basename rest
+
+def new (dir : string) := do
+ex ← dir_exists dir,
+when ex $ io.fail $ "directory already exists: " ++ dir,
+exec_cmd "mkdir" ["-p", dir],
+init_pkg (basename dir) dir
+
+def usage := "
+Usage: leanpkg <command>
+
+configure       download dependencies
+build           download dependencies and build *.olean files
+
+new <dir>       creates a lean package in the specified directory
+init <name>     adds a leanpkg.toml file to the current directory, and sets up .gitignore
+
+add --git <name> <url> <rev>
+                adds a dependency from a git repository
+add --local <name> <directory>
+                adds a local dependency
+
+install --git <name> <url> <rev>
+                installs a user-wide package from git
+install --local <name> <url>
+                installs a user-wide package from a local directory
+
+dump            prints the parsed leanpkg.toml file (for debugging)
+"
+
+def main : ∀ (args : list string), io unit
+| ["configure"] := configure
+| ["build"] := build
+| ["new", dir] := new dir
+| ["init", name] := init name
+| ["add", "--git", n, url, rev] :=
+  add { name := n, src := source.git url rev }
+| ["add", "--local", n, dir] :=
+  add { name := n, src := source.path dir }
+| ("install" :: rest) := do
+  dot_lean_dir ← get_dot_lean_dir,
+  exec_cmd "mkdir" ["-p", dot_lean_dir],
+  let user_toml_fn := dot_lean_dir ++ "/" ++ leanpkg_toml_fn,
+  ex ← exists_file user_toml_fn,
+  when (¬ ex) $ write_desc {
+      name := "_user_local_packages",
+      version := "1",
+      dependencies := []
+    } user_toml_fn,
+  -- TODO(gabriel): remove this awesomely disgusting hack
+  exec_cmd "bash" $ ["-c", "cd $1 && shift && leanpkg add \"$@\" && leanpkg configure", "_", dot_lean_dir] ++ rest
+| ["dump"] := read_desc >>= io.print_ln
+| _ := io.fail usage
+
+end leanpkg
+
+def main : io unit := io.cmdline_args >>= leanpkg.main
diff --git a/leanpkg/leanpkg/proc.lean b/leanpkg/leanpkg/proc.lean
new file mode 100644
index 0000000000..c4dc4d42fd
--- /dev/null
+++ b/leanpkg/leanpkg/proc.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Gabriel Ebner
+-/
+import system.io leanpkg.toml
+open io io.proc
+variable [io.interface]
+
+namespace leanpkg
+
+def exec_cmd (cmd : string) (args : list string) (cwd : option string := none) : io unit := do
+let cmdstr := join " " (cmd::args),
+io.put_str_ln $ "> " ++
+  match cwd with
+  | some cwd := "(cd " ++ cwd ++ "; " ++ cmdstr ++ ")"
+  | none := cmdstr
+  end,
+ch ← spawn { cmd := cmd, args := args, cwd := cwd },
+exitv ← wait ch,
+when (exitv ≠ 0) $ io.fail $
+  "external command exited with status " ++ exitv.to_string
+
+end leanpkg
diff --git a/leanpkg/leanpkg/resolve.lean b/leanpkg/leanpkg/resolve.lean
new file mode 100644
index 0000000000..bc09de69d8
--- /dev/null
+++ b/leanpkg/leanpkg/resolve.lean
@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Gabriel Ebner
+-/
+import leanpkg.desc system.io data.hash_map leanpkg.proc
+variable [io.interface]
+
+namespace leanpkg
+
+def assignment := hash_map string (λ _, string)
+-- TODO(gabriel): hash function for strings
+def assignment.empty : assignment := mk_hash_map list.length
+
+@[reducible] def solver := state_t assignment io
+instance {α : Type} : has_coe (io α) (solver α) := ⟨state_t.lift⟩
+
+def not_yet_assigned (d : string) : solver bool := do
+assg ← state_t.read,
+return $ ¬ assg.contains d
+
+def resolved_path (d : string) : solver string := do
+assg ← state_t.read,
+some path ← return (assg.find d) | io.fail "",
+return path
+
+-- TODO(gabriel): directory existence testing
+def dir_exists (d : string) : io bool := do
+ch ← io.proc.spawn { cmd := "test", args := ["-d", d] },
+ev ← io.proc.wait ch,
+return $ ev = 0
+
+-- TODO(gabriel): windows?
+def resolve_dir (abs_or_rel : string) (base : string) : string :=
+if abs_or_rel.reverse.head = #"/" then
+  abs_or_rel -- absolute
+else
+  base ++ "/" ++ abs_or_rel
+
+def materialize (relpath : string) (dep : dependency) : solver unit :=
+match dep.src with
+| (source.path dir) := do
+  let depdir := resolve_dir dir relpath,
+  io.put_str_ln $ dep.name ++ ": using local path " ++ depdir,
+  state_t.modify $ λ assg, assg.insert dep.name depdir
+| (source.git url rev) := do
+  let depdir := "_target/deps/" ++ dep.name,
+  already_there ← dir_exists depdir,
+  let checkout_action := exec_cmd "git" ["checkout", rev] (some depdir),
+  (do guard already_there,
+      io.put_str_ln $ dep.name ++ ": trying to update " ++ depdir ++ " to revision " ++ rev,
+      checkout_action) <|>
+  (do guard already_there,
+      exec_cmd "git" ["fetch"] (some depdir),
+      checkout_action) <|>
+  (do io.put_str_ln $ dep.name ++ ": cloning " ++ url ++ " to " ++ depdir,
+      exec_cmd "rm" ["-rf", depdir],
+      exec_cmd "mkdir" ["-p", depdir],
+      exec_cmd "git" ["clone", url, depdir],
+      exec_cmd "git" ["checkout", rev] (some depdir)),
+  state_t.modify $ λ assg, assg.insert dep.name depdir
+end
+
+def solve_deps_core : ∀ (rel_path : string) (d : desc) (max_depth : ℕ), solver unit
+| _ _ 0 := io.fail "maximum dependency resolution depth reached"
+| relpath d (max_depth + 1) := do
+deps ← monad.filter (not_yet_assigned ∘ dependency.name) d.dependencies,
+monad.for' deps (materialize relpath),
+monad.for' deps $ λ dep, do
+  p ← resolved_path dep.name,
+  d ← desc.from_file $ p ++ "/" ++ "leanpkg.toml",
+  when (d.name ≠ dep.name) $
+    io.fail $ d.name ++ " (in " ++ relpath ++ ") depends on " ++ d.name ++
+      ", but resolved dependency has name " ++ dep.name ++ " (in " ++ p ++ ")",
+  solve_deps_core p d max_depth
+
+def solve_deps (d : desc) : io assignment := do
+(_, assg) ← solve_deps_core "." d 1024 assignment.empty,
+return assg
+
+end leanpkg
diff --git a/leanpkg/leanpkg/toml.lean b/leanpkg/leanpkg/toml.lean
new file mode 100644
index 0000000000..2e6baf3839
--- /dev/null
+++ b/leanpkg/leanpkg/toml.lean
@@ -0,0 +1,143 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Gabriel Ebner
+-/
+import data.buffer.parser
+
+-- I'd like to contribute a new naming convention:
+-- CamelCase for non-terminals.
+
+def join (sep : string) : list string → string
+| [x]     := x
+| []      := ""
+| (x::xs) := x ++ sep ++ join xs
+
+namespace toml
+
+inductive value : Type
+| str : string → value
+| bool : bool → value
+| table : list (string × value) → value
+
+namespace value
+
+private def escapec : char → string
+| #"\"" := "\\\""
+| #"\t" := "\\t"
+| #"\n" := "\\n"
+| #"\\" := "\\\\"
+| c     := [c]
+
+private def escape (s : string) : string :=
+list.bind s escapec
+
+private def to_string_core : ∀ (n : ℕ), value → string
+| _ (value.str s) := "\"" ++ escape s ++ "\""
+| _ (value.bool tt) := "true"
+| _ (value.bool ff) := "false"
+| (n+1) (value.table cs) :=
+  "{ " ++ join ", " (do (k, v) ← cs, [k ++ " = " ++ to_string_core n v]) ++ " }"
+| 0 _ := "<max recursion depth reached>"
+
+protected def to_string : ∀ (v : value), string
+| (table cs) := join "\n" $ do (h, c) ← cs,
+  match c with
+  | table ds :=
+    ["[" ++ h ++ "]\n" ++
+     join "" (do (k, v) ← ds,
+       [k ++ " = " ++ to_string_core 1024 v ++ "\n"])]
+  | _ := ["<error> " ++ to_string_core 1024 c]
+  end
+| v := to_string_core (sizeof v) v
+
+instance : has_to_string value :=
+⟨value.to_string⟩
+
+def lookup : value → string → option value
+| (value.table cs) k :=
+  match cs.filter (λ c : string × value, c.fst = k) with
+  | [] := none
+  | (k,v) ::_ := some v
+  end
+| _ _ := none
+
+end value
+
+open parser
+
+def Comment : parser unit :=
+ch #"#" >> many' (sat (≠ #"#")) >> optional (ch #"\n") >> eps
+
+def Ws : parser unit :=
+decorate_error "<whitespace>" $
+many' $ one_of " \t\n" <|> Comment
+
+def tok (s : string) := str s >> Ws
+
+def StringChar : parser char :=
+sat (λc, c ≠ #"\"" ∧ c ≠ #"\\" ∧ c.val > 0x1f)
+ <|> (do str "\\",
+         (str "t" >> return #"\t") <|>
+         (str "n" >> return #"\n") <|>
+         (str "\\" >> return #"\\") <|>
+         (str "\"" >> return #"\""))
+
+def BasicString : parser string :=
+str "\"" *> (list.reverse <$> many StringChar) <* str "\"" <* Ws
+
+def String := BasicString
+
+def Boolean : parser bool :=
+(tok "true" >> return tt) <|>
+(tok "false" >> return ff)
+
+def BareKey : parser string := do
+cs ← many1 $ sat $ λ c, c.is_alpha ∨ c.is_digit ∨ c = #"_" ∨ c = #"-",
+Ws,
+return cs.reverse
+
+def Key := BareKey <|> BasicString
+
+section
+parameter Val : parser value
+
+def KeyVal : parser (string × value) := do
+k ← Key, tok "=", v ← Val,
+return (k, v)
+
+def StdTable : parser (string × value) := do
+tok "[", n ← Key, tok "]",
+cs ← many KeyVal,
+return (n, value.table cs)
+
+def Table : parser (string × value) := StdTable
+
+def StrVal : parser value :=
+value.str <$> String
+
+def BoolVal : parser value :=
+value.bool <$> Boolean
+
+def InlineTable : parser value :=
+tok "{" *> (value.table <$> sep_by (tok ",") KeyVal) <* tok "}"
+
+end
+
+def Val : parser value :=
+fix $ λ Val, StrVal <|> BoolVal <|> InlineTable Val
+
+def Expression := Table Val
+
+def File : parser value :=
+Ws *> (value.table <$> many Expression)
+
+-- #eval run_string File $
+--   "[package]\n" ++
+--   "name = \"sss\"\n" ++
+--   "version = \"0.1\"\n" ++
+--   "\n" ++
+--   "[dependencies]\n" ++
+--   "library_dev = { git = \"https://github.com/leanprover/library_dev\", rev = \"master\" }"
+
+end toml
diff --git a/library/leanpkg.path b/library/leanpkg.path
new file mode 100644
index 0000000000..c0926e3e67
--- /dev/null
+++ b/library/leanpkg.path
@@ -0,0 +1 @@
+path .