max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(leanpkg): fix error message

Browse source
This commit is contained in:
Sebastian Ullrich 2017-09-14 15:31:32 +02:00
parent 87b39bd1c3
commit 3c68f6fa00
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
leanpkg/leanpkg/resolve.lean
View file

@ -87,11 +87,11 @@ deps ← monad.filter (not_yet_assigned ∘ dependency.name) d.dependencies,
deps.mmap' (materialize relpath),
deps.mmap' $ λ dep, do
p ← resolved_path dep.name,
d ← manifest.from_file $ p ++ "/" ++ "leanpkg.toml",
when (d.name ≠ dep.name) $
io.fail $ d.name ++ " (in " ++ relpath ++ ") depends on " ++ d.name ++
d' ← manifest.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
solve_deps_core p d' max_depth
def solve_deps (d : manifest) : io assignment := do
(_, assg) ← solve_deps_core "." d 1024 $ assignment.empty.insert d.name ".",