diff --git a/bin/.gitignore b/bin/.gitignore
new file mode 100644
index 000000000..3d8d93961
--- /dev/null
+++ b/bin/.gitignore
@@ -0,0 +1,2 @@
+lean
+lean.exe
diff --git a/bin/lmake b/bin/lmake
new file mode 100755
index 000000000..024edd4f2
--- /dev/null
+++ b/bin/lmake
@@ -0,0 +1,156 @@
+#!/usr/bin/env python2
+#
+# Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+# Released under Apache 2.0 license as described in the file LICENSE.
+#
+# Author: Soonho Kong
+
+import os.path
+import sys
+import subprocess
+import string
+import argparse
+
+def lean_exe_name():
+    """ Return a lean executable name """
+    import platform
+    if platform.system() == 'Windows':
+        return "lean.exe"
+    else:
+        return "lean"
+
+def find_makefile(path, makefile_names):
+    """ Find makefile in a given directory.
+
+    Args:
+        path: a string of path to look up
+        makefile_names: a list of strings to search
+
+    Return:
+        When found, return the full path of a makefile
+        Otherwise, return False.
+    """
+    for makefile in makefile_names:
+        makefile_pathname = os.path.join(path, makefile)
+        if os.path.isfile(makefile_pathname):
+            return makefile_pathname
+    return False
+
+def find_makefile_upward(path, makefile_names):
+    """ Strating from a given directory, search upward to find
+    a makefile
+
+    Args:
+        path: a string of path to start the search
+
+    Return:
+        When found, return the full path of a makefile
+        Otherwise, return False.
+    """
+    makefile = find_makefile(path, makefile_names)
+    if makefile:
+        return makefile
+    up = os.path.dirname(path)
+    if up != path:
+        return find_makefile_upward(up, makefile_names)
+    return False
+
+def which(program):
+    """ Lookup program in a path """
+    import os
+    def is_exe(fpath):
+        return os.path.isfile(fpath) and os.access(fpath, os.X_OK)
+    fpath, fname = os.path.split(program)
+    if fpath:
+        if is_exe(program):
+            return program
+    else:
+        for path in os.environ["PATH"].split(os.pathsep):
+            path = path.strip('"')
+            exe_file = os.path.join(path, program)
+            if is_exe(exe_file):
+                return exe_file
+    return None
+
+def find_lean_exe():
+    """ Find a fullpath of Lean executable """
+    # First Look up environment variable
+    lean=os.environ.get('LEAN')
+    if lean:
+        return lean
+    # Otherwise, Look up in PATH
+    import platform
+    lean = which(lean_exe_name())
+    # Otherwise, look up the directory where lmake is at
+    script_dir = os.path.dirname(os.path.realpath(__file__))
+    lean = os.path.join(script_dir, lean_exe_name())
+    if os.path.isfile(lean):
+        return lean
+    return False
+
+def find_lean_opt():
+    """ Return a list of lean options from env_var LEAN_OPTION"""
+    lean_opt = os.environ.get('LEAN_OPTION')
+    if lean_opt:
+        return string.split(lean_opt)
+    else:
+        return []
+
+def call_lean(leanfile, options):
+    """ Call lean with options """
+    from collections import OrderedDict
+    lean_exe = find_lean_exe()
+    lean_opt = list(OrderedDict.fromkeys(find_lean_opt() + options))
+    subprocess.call([lean_exe] + lean_opt + [leanfile], stderr=subprocess.STDOUT)
+
+def get_target(s):
+    """ Extract a target from an argument
+    if we have "xyz.lean", return "xyz.olean"
+    Otherwise, return s as it is. (it might be phony target such as 'clean')
+    """
+    if os.path.isfile(s) and s[-5:] == ".lean":
+        leanfile = os.path.realpath(s)
+        return leanfile[:-5] + ".olean"
+    if os.path.isfile(s + ".lean"):
+        leanfile = os.path.realpath(s + ".lean")
+        return leanfile[:-5] + ".olean"
+    return s
+
+def call_makefile(makefile, arg):
+    """ Call makefile with a target generated from a given arg """
+    env_copy = os.environ.copy()
+    env_copy['LEAN'] = find_lean_exe()
+    cmd = ["make", "-C", os.path.dirname(makefile)]
+    if arg:
+        target = get_target(arg)
+        cmd.append(target)
+    subprocess.call(cmd, stderr=subprocess.STDOUT, env=env_copy)
+
+def parse_arg(argv):
+    """ Parse arguments """
+    parser = argparse.ArgumentParser(description='Process arguments.')
+    parser.add_argument('--flycheck', '-F', action='store_true', default=False, help="flycheck")
+    parser.add_argument('--flyinfo',  '-I', action='store_true', default=False, help="flyinfo")
+    parser.add_argument('target', nargs='?')
+    args = parser.parse_args(argv)
+    options = []
+    if args.flycheck:
+        options.append("--flycheck")
+    if args.flyinfo:
+        options.append("--flyinfo")
+    return (options, args.target)
+
+def main(argv=None):
+    if argv is None:
+        argv = sys.argv[1:]
+    (options, arg) = parse_arg(argv)
+    working_dir = os.getcwd()
+    makefile_names = ["Makefile", "makefile"]
+    makefile = find_makefile_upward(working_dir, makefile_names)
+    if makefile:
+        call_makefile(makefile, arg)
+    if arg and os.path.isfile(arg):
+        call_lean(arg, options)
+
+if __name__ == "__main__":
+    sys.exit(main())