https://github.com/JasonGross/coq-tools
Raw File
Tip revision: a47ed37e05cc2f848d43cb70a627db5c518ba0c0 authored by Jason Gross on 12 July 2022, 18:21:59 UTC
Remove path sensitivity in traceback output, test 12
Tip revision: a47ed37
custom_arguments.py
from __future__ import print_function
import sys, os
from argparse_compat import argparse
from util import PY3

__all__ = ["add_libname_arguments", "add_passing_libname_arguments", "ArgumentParser", "update_env_with_libnames", "add_logging_arguments", "process_logging_arguments", "update_env_with_coqpath_folders", "DEFAULT_LOG", "DEFAULT_VERBOSITY", "LOG_ALWAYS"]

# grumble, grumble, we want to support multiple -R arguments like coqc
class CoqLibnameAction(argparse.Action):
    non_default = False
#     def __init__(self, *args, **kwargs):
#         super(CoqLibnameAction, self).__init__(*args, **kwargs)
    def __call__(self, parser, namespace, values, option_string=None):
#        print('%r %r %r' % (namespace, values, option_string))
        if not self.non_default:
            setattr(namespace, self.dest, [])
            self.non_default = True
        getattr(namespace, self.dest).append(tuple(values))

DEFAULT_VERBOSITY=1
LOG_ALWAYS=None

def make_logger(log_files):
    # log if level <= the level of the logger
    def log(text, level=DEFAULT_VERBOSITY, max_level=None, force_stdout=False, force_stderr=False, end='\n'):
        selected_log_files = [f for flevel, f in log_files if level is LOG_ALWAYS or (level <= flevel and (max_level is None or flevel < max_level))]
        for i in selected_log_files:
            if force_stderr and i.fileno() == 1 and not force_stdout: continue # skip stdout if we write to stderr
            if force_stdout and i.fileno() == 2 and not force_stderr: continue # skip stderr if we write to stdout
            i.write(str(text) + end)
            i.flush()
            if i.fileno() > 2: # stderr
                os.fsync(i.fileno())
        for (force, fno, sys_file) in ((force_stdout, 1, sys.stdout), (force_stderr, 2, sys.stderr)):
            if force and not any(i.fileno() == fno for i in selected_log_files): # not already writing to std{out,err}
                if PY3:
                    sys_file.buffer.write(text.encode('utf-8'))
                    sys_file.buffer.write(end.encode('utf-8'))
                    sys_file.flush()
                else:
                    print(text, end=end, file=sys_file)
    return log

DEFAULT_LOG = make_logger([(DEFAULT_VERBOSITY, sys.stderr)])

class DeprecatedAction(argparse.Action):
    def __init__(self, replacement=None, *args, **kwargs):
        if replacement is None:
            raise ValueError("replacement must not be None")
        super(DeprecatedAction, self).__init__(*args, **kwargs)
        self.replacement = replacement
    def __call__(self, parser, namespace, values, option_string=None):
        print('ERROR: option %s is deprecated.  Use %s instead.' % (option_string, self.replacement), file=sys.stderr)
        sys.exit(0)

class ArgAppendWithWarningAction(argparse.Action):
    def __call__(self, parser, namespace, value, option_string=None):
        items = getattr(namespace, self.dest) or []
        items.append(value)
        setattr(namespace, self.dest, items)
        if value.startswith('-w '):
            print(('WARNING: You seem to be trying to pass a warning list to Coq via a single %s ("%s").' +
                   '\n  I will continue anyway, but this will most likely not work.' +
                   '\n  Instead try using multiple invocations, as in' +
                   '\n    %s')
                  % (option_string, value, ' '.join(option_string + '=' + v for v in value.split(' '))),
                  file=sys.stderr)

