Fix for making globs when coqc is coqtop

Previously handled only in fill_kwargs in replace_imports

coq_version.py

@@ -5,7 +5,7 @@
 from memoize import memoize
 import util
 
-__all__ = ["get_coqc_version", "get_coqtop_version", "get_coqc_help", "get_coqc_coqlib", "get_coq_accepts_top", "get_coq_accepts_time", "get_coq_accepts_o", "get_coq_native_compiler_ondemand_fragment", "group_coq_args_split_recognized", "group_coq_args", "coq_makefile_supports_arg", "get_proof_term_works_with_time", "get_ltac_support_snippet"]
+__all__ = ["get_coqc_version", "get_coqtop_version", "get_coqc_help", "get_coqc_coqlib", "get_coq_accepts_top", "get_coq_accepts_time", "get_coq_accepts_o", "get_coq_accepts_compile", "get_coq_native_compiler_ondemand_fragment", "group_coq_args_split_recognized", "group_coq_args", "coq_makefile_supports_arg", "get_proof_term_works_with_time", "get_ltac_support_snippet"]
 
 @memoize
 def get_coqc_version_helper(coqc):
@@ -73,6 +73,9 @@ def get_coq_accepts_time(coqc_prog, **kwargs):
 def get_coq_accepts_w(coqc_prog, **kwargs):
     return get_coq_accepts_option(coqc_prog, '-w', **kwargs)
 
+def get_coq_accepts_compile(coqc_prog, **kwargs):
+    return get_coq_accepts_option(coqc_prog, '-compile', **kwargs)
+
 @memoize
 def get_coqc_native_compiler_ondemand_errors(coqc):
     temp_file = tempfile.NamedTemporaryFile(suffix='.v', dir='.', delete=True)

find-bug.py

@@ -12,7 +12,7 @@
 from admit_abstract import transform_abstract_to_admit
 from import_util import lib_of_filename, clear_libimport_cache, IMPORT_ABSOLUTIZE_TUPLE, ALL_ABSOLUTIZE_TUPLE
 from memoize import memoize
-from coq_version import get_coqc_version, get_coqtop_version, get_coqc_help, get_coq_accepts_top, get_coq_native_compiler_ondemand_fragment, group_coq_args, get_ltac_support_snippet, get_coqc_coqlib
+from coq_version import get_coqc_version, get_coqtop_version, get_coqc_help, get_coq_accepts_top, get_coq_native_compiler_ondemand_fragment, group_coq_args, get_ltac_support_snippet, get_coqc_coqlib, get_coq_accepts_compile
 from custom_arguments import add_libname_arguments, add_passing_libname_arguments, update_env_with_libnames, update_env_with_coqpath_folders, add_logging_arguments, process_logging_arguments, DEFAULT_LOG, LOG_ALWAYS
 from binding_util import has_dir_binding, deduplicate_trailing_dir_bindings, process_maybe_list
 from file_util import clean_v_file, read_from_file, write_to_file, restore_file
@@ -1275,11 +1275,17 @@ def prepend_coqbin(prog):
         temp_file.close()
         env['remove_temp_file'] = True
 
+    def make_make_coqc(coqc_prog, **kwargs):
+        if get_coq_accepts_compile(coqc_prog, **kwargs): return os.path.join(SCRIPT_DIRECTORY, 'coqtop-as-coqc.sh') + ' ' + coqc_prog
+        if 'coqtop' in coqc_prog: return coqc_prog.replace('coqtop', 'coqc')
+        return 'coqc'
+
     if env['coqc_is_coqtop']:
         if env['coqc'] == 'coqc': env['coqc'] = env['coqtop']
-        env['make_coqc'] = os.path.join(SCRIPT_DIRECTORY, 'coqtop-as-coqc.sh') + ' ' + env['coqc']
+        env['make_coqc'] = make_make_coqc(env['coqc'], **env)
     if env['passing_coqc_is_coqtop']:
         if env['passing_coqc'] == 'coqc': env['passing_coqc'] = env['coqtop']
+        env['passing_make_coqc'] = make_make_coqc(env['passing_coqc'], **env)
 
     coqc_help = get_coqc_help(env['coqc'], **env)
     coqc_version = get_coqc_version(env['coqc'], **env)

import_util.py

@@ -30,7 +30,7 @@ def warning(*objs):
 def error(*objs):
     print("ERROR: ", *objs, file=sys.stderr)
 
-def fill_kwargs(kwargs):
+def fill_kwargs(kwargs, for_makefile=False):
     rtn = {
         'libnames'              : DEFAULT_LIBNAMES,
         'non_recursive_libnames': tuple(),
@@ -41,8 +41,13 @@ def fill_kwargs(kwargs):
         'walk_tree'             : True,
         'coqc_args'             : tuple(),
         'inline_coqlib'         : None,
-        }
+    }
     rtn.update(kwargs)
+    if for_makefile:
+        if 'make_coqc' in rtn.keys(): # handle the case where coqc for the makefile is different
+            rtn['coqc'] = rtn['make_coqc']
+        if 'passing_make_coqc' in rtn.keys(): # handle the case where coqc for the makefile is different
+            rtn['passing_coqc'] = rtn['passing_make_coqc']
     return rtn
 
 def safe_kwargs(kwargs):
@@ -298,7 +303,7 @@ def get_maybe_passing_arg(kwargs, key):
     return kwargs[key]
 
 def run_coq_makefile_and_make(v_files, targets, **kwargs):
-    kwargs = safe_kwargs(fill_kwargs(kwargs))
+    kwargs = safe_kwargs(fill_kwargs(kwargs, for_makefile=True))
     f = tempfile.NamedTemporaryFile(suffix='.coq', prefix='Makefile', dir='.', delete=False)
     mkfile = os.path.basename(f.name)
     f.close()

replace_imports.py

@@ -15,8 +15,8 @@
 
 IMPORT_LINE_REG = re.compile(r'^\s*(?:From|Require\s+Import|Require\s+Export|Require|Load\s+Verbose|Load)\s+(.*?)\.(?:\s|$)', re.MULTILINE | re.DOTALL)
 
-def fill_kwargs(kwargs):
-    defaults = {
+def fill_kwargs(kwargs, for_makefile=True):
+    rtn = {
         'fast':False,
         'log':DEFAULT_LOG,
         'libnames':DEFAULT_LIBNAMES,
@@ -25,12 +25,13 @@ def fill_kwargs(kwargs):
         'absolutize':ALL_ABSOLUTIZE_TUPLE,
         'coq_makefile':'coq_makefile'
     }
-    for k, v in defaults.items():
-        if k not in kwargs.keys():
-            kwargs[k] = v
-    if 'make_coqc' in kwargs.keys(): # handle the case where coqc for the makefile is different
-        kwargs['coqc'] = kwargs['make_coqc']
-    return kwargs
+    rtn.update(kwargs)
+    if for_makefile:
+        if 'make_coqc' in rtn.keys(): # handle the case where coqc for the makefile is different
+            rtn['coqc'] = rtn['make_coqc']
+        if 'passing_make_coqc' in rtn.keys(): # handle the case where coqc for the makefile is different
+            rtn['passing_coqc'] = rtn['passing_make_coqc']
+    return rtn
 
 def contents_without_imports(lib, **kwargs):
     v_file = filename_of_lib(lib, ext='.v', **kwargs)