feat(leanpkg): support path option to specify source directory

leanpkg/leanpkg/main.lean

@@ -57,7 +57,7 @@ def init_gitignore_contents :=
 "
 
 def init_pkg (n : string) (dir : string) : io unit := do
-write_manifest { name := n, version := "0.1", dependencies := [] }
+write_manifest { name := n, version := "0.1", path := none, dependencies := [] }
   (dir ++ "/" ++ leanpkg_toml_fn),
 write_file (dir ++ "/.gitignore") init_gitignore_contents io.mode.append
 
@@ -115,6 +115,7 @@ def main : ∀ (args : list string), io unit
   when (¬ ex) $ write_manifest {
       name := "_user_local_packages",
       version := "1",
+      path := none,
       dependencies := []
     } user_toml_fn,
   exec_cmd "leanpkg" ("add" :: rest) dot_lean_dir,

leanpkg/leanpkg/manifest.lean

@@ -44,24 +44,33 @@ end dependency
 
 structure manifest :=
 (name : string) (version : string)
+(path : option string)
 (dependencies : list dependency)
 
 namespace manifest
 
+def effective_path (m : manifest) : list string :=
+[match m.path with some p := p | none := "." end]
+
 def from_toml (t : toml.value) : option manifest := do
 pkg ← t.lookup "package",
 toml.value.str n ← pkg.lookup "name" | none,
 toml.value.str ver ← pkg.lookup "version" | none,
+path ← match pkg.lookup "path" with
+       | some (toml.value.str path) := some (some path)
+       | none := some none
+       | _ := none
+       end,
 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 }
+return { name := n, version := ver, path := path, dependencies := deps }
 
 def to_toml (d : manifest) : toml.value :=
-let pkg := toml.value.table [("name", toml.value.str d.name),
-                             ("version", toml.value.str d.version)],
+let pkg := [("name", toml.value.str d.name), ("version", toml.value.str d.version)],
+    pkg := match d.path with some p := pkg ++ [("path", toml.value.str p)] | none := pkg end,
     deps := toml.value.table $ d.dependencies.for $ λ dep, (dep.name, dep.src.to_toml) in
-toml.value.table [("package", pkg), ("dependencies", deps)]
+toml.value.table [("package", toml.value.table pkg), ("dependencies", deps)]
 
 instance : has_to_string manifest :=
 ⟨λ d, d.to_toml.to_string⟩

leanpkg/leanpkg/resolve.lean

@@ -78,9 +78,9 @@ def solve_deps (d : manifest) : io assignment := do
 (_, assg) ← solve_deps_core "." d 1024 $ assignment.empty.insert d.name ".",
 return assg
 
-def construct_path_core (depname : string) (dirname : string) : io (list string) := do
-manifest ← manifest.from_file $ dirname ++ "/" ++ leanpkg_toml_fn,
-return [dirname]
+def construct_path_core (depname : string) (dirname : string) : io (list string) :=
+list.map (λ relpath, dirname ++ "/" ++ relpath) <$>
+manifest.effective_path <$> (manifest.from_file $ dirname ++ "/" ++ leanpkg_toml_fn)
 
 def construct_path (assg : assignment) : io (list string) := do
 let assg := assg.fold [] (λ xs depname dirname, (depname, dirname) :: xs),