def add_libname_arguments_gen(parser, passing):
    passing_dash = passing + '-' if passing else ''
    twodash_passing_dash = '--' + passing_dash
    onedash_passing_dash = '-' + ('-' + passing + '-' if passing else '')
    passing_underscore = passing + '_' if passing else ''
    passing_for = ', for --' + passing + 'coqc' if passing else ''
    parser.add_argument(twodash_passing_dash + 'topname', metavar='TOPNAME', dest=passing_underscore+'topname', type=str, default='Top', action=DeprecatedAction, replacement='-R',
                        help='The name to bind to the current directory using -R .')
    parser.add_argument(onedash_passing_dash + 'R', metavar=('DIR', 'COQDIR'), dest=passing_underscore+'libnames', type=str, default=[], nargs=2, action=CoqLibnameAction,
                        help='recursively map physical DIR to logical COQDIR, as in the -R argument to coqc' + passing_for)
    parser.add_argument(onedash_passing_dash + 'Q', metavar=('DIR', 'COQDIR'), dest=passing_underscore+'non_recursive_libnames', type=str, default=[], nargs=2, action=CoqLibnameAction,
                        help='(nonrecursively) map physical DIR to logical COQDIR, as in the -Q argument to coqc' + passing_for)
    parser.add_argument(onedash_passing_dash + 'I', metavar='DIR', dest=passing_underscore+'ocaml_dirnames', type=str, default=[], action='append',
                        help='Look for ML files in DIR, as in the -I argument to coqc' + passing_for)
    parser.add_argument(twodash_passing_dash + 'arg', metavar='ARG', dest=passing_underscore+'coq_args', type=str, action=ArgAppendWithWarningAction,
                        help='Arguments to pass to coqc and coqtop; e.g., " -indices-matter" (leading and trailing spaces are stripped)' + passing_for)
    parser.add_argument(onedash_passing_dash + 'f', metavar='FILE', dest=passing_underscore+'CoqProjectFile', nargs=1, type=argparse.FileType('r'),
                        default=None,
                        help=('A _CoqProject file' + passing_for))

def add_libname_arguments(parser): add_libname_arguments_gen(parser, passing='')
def add_passing_libname_arguments(parser):
    add_libname_arguments_gen(parser, 'passing')
    add_libname_arguments_gen(parser, 'nonpassing')

def TupleType(*types):
    def call(strings):
        vals = strings.split(',')
        if len(vals) != len(types):
            raise ValueError("Got %d arguments, expected %d arguments" % (len(vals), len(types)))
        return tuple(ty(val) for ty, val in zip(types, vals))
    return call

def add_logging_arguments(parser):
    parser.add_argument('--verbose', '-v', dest='verbose',
                        action='count',
                        help='display some extra information by default (does not impact --verbose-log-file)')
    parser.add_argument('--quiet', '-q', dest='quiet',
                        action='count',
                        help='the inverse of --verbose')
    parser.add_argument('--log-file', '-l', dest='log_files', nargs='+', type=argparse.FileType('w'),
                        default=[sys.stderr],
                        help='The files to log output to.  Use - for stdout.')
    parser.add_argument('--verbose-log-file', dest='verbose_log_files', nargs='+', type=TupleType(int, argparse.FileType('w')),
                        default=[],
                        help=(('The files to log output to at verbosity other than the default verbosity (%d if no -v/-q arguments are passed); ' +
                               'each argument should be a pair of a verbosity level and a file name. '
                               'Use - for stdout.') % DEFAULT_VERBOSITY))

def process_logging_arguments(args):
    if args.verbose is None: args.verbose = DEFAULT_VERBOSITY
    if args.quiet is None: args.quiet = 0
    args.verbose -= args.quiet
    args.log = make_logger([(args.verbose, f) for f in args.log_files]
                           + args.verbose_log_files)
    del args.quiet
    del args.verbose
    return args

def tokenize_CoqProject(contents):
    is_in_string = False
    is_in_comment = False
    cur = ''
    for ch in contents:
        if is_in_string:
            cur += ch
            if ch == '"':
                yield cur
                cur = ''
                is_in_string = False
        elif is_in_comment:
            if ch in '\n\r': is_in_comment = False
        elif ch == '"':
            cur += ch
            is_in_string = True
        elif ch == '#':
            if cur: yield cur
            cur = ''
            is_in_comment = True
        else:
            if ch in '\n\r\t ':
                if cur: yield cur
                cur = ''
            else:
                cur += ch
    if cur:
        yield cur

def argstring_to_iterable(arg):
    if arg[:1] == '"' and arg[-1:] == '"': arg = arg[1:-1]
    return arg.split(' ')

def append_coq_arg(env, arg, passing=''):
    for key in ('coqc_args', 'coqtop_args'):
        env[passing + key] = tuple(list(env.get(passing + key, [])) + list(argstring_to_iterable(arg)))

