lean2/bin/lmake

#!/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 os.path
import string
import subprocess
import sys

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_OPTIONS """
    lean_opt = os.environ.get('LEAN_OPTIONS')
    return string.split(lean_opt) if lean_opt is not None else []

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_lean(s):
    """ Given a string s, return corresponding .lean file if exists """
    # xyz.olean => realpath(xyz.lean)
    if len(s) > 6 and s[-6:] == ".olean":
        leanfile = os.path.realpath(s[:-6] + ".lean")
        return leanfile if os.path.isfile(leanfile) else None
    # xyz.lean  => realpath(xyz.lean)
    if os.path.isfile(s) and len(s) > 5 and s[-5:] == ".lean":
        return os.path.realpath(s)
    # xyz       => realpath(xyz.lean)
    if os.path.isfile(s + ".lean"):
        return os.path.realpath(s + ".lean")
    return None

def get_olean(s):
    """ Given a string s, return corresponding .olean file if exists """
    # xyz.olean => realpath(xyz.olean)
    if len(s) > 6 and s[-6:] == ".olean":
        leanfile = s[:-6] + ".lean"
        return os.path.realpath(s) if os.path.isfile(leanfile) else None
    # xyz.lean  => realpath(xyz.olean)
    if os.path.isfile(s) and len(s) > 5 and s[-5:] == ".lean":
        leanfile = os.path.realpath(s)
        return leanfile[:-5] + ".olean"
    # xyz       => realpath(xyz.olean)
    if os.path.isfile(s + ".lean"):
        return os.path.realpath(s + ".olean")
    return None

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')
    """
    oleanfile = get_olean(s)
    return oleanfile if oleanfile is not None else s

def touch(fname, times=None):
    "touch a file"
    with open(fname, 'a'):
        os.utime(fname, times)

def touch_all_lean_files(directory):
    "Touch all lean file under directory"
    for root, dirnames, filenames in os.walk(directory):
        for filename in fnmatch.filter(filenames, '*.lean'):
            touch(os.path.join(root, filename))

def check_lean_options_file(directory, lean_options):
    "Check lean_options file and return true if all lean files should be touched."
    lean_new_options = " ".join(lean_options)
    lean_options_file_name = os.path.join(directory, ".lean_options")
    need_to_write = True
    if os.path.isfile(lean_options_file_name):
        with open(lean_options_file_name, 'r') as f:
            lean_old_options = f.readline()
            need_to_write = not (lean_old_options == lean_new_options)
    if need_to_write:
        with open(lean_options_file_name, 'w') as f:
            f.write(lean_new_options)
        return True
    return False

def call_makefile(directory, makefile, makefile_options, args, lean_options):
    """ Call makefile with a target generated from a given arg """
    need_to_update = check_lean_options_file(directory, lean_options)
    if need_to_update:
        touch_all_lean_files(directory)
    env_copy = os.environ.copy()
    env_copy['LEAN'] = find_lean_exe()
    lean_options_str = ' '.join(lean_options)
    if env_copy.get("LEAN_OPTIONS"):
        env_copy['LEAN_OPTIONS'] = env_copy['LEAN_OPTIONS'] + lean_options_str
    else:
        env_copy['LEAN_OPTIONS'] = lean_options_str
    cmd = ["make"]
    if makefile:
        cmd += ["--makefile", makefile]
    if directory:
        cmd += ["-C", directory]
    cmd += makefile_options
    for arg in args:
        target = get_target(arg)
        cmd.append(target)
    subprocess.call(cmd, stderr=subprocess.STDOUT, env=env_copy)

def check_positive(value):
    ivalue = int(value)
    if ivalue <= 0:
         raise argparse.ArgumentTypeError("%s is an invalid positive int value" % value)
    return ivalue

def parse_arg(argv):
    """ Parse arguments """
    parser = argparse.ArgumentParser(description='Process arguments.')
    parser.add_argument('--flycheck',   '-F', action='store_true', default=False, help="Use --flycheck option for Lean.")
    parser.add_argument('--permissive', '-P', action='store_true', default=False, help="Use --permissive option for Lean.")
    parser.add_argument('--keep-going', '-k', action='store_true', default=False, help="Continue as much as possible after an error.")
    parser.add_argument('--directory',  '-C', action='store', help="Change to directory dir before reading the makefiles or doing anything else.")
    parser.add_argument('--makefile',   '-f', '--file', action='store', help="Use file as a makefile.")
    parser.add_argument('--jobs',       '-j', nargs='?', default=-1, const=-2, type=check_positive, help="Specifies the number of jobs (commands) to run simultaneously.")
    parser.add_argument('--just-print', '--dry-run', '--recon', '-n', action='store_true', default=False, help="Don't actually run any commands; just print them.")
    parser.add_argument('targets', nargs='*')
    args = parser.parse_args(argv)
    lean_options = extract_lean_options(args)
    makefile_options = extract_makefile_options(args)
    return (args.directory, args.makefile, makefile_options, lean_options, args.targets)

def extract_lean_options(args):
    lean_options = []
    if args.flycheck:
        lean_options.append("--flycheck")
    if args.permissive:
        lean_options.append("--permissive")
    return lean_options

def extract_makefile_options(args):
    makefile_options = []
    if args.keep_going:
        makefile_options.append("--keep-going")
    if args.jobs == -1:
        # -j is not used
        pass
    elif args.jobs == -2:
        # -j is used but without providing number of processes
        makefile_options.append("-j")
    elif args.jobs:
        makefile_options += ["-j", args.jobs]
    if args.just_print:
        makefile_options.append("--just-print")
    return makefile_options

def main(argv=None):
    if argv is None:
        argv = sys.argv[1:]
    (directory, makefile, makefile_options, lean_options, args) = parse_arg(argv)
    working_dir = os.getcwd()
    if makefile is None and directory is None:
        makefile_names = ["GNUmakefile", "makefile", "Makefile"]
        makefile = find_makefile_upward(working_dir, makefile_names)
        if makefile:
            directory = os.path.dirname(makefile)
    if directory or makefile:
        call_makefile(directory, makefile, makefile_options, args, lean_options)
    else:
        for arg in args:
            leanfile = get_lean(arg)
            if leanfile and os.path.isfile(leanfile):
                call_lean(leanfile, lean_options)

if __name__ == "__main__":
    sys.exit(main())