Escape reserved keywords when inlining deps

Fixes #129

The code for finding the list of reserved names is kind-of hacky (see
https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Printing.20keywords/near/292550511),
and this doesn't handle all cases (in particular, there still seems to
be no way to handle qualified references to
`Equations.Prop.Equations.foo` which don't show up in the .glob file, or
which show up in the glob file in a way that is too fragile to do
mangling on), but this handles the common case of just doing `Require
Import Equations.Prop.Equations.`.

coq_running_support.py

@@ -1,17 +1,19 @@
 from __future__ import with_statement
+import re
 from diagnose_error import get_coq_output
 from coq_version import get_coq_native_compiler_ondemand_fragment
+from coq_full_grammar import COQ_GRAMMAR_TOKENS
 
 # Like coq_version.py, except for things that use get_coq_output (or
 # perhaps a bit more generally for things that need to run coqc on a
 # file)
 
-__all__ = ["get_proof_term_works_with_time", "get_ltac_support_snippet"]
+__all__ = ["get_proof_term_works_with_time", "get_ltac_support_snippet", "get_reserved_modnames"]
 
 def get_proof_term_works_with_time(coqc_prog, **kwargs):
     contents = r"""Lemma foo : forall _ : Type, Type.
 Proof (fun x => x)."""
-    output, cmds, retcode, runtime = get_coq_output(coqc_prog, ('-time', '-q'), contents, 1, verbose_base=3, **kwargs)
+    output, cmds, retcode, runtime = get_coq_output(coqc_prog, ('-time', '-q'), contents, timeout_val=1, verbose_base=3, **kwargs)
     return 'Error: Attempt to save an incomplete proof' not in output
 
 LTAC_SUPPORT_SNIPPET = {}
@@ -38,3 +40,18 @@ def get_ltac_support_snippet(coqc, **kwargs):
         else:
             errinfo[contents] = {'output': output, 'cmds': cmds, 'retcode': retcode, 'runtime': runtime}
     raise Exception('No valid ltac support snipped found.  Debugging info: %s' % repr(errinfo))
+
+def get_is_modname_valid(coqc_prog, modname, **kwargs):
+    contents = "Module %s. End %s." % (modname, modname)
+    if ' ' in modname: return False
+    output, cmds, retcode, runtime = get_coq_output(coqc_prog, ('-q',), contents, timeout_val=1, verbose_base=3, **kwargs)
+    return 'Syntax error:' not in output
+
+def get_reserved_modnames(coqtop_prog, **kwargs):
+    grammars_contents = 'Print Grammar tactic. Print Grammar constr. Print Grammar vernac.'
+    grammars_output, cmds, retcode, runtime = get_coq_output(coqtop_prog, ('-q',), grammars_contents, is_coqtop=True, pass_on_stdin=True, timeout_val=1, verbose_base=3, **kwargs)
+    tokens = sorted(set([i.strip('"') for i in re.findall(r'"[a-zA-Z_][^"]*"', grammars_output)] + COQ_GRAMMAR_TOKENS))
+    contents = '\n'.join("Module %s. End %s." % (modname, modname) for modname in tokens)
+    output, cmds, retcode, runtime = get_coq_output(coqtop_prog, ('-q',), contents, is_coqtop=True, pass_on_stdin=True, timeout_val=10, verbose_base=3, **kwargs)
+    success = re.findall(r'Module ([^ ]+) is defined', output)
+    return tuple(modname for modname in tokens if modname not in success)

examples/run-example-052.sh

