leanprover/lean0.1 — pull request #3 by soonhokong (2014-06-03 22:36:02+00:00)
Title: fix(frontends/lean/parser): add to check ".lean" file

Problem
=======

Consider a case where we have:

library/standard/nat.lean
library/standard/int2.lean
...

and int2.lean has "import nat".

In the previous version, '--deps' generates

int2.olean: file 'nat' not found in the LEAN_PATH

because it can't find int2.olean.

Solution
========

Add to check ".lean" file and output ".olean" as a dependency.
With it, we have

int2.olean: ./nat.olean ./macros.lua