diff --git a/bin/ltags b/bin/ltags
new file mode 100755
index 0000000000..148431396b
--- /dev/null
+++ b/bin/ltags
@@ -0,0 +1,185 @@
+#!/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 argparse
+import fnmatch
+import os
+import sys
+import codecs
+
+def get_ilean_files(directory):
+    """Return ilean files under directory (recursively)"""
+    ilean_files = []
+    if not os.path.isdir(directory):
+        raise IOError("%s is not a directory" % directory)
+
+    for root, dirnames, filenames in os.walk(directory):
+        for filename in fnmatch.filter(filenames, '*.ilean'):
+            ilean_files.append(os.path.join(root, filename))
+    return ilean_files
+
+def parse_arg(argv):
+    """ Parse arguments """
+    parser = argparse.ArgumentParser(description='Process arguments.')
+    parser.add_argument('--etags', '-e', action='store_true', default=True,  help="Generate etags TAGS file.")
+    parser.add_argument('--gtags', '-g', action='store_true', default=False, help="Generate gtags files (GTAGS, GRTAGS, GPATH).")
+    parser.add_argument('files', nargs='*')
+    args = parser.parse_args(argv)
+    return args
+
+def get_short_name(id):
+    last_pos_of_dot = id.rfind('.')
+    if last_pos_of_dot >= 0:
+        return id[last_pos_of_dot+1:]
+    return id
+
+def build_line_to_byteoffset_map(ilean_filename):
+    """Given a .ilean filename, return a mapping from a line number to the
+    byte offset of the beginning of the line. Note that line number
+    starts with 0 in our convention.
+    """
+    map = [0, 0]
+    lines = [""]
+    pos = 0
+    with codecs.open(ilean_filename, "r", "utf-8") as f:
+        while True:
+            line = f.readline()
+            if not line:
+                break
+            pos = pos + len(line)
+            map.append(pos + 1)
+            lines.append(line)
+    return (map, lines)
+
+def convert_position_to_etag_style(info):
+    """Convert the position format from (line, col) to (line, byteoffset)"""
+    filename = info[0]['filename']
+    (line_to_byteoffset, contents) = build_line_to_byteoffset_map(filename)
+    for item in info:
+        linenum = item['linenum']
+        col     = item['col']
+        item['offset'] = line_to_byteoffset[linenum] + col
+        item['prefix'] = contents[linenum][:col] + get_short_name(item['id'])
+#        item['prefix'] = ".*" + get_short_name(item['id'])
+
+def extract_info_from_ilean(ilean_file):
+    info = []
+    with open(ilean_file) as f:
+        for line in f:
+            array = line[:-1].split("|")
+            item = {}
+            item['type'] = array[0]
+            item['filename'] = array[1]
+            item['linenum'] = int(array[2])
+            item['col'] = int(array[3])
+            item['id'] = array[4]
+            info.append(item)
+    return info
+
+def get_etag_def_header(filename, len):
+    result = "\x0c\n%s,%d\n" % (filename, len)
+    return result
+
+def get_etag_def_item(item):
+    result = "%s\x7f%s\x01%d,%d\n" \
+             % (item['prefix'], get_short_name(item['id']), item['linenum'], item['offset'])
+    return result
+
+def get_etag_def_items(items):
+    result = ""
+    for item in items:
+        if item['type'] == 'd':
+            result += get_etag_def_item(item)
+    return result
+
+def get_etag_def(info):
+    body_str = get_etag_def_items(info)
+    header = get_etag_def_header(info[0]['filename'], len(body_str))
+    return header + body_str
+
+def print_item(item):
+    print "\t%s\t%-60s:%4d:%4d:%6d - %s" \
+        % (item['type'], item['filename'], item['linenum'], item['col'], item['offset'], item['id'])
+
+def print_items(items):
+    for item in items:
+        print get_etag_def_entry(item),
+
+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 filter_ilean_files(ilean_files):
+    """Remove .ilean file if a corresponding .lean file does not exist."""
+    result = []
+    for ilean_file in ilean_files:
+        lean_file = ilean_file[:-5] + "lean"
+        if os.path.isfile(lean_file) and os.path.isfile(ilean_file):
+            result.append(ilean_file)
+    return result
+
+def main(argv=None):
+    if argv is None:
+        argv = sys.argv[1:]
+    args = parse_arg(argv)
+
+    directory = os.getcwd()
+    if args.files:
+        ilean_files = fnmatch.filter(args.files, '*.ilean')
+    else:
+        makefile_names = ["GNUmakefile", "makefile", "Makefile"]
+        makefile = find_makefile_upward(directory, makefile_names)
+        if makefile:
+            directory = os.path.dirname(makefile)
+        ilean_files = get_ilean_files(directory)
+
+    ilean_files = filter_ilean_files(ilean_files)
+
+    if not ilean_files:
+        return 0
+
+    with codecs.open(os.path.join(directory, "TAGS"), 'w', 'utf-8') as tag_file:
+        for ilean_file in ilean_files:
+            info = extract_info_from_ilean(ilean_file)
+            if info:
+                convert_position_to_etag_style(info)
+                tag_file.write(get_etag_def(info))
+
+if __name__ == "__main__":
+    sys.exit(main())