@@ -87,12 +87,10 @@ ${PYTHON} "$FIND_BUG_PY" "$EXAMPLE_INPUT" "$EXAMPLE_OUTPUT" "${EXTRA_ARGS[@]}" |
 # entirely if you don't care about the minimized file.
 EXPECTED=$(cat <<EOF
 (\* -\*- mode: coq; coq-prog-args: ("-emacs"\( "-w" "-deprecated-native-compiler-option,-native-compiler-disabled"\)\? "-R" "\." "Top"\( "-top" "Top\.example_[0-9]\+"\)\?\( "-native-compiler" "ondemand"\)\?) -\*- \*)
-(\* File reduced by coq-bug-minimizer from original input, then from [0-9]\+ lines to [0-9]\+ lines, then from [0-9]\+ lines to [0-9]\+ lines \*)
+(\* File reduced by coq-bug-minimizer from original input, then from [0-9]\+ lines to [0-9]\+ lines, then from [0-9]\+ lines to [0-9]\+ lines, then from [0-9]\+ lines to [0-9]\+ lines, then from [0-9]\+ lines to [0-9]\+ lines \*)
 (\* coqc version [^\*]*\*)
 
-Require Top\.Prop\.Foo\.
-Import Top\.Prop\.Foo\.
-
+Definition n := nat\.
 Fail Check n\.
 
 EOF

examples/run-example-053.sh

@@ -90,8 +90,8 @@ EXPECTED=$(cat <<EOF
 (\* File reduced by coq-bug-minimizer from original input, then from [0-9]\+ lines to [0-9]\+ lines, then from [0-9]\+ lines to [0-9]\+ lines \*)
 (\* coqc version [^\*]*\*)
 
-Require Top\.Prop\.Foo\.
-
+Module Export Foo\.
+Definition n := nat\.
 Fail Check Foo\.n\.
 
 EOF

examples/run-example-054.sh

@@ -87,12 +87,10 @@ ${PYTHON} "$FIND_BUG_PY" "$EXAMPLE_INPUT" "$EXAMPLE_OUTPUT" "${EXTRA_ARGS[@]}" |
 # entirely if you don't care about the minimized file.
 EXPECTED=$(cat <<EOF
 (\* -\*- mode: coq; coq-prog-args: ("-emacs"\( "-w" "-deprecated-native-compiler-option,-native-compiler-disabled"\)\? "-R" "\." "Top"\( "-top" "Top\.example_[0-9]\+"\)\?\( "-native-compiler" "ondemand"\)\?) -\*- \*)
-(\* File reduced by coq-bug-minimizer from original input, then from [0-9]\+ lines to [0-9]\+ lines, then from [0-9]\+ lines to [0-9]\+ lines \*)
+(\* File reduced by coq-bug-minimizer from original input, then from [0-9]\+ lines to [0-9]\+ lines, then from [0-9]\+ lines to [0-9]\+ lines, then from [0-9]\+ lines to [0-9]\+ lines, then from [0-9]\+ lines to [0-9]\+ lines \*)
 (\* coqc version [^\*]*\*)
 
-Require Top\.Prop\.
-Import Top\.Prop\.
-
+Definition n := nat\.
 Fail Check n\.
 
 EOF

find-bug.py

@@ -1497,20 +1497,28 @@ def make_make_coqc(coqc_prog, **kwargs):
                         # because this is a bit more robust against
                         # future module inlining (see example test 45)
                         def get_test_output(absolutize_mods=False, first_wrap_then_include=True, without_require=True, insert_at_top=False):
-                            test_output = cur_output if not absolutize_mods else cur_output_gen({req_module: absolutize_and_mangle_libname(req_module, first_wrap_then_include=first_wrap_then_include)})
+                            new_req_module = absolutize_and_mangle_libname(req_module, first_wrap_then_include=first_wrap_then_include, **env)
+                            test_output = cur_output if not absolutize_mods else cur_output_gen({req_module: new_req_module})
+                            if not absolutize_mods:
+                                cur_rep = rep
+                            else:
+                                cur_rep = '\nRequire %s.\n' % new_req_module
+                            if cur_rep not in '\n' + test_output:
+                                env['log']('\nWarning: I cannot find Require %s.' % new_req_module)
+                                env['log']('in contents:\n' + test_output, level=3)
                             replacement = '\n' + get_required_contents(req_module, first_wrap_then_include=first_wrap_then_include, without_require=without_require, **env).strip() + '\n'
                             if without_require:
-                                all_imports = run_recursively_get_imports(req_module, **env) # like get_recursive_require_names, but with better sorting properties, I think, and also automatically strips off the self module
+                                all_imports = get_recursive_require_names(req_module, **env) # like run_recursively_get_imports, but get_recursive_require_names also strips off the self module
                                 replacement = '\n' + ''.join('Require %s.\n' % i for i in all_imports) + replacement
                             if insert_at_top:
                                 header, test_output = split_leading_comments_and_whitespace(test_output)
                                 return add_admit_tactic((
                                     header +
                                     replacement + '\n' +
-                                    ('\n' + test_output).replace(rep, '\n')).strip() + '\n',
+                                    ('\n' + test_output).replace(cur_rep, '\n')).strip() + '\n',
                                                         **env)
                             else:
-                                return ('\n' + test_output).replace(rep, replacement, 1).replace(rep, '\n').strip() + '\n'
+                                return ('\n' + test_output).replace(cur_rep, replacement, 1).replace(cur_rep, '\n').strip() + '\n'
                         test_output_alts = [
                             (((' without Include' if not first_wrap_then_include else ' via Include')
                               + (', absolutizing mod references' if absolutize_mods else '')

generate-full-grammar.py

@@ -0,0 +1,8 @@
+#!/usr/bin/env python3
+# invoke as
+# cat /path/to/coq/doc/tools/docgram/fullGrammar | ./generate-full-grammar.py > coq_full_grammar.py
+import sys, re
+print(r'''# autogenerated by cat /path/to/coq/doc/tools/docgram/fullGrammar | ./generate-full-grammar.py > coq_full_grammar.py
+__all__ = ["COQ_GRAMMAR_TOKENS"]
+
+COQ_GRAMMAR_TOKENS = %s''' % repr(sorted(set(i.strip('"') for i in re.findall('"[a-zA-Z_][^"]*"', sys.stdin.read())))).replace(' ', '\n'))

import_util.py

@@ -1,5 +1,6 @@
 from __future__ import with_statement, print_function
 import os, subprocess, re, sys, glob, os.path, tempfile, time
+from collections import OrderedDict
 from functools import cmp_to_key
 from memoize import memoize
 from coq_version import get_coqc_help, get_coq_accepts_o, group_coq_args_split_recognized, coq_makefile_supports_arg, group_coq_args
@@ -649,32 +650,37 @@ def transitively_close(d, make_new_value=(lambda x: tuple()), reflexive=True):
     return d
 
 def get_recursive_requires(*libnames, **kwargs):
+    reverse = kwargs.get('reverse', True)
     requires = dict((lib, get_require_names(lib, **kwargs)) for lib in libnames)
     transitively_close(requires, make_new_value=(lambda lib: get_require_names(lib, **kwargs)), reflexive=True)
-    return requires
-
-def get_recursive_require_names(libname, **kwargs):
-    return tuple(i for i in get_recursive_requires(libname, **kwargs).keys() if i != libname)
-
-def sort_files_by_dependency(filenames, reverse=True, **kwargs):
-    kwargs = fill_kwargs(kwargs)
-    filenames = map(fix_path, filenames)
-    filenames = [(filename + '.v' if filename[-2:] != '.v' else filename) for filename in filenames]
-    libnames = [lib_of_filename(filename, **kwargs) for filename in filenames]
-    requires = get_recursive_requires(*libnames, **kwargs)
-
-    def fcmp(f1, f2):
-        if f1 == f2: return cmp(f1, f2)
-        l1, l2 = lib_of_filename(f1, **kwargs), lib_of_filename(f2, **kwargs)
-        if l1 == l2: return cmp(f1, f2)
+    def lcmp(l1, l2):
+        l1, l2 = l1[0], l2[0] # strip off value part
+        if l1 == l2: return cmp(l1, l2)
         # this only works correctly if the closure is *reflexive* as
         # well as transitive, because we require that if A requires B,
         # then A must have strictly more requires than B (i.e., it
         # must include itself)
         if len(requires[l1]) != len(requires[l2]): return cmp(len(requires[l1]), len(requires[l2]))
         return cmp(l1, l2)
+    return OrderedDict(sorted(requires.items(), key=cmp_to_key(lcmp), reverse=reverse))
+
+def get_recursive_require_names(libname, **kwargs):
+    requires = get_recursive_requires(libname, **kwargs)
+    return tuple(i for i in requires.keys() if i != libname)
 
-    filenames = sorted(filenames, key=cmp_to_key(fcmp), reverse=reverse)
+def sort_files_by_dependency(filenames, reverse=True, **kwargs):
+    kwargs = fill_kwargs(kwargs)
+    filenames = map(fix_path, filenames)
+    filenames = [(filename + '.v' if filename[-2:] != '.v' else filename) for filename in filenames]
+    libname_map = dict((lib_of_filename(filename, **kwargs), filename) for filename in filenames)
+    requires = get_recursive_requires(*libname_map.keys(), reverse=reverse, **kwargs)
+    # filter the sorted requires by the ones that were in the original
+    # filenames list, and use libname_map to lookup the original
+    # filename.  We could probably just map filename_of_lib over the
+    # requires and keep the ones that are in the original filenames,
+    # but this is more robust if there are edge cases where
+    # filename_of_lib(lib_of_filename(x)) != x
+    filenames = [libname_map[libname] for libname in requires.keys() if libname in libname_map.keys()]
     return filenames
 
 def get_imports(lib, fast=False, **kwargs):

replace_imports.py

@@ -4,6 +4,7 @@
 from split_file import split_leading_comments_and_whitespace
 from import_util import filename_of_lib, lib_of_filename, get_file, run_recursively_get_imports, recursively_get_imports, absolutize_has_all_constants, is_local_import, ALL_ABSOLUTIZE_TUPLE, IMPORT_ABSOLUTIZE_TUPLE
 from custom_arguments import DEFAULT_LOG
+from coq_running_support import get_reserved_modnames
 
 __all__ = ["include_imports", "normalize_requires", "get_required_contents", "recursively_get_requires_from_file", "absolutize_and_mangle_libname"]
 
@@ -22,6 +23,7 @@ def fill_kwargs(kwargs, for_makefile=True):
         'libnames':DEFAULT_LIBNAMES,
         'non_recursive_libnames':tuple(),
         'coqc':'coqc',
+        'coqtop':'coqtop',
         'absolutize':ALL_ABSOLUTIZE_TUPLE,
         'coq_makefile':'coq_makefile'
     }
@@ -40,8 +42,12 @@ def contents_without_imports(lib, **kwargs):
         print('Warning: There are comments in your Require/Import/Export lines in %s.' % v_file)
     return IMPORT_LINE_REG.sub('', contents)
 
-def escape_lib(lib):
-    return lib.replace('.', '_DOT_').replace('-', '_DASH_')
+def escape_lib(lib, **kwargs):
+    reserved = get_reserved_modnames(kwargs['coqtop'], **kwargs)
+    lib = lib.replace('.', '_DOT_').replace('-', '_DASH_')
+    while lib in reserved:
+        lib = 'AVOID_RESERVED_' + lib
+    return lib
 
 def group_by_first_component(lib_libname_pairs):
     rtn = dict((lib.split('.')[0], []) for lib, libname in lib_libname_pairs)
@@ -57,20 +63,21 @@ def nest_iter_up_to(iterator):
         yield tuple(so_far)
 
 
-def construct_import_list(import_libs, import_all_directories=False):
+def construct_import_list(import_libs, import_all_directories=False, **kwargs):
     '''Takes a list of library names, and returns a list of imports in an order that should have modules representing files at the end.  If import_all_directories is true, then the resulting imports should handle semi-absolute constants, and not just fully absolute or fully relative ones.'''
+    def escape_lib_local(l): return escape_lib(l, **kwargs)
     if import_all_directories:
-        lib_components_list = [(libname, tuple(reversed(list(nest_iter_up_to(map(escape_lib, libname.split('.'))))[:-1])))
+        lib_components_list = [(libname, tuple(reversed(list(nest_iter_up_to(map(escape_lib_local, libname.split('.'))))[:-1])))
                                for libname in import_libs]
-        ret = list(map(escape_lib, import_libs))
+        ret = list(map(escape_lib_local, import_libs))
         lib_components = [(libname, i, max(map(len, lst)) - len(i))
                           for libname, lst in lib_components_list
                           for i in lst]
         for libname, components, components_left in reversed(sorted(lib_components, key=(lambda x: x[2]))):
-            ret.append(escape_lib(libname) + '.' + '.'.join(map(escape_lib, components)))
+            ret.append(escape_lib_local(libname) + '.' + '.'.join(map(escape_lib_local, components)))
         return ret
     else:
-        return map(escape_lib, import_libs)
+        return map(escape_lib_local, import_libs)
 
 def strip_requires(contents):
     reg1 = re.compile(r'^\s*Require\s+((?:Import|Export)\s)', flags=re.MULTILINE)
@@ -84,10 +91,11 @@ def strip_requires(contents):
     return contents
 
 
-def get_module_name_and_lib_parts(lib, first_wrap_then_include=False):
-    module_name = escape_lib(lib)
+def get_module_name_and_lib_parts(lib, first_wrap_then_include=False, **kwargs):
+    def escape_lib_local(libname): return escape_lib(libname, **kwargs)
+    module_name = escape_lib_local(lib)
     mangled_module_name = module_name + '_WRAPPED'
-    lib_parts = list(map(escape_lib, lib.split('.')))
+    lib_parts = list(map(escape_lib_local, lib.split('.')))
     # we could actually return the same thing, that is the string
     # ('%s.%s' % (module_name, '.'.join(lib_parts))), in both cases,
     # but we choose to return the module prior to Include rather than
@@ -100,8 +108,8 @@ def get_module_name_and_lib_parts(lib, first_wrap_then_include=False):
         full_module_name = '%s.%s' % (module_name, '.'.join(lib_parts))
     return module_name, mangled_module_name, lib_parts, full_module_name
 
-def absolutize_and_mangle_libname(lib, first_wrap_then_include=False):
-    module_name, mangled_module_name, lib_parts, full_module_name = get_module_name_and_lib_parts(lib, first_wrap_then_include=first_wrap_then_include)
+def absolutize_and_mangle_libname(lib, first_wrap_then_include=False, **kwargs):
+    module_name, mangled_module_name, lib_parts, full_module_name = get_module_name_and_lib_parts(lib, first_wrap_then_include=first_wrap_then_include, **kwargs)
     return full_module_name
 
 def contents_as_module(lib, other_imports, first_wrap_then_include=False, export=False, without_require=True, **kwargs):
@@ -111,18 +119,18 @@ def contents_as_module(lib, other_imports, first_wrap_then_include=False, export
         # that we use to fix
         # https://github.com/JasonGross/coq-tools/issues/67, so we disable it
         first_wrap_then_include = False
-        transform_base = lambda x: (escape_lib(x) + '.' + x if is_local_import(x, **kwargs) else x)
+        transform_base = lambda x: (escape_lib(x, **kwargs) + '.' + x if is_local_import(x, **kwargs) else x)
     else:
         transform_base = lambda x: x
     v_name = filename_of_lib(lib, ext='.v', **kwargs)
     contents = get_file(v_name, transform_base=transform_base, **kwargs)
     if without_require: contents = strip_requires(contents)
     kwargs['log'](contents, level=3)
-    module_name, mangled_module_name, lib_parts, _ = get_module_name_and_lib_parts(lib, first_wrap_then_include=first_wrap_then_include)
+    module_name, mangled_module_name, lib_parts, _ = get_module_name_and_lib_parts(lib, first_wrap_then_include=first_wrap_then_include, **kwargs)
     # import the top-level wrappers
     if len(other_imports) > 0 and not export:
         # we need to import the contents in the correct order.  Namely, if we have a module whose name is also the name of a directory (in the same folder), we want to import the file first.
-        for imp in reversed(construct_import_list(other_imports, import_all_directories=import_all_directories)):
+        for imp in reversed(construct_import_list(other_imports, import_all_directories=import_all_directories, **kwargs)):
             contents = 'Import %s.\n%s' % (imp, contents)
     # wrap the contents in directory modules
     maybe_export = 'Export ' if export else ''
@@ -218,7 +226,7 @@ def include_imports(filename, as_modules=True, fast=False, log=DEFAULT_LOG, coqc
     for import_name in all_imports:
         try:
             if as_modules:
-                rtn += contents_as_module(import_name, imports_done, log=log, absolutize=absolutize, without_require=True, **kwargs) + '\n'
+                rtn += contents_as_module(import_name, imports_done, log=log, absolutize=absolutize, without_require=True, coqc=coqc, **kwargs) + '\n'
             else:
                 rtn += contents_without_imports(import_name, log=log, absolutize=tuple(), **kwargs) + '\n'
             imports_done.append(import_name)