def process_CoqProject(env, contents, passing=''):
    if contents is None: return
    tokens = tuple(tokenize_CoqProject(contents))
    i = 0
    while i < len(tokens):
        if tokens[i] == '-R' and i+2 < len(tokens):
            env[passing + 'libnames'].append((tokens[i+1], tokens[i+2]))
            i += 3
        elif tokens[i] == '-Q' and i+2 < len(tokens):
            env[passing + 'non_recursive_libnames'].append((tokens[i+1], tokens[i+2]))
            i += 3
        elif tokens[i] == '-I' and i+1 < len(tokens):
            env[passing + 'ocaml_dirnames'].append(tokens[i+1])
            i += 2
        elif tokens[i] == '-arg' and i+1 < len(tokens):
            append_coq_arg(env, tokens[i+1], passing=passing)
            i += 2
        elif tokens[i][-2:] == '.v':
            env[passing + '_CoqProject_v_files'].append(tokens[i])
            i += 1
        elif any(tokens[i][-len(ext):] == ext for ext in ('.mli', '.ml', '.mlg', '.mllib', '.ml4')):
            i += 1
        else:
            if 'log' in env.keys(): env['log']('Unknown _CoqProject entry: %s' % repr(tokens[i]))
            env[passing + '_CoqProject_unknown'].append(tokens[i])
            i += 1

def update_env_with_libname_default(env, args, default=(('.', 'Top'), ), passing=''):
    if len(getattr(args, passing + 'libnames') + getattr(args, passing + 'non_recursive_libnames') + env[passing + 'libnames'] + env[passing + 'non_recursive_libnames']) == 0:
        env[passing + 'libnames'].extend(list(default))

def update_env_with_libnames(env, args, default=(('.', 'Top'), ), include_passing=False, use_default=True, use_passing_default=True):
    all_keys = ('libnames', 'non_recursive_libnames', 'ocaml_dirnames', '_CoqProject', '_CoqProject_v_files', '_CoqProject_unknown')
    passing_opts = ('', ) if not include_passing else ('', 'passing_', 'nonpassing_')
    for passing in passing_opts:
        for key in all_keys:
            env[passing + key] = []
        if getattr(args, passing + 'CoqProjectFile'):
            for f in getattr(args, passing + 'CoqProjectFile'):
                env[passing + '_CoqProject'] = f.read()
                f.close()
        process_CoqProject(env, env[passing + '_CoqProject'], passing=passing)
        env[passing + 'libnames'].extend(getattr(args, passing + 'libnames'))
        env[passing + 'non_recursive_libnames'].extend(getattr(args, passing + 'non_recursive_libnames'))
        env[passing + 'ocaml_dirnames'].extend(getattr(args, passing + 'ocaml_dirnames'))
    if include_passing:
        # The nonpassing_ prefix is actually temporary; the semantics
        # are that, e.g., libnames = libnames + nonpassing_libnames,
        # while passing_libnames = libnames + passing_libnames
        for key in all_keys:
            env['passing_' + key] = env[key] + env['passing_' + key]
            env[key] = env[key] + env['nonpassing_' + key]
            del env['nonpassing_' + key]
    if use_default:
        update_env_with_libname_default(env, args, default=default)
    if use_passing_default and include_passing:
        update_env_with_libname_default(env, args, default=default, passing='passing_')

def update_env_with_coqpath_folders(passing_prefix, env, *coqpaths):
    def do_with_path(path):
        env.get(passing_prefix + 'non_recursive_libnames', []).extend((os.path.join(path, d), d) for d in sorted(os.listdir(path)))
    for coqpath in coqpaths:
        if os.path.isdir(coqpath):
            do_with_path(coqpath)
        elif ';' in coqpath:
            for path in coqpath.split(';'):
                do_with_path(coqpath if coqpath != '' else '.')
        elif ':' in coqpath:
            for path in coqpath.split(':'):
                do_with_path(coqpath if coqpath != '' else '.')

# http://stackoverflow.com/questions/5943249/python-argparse-and-controlling-overriding-the-exit-status-code
class ArgumentParser(argparse.ArgumentParser):
    def _get_action_from_name(self, name):
        """Given a name, get the Action instance registered with this parser.
        If only it were made available in the ArgumentError object. It is
        passed as it's first arg...
        """
        container = self._actions
        if name is None:
            return None
        for action in container:
            if '/'.join(action.option_strings) == name:
                return action
            elif action.metavar == name:
                return action
            elif action.dest == name:
                return action

    def error(self, message):
        def reraise(extra=''):
            super(ArgumentParser, self).error(message + extra)
        exc = sys.exc_info()[1]
        if exc:
            exc.argument = self._get_action_from_name(exc.argument_name)
            exc.reraise = reraise
            raise exc
        reraise()
back to top