Hack to work around lack of installed .glob (#236)

We add -R for user-contrib developments only in cases where coqc fails.

coq_tools/find_bug.py

@@ -2140,6 +2140,8 @@ def prepend_coqbin(prog):
         "temp_file_log_name": args.temp_file_log,
         "coqc_is_coqtop": args.coqc_is_coqtop,
         "passing_coqc_is_coqtop": args.passing_coqc_is_coqtop,
+        "coqpath_paths": [],
+        "passing_coqpath_paths": [],
         "yes": args.yes,
         "color_on": args.color_on,
         "inline_failure_libnames": [],
@@ -2218,16 +2220,18 @@ def make_make_coqc(coqc_prog, **kwargs):
     if args.inline_user_contrib:
         for passing_prefix in ("", "passing_"):
             if env[passing_prefix + "coqc"]:
-                update_env_with_coqpath_folders(
-                    passing_prefix,
-                    env,
-                    os.path.join(
+                coq_user_contrib_path = os.path.join(
                         get_coqc_coqlib(
                             env[passing_prefix + "coqc"], coq_args=env[passing_prefix + "coqc_args"], **env
                         ),
                         "user-contrib",
-                    ),
+                    )
+                update_env_with_coqpath_folders(
+                    passing_prefix,
+                    env,
+                    coq_user_contrib_path,
                 )
+                env[passing_prefix + "coqpath_paths"].append(coq_user_contrib_path)
 
     if args.inline_coqlib or args.inline_stdlib:
         for passing_prefix in ("", "passing_"):
@@ -2260,6 +2264,10 @@ def make_make_coqc(coqc_prog, **kwargs):
                         env[passing_prefix + "libnames"] = tuple(
                             list(env[passing_prefix + "libnames"]) + [(os.path.join(p, "Stdlib"), "Stdlib")]
                         )
+                if args.inline_coqlib or args.inline_stdlib:
+                    env[passing_prefix + "coqpath_paths"].append(coq_theories_path)
+                    env[passing_prefix + "coqpath_paths"].append(coq_user_contrib_path)
+                    env[passing_prefix + "coqpath_paths"].extend(coqpath_paths)
 
     env["log"]("{", level=2)
     for k, v in sorted(list(env.items())):

coq_tools/import_util.py

@@ -25,7 +25,7 @@
 from .split_file import get_coq_statement_byte_ranges, split_coq_file_contents
 from .strip_comments import strip_comments, strip_trailing_comments
 from .util import cmp_compat as cmp
-from .util import shlex_quote
+from .util import shlex_quote, shlex_join
 
 __all__ = [
     "filename_of_lib",
@@ -118,6 +118,7 @@ def fill_kwargs(kwargs, for_makefile=False):
         "cli_mapping": {
             "use_coq_makefile_for_deps": {False: ["--no-deps"]},
         },
+        "coqpath_paths": tuple(),
     }
     rtn.update(kwargs)
     if for_makefile:
@@ -644,21 +645,21 @@ def run_coq_makefile_and_make(v_files, targets, **kwargs):
         else:
             kwargs["log"]("WARNING: Unrecognized arguments to coq_makefile: %s" % repr(unrecognized_args))
     cmds += list(map(fix_path, v_files))
-    kwargs["log"](" ".join(cmds))
+    kwargs["log"](shlex_join(cmds))
     try:
         p_make_makefile = subprocess.Popen(cmds, stdout=subprocess.PIPE)
         (stdout, stderr) = p_make_makefile.communicate()
     except OSError as e:
         error("When attempting to run coq_makefile:")
         error(repr(e))
         error("Failed to run coq_makefile using command line:")
-        error(" ".join(cmds))
+        error(shlex_join(cmds))
         error("Perhaps you forgot to add COQBIN to your PATH?")
         error("Try running coqc on your files to get .glob files, to work around this.")
         sys.exit(1)
     keep_error_fragment = [] if get_keep_error_reversed(mkfile, **kwargs) else ["KEEP_ERROR=1"]
     make_cmds = ["make", "-k", "-f", mkfile] + keep_error_fragment + targets
-    kwargs["log"](" ".join(make_cmds))
+    kwargs["log"](shlex_join(make_cmds))
     try:
         p_make = subprocess.Popen(
             make_cmds,
@@ -683,6 +684,7 @@ def run_coq_makefile_and_make(v_files, targets, **kwargs):
 def make_one_glob_file(v_file, clobber_glob_on_failure: bool = True, **kwargs):
     kwargs = safe_kwargs(fill_kwargs(kwargs))
     coqc_prog = get_maybe_passing_arg(kwargs, "coqc")
+    coqpath_paths = get_maybe_passing_arg(kwargs, "coqpath_paths")
     cmds = [coqc_prog, "-q"]
     for physical_name, logical_name in get_maybe_passing_arg(kwargs, "libnames"):
         cmds += [
@@ -699,7 +701,8 @@ def make_one_glob_file(v_file, clobber_glob_on_failure: bool = True, **kwargs):
     for dirname in get_maybe_passing_arg(kwargs, "ocaml_dirnames"):
         cmds += ["-I", dirname]
     cmds += list(get_maybe_passing_arg(kwargs, "coqc_args"))
-    v_file_root, ext = os.path.splitext(fix_path(v_file))
+    v_file = fix_path(v_file)
+    v_file_root, ext = os.path.splitext(v_file)
     o_file = os.path.join(tempfile.gettempdir(), os.path.basename(v_file_root) + ".vo")
     tmp_glob_file = os.path.join(tempfile.gettempdir(), os.path.basename(v_file_root) + ".glob")
     glob_file = v_file_root + ".glob"
@@ -710,18 +713,37 @@ def make_one_glob_file(v_file, clobber_glob_on_failure: bool = True, **kwargs):
             "WARNING: Clobbering '%s' because coqc does not support -o" % o_file,
             level=LOG_ALWAYS,
         )
-    cmds += ["-dump-glob", tmp_glob_file, v_file_root + ext]
-    kwargs["log"](" ".join(cmds))
+    cmds += ["-dump-glob", tmp_glob_file, v_file]
+    # if the file has user-contrib in it, we may try to its local paths with -R for more robustness
+    extra_cmds_options = []
+    v_file_in_coqpaths = [p for p in coqpath_paths if is_subdirectory_of(v_file, p)]
+    # sort the paths by length of absolute path so that we try the longest paths first
+    v_file_in_coqpaths.sort(key=lambda p: len(os.path.abspath(p)), reverse=True)
+    for coqpath_path in v_file_in_coqpaths:
+        relative_path = os.path.relpath(v_file, coqpath_path)
+        first_component = fix_path(relative_path).split("/")[0]
+        extra_cmds_options.append(["-R", os.path.join(coqpath_path, first_component), first_component])
+    kwargs["log"](shlex_join(cmds))
     try:
         p = subprocess.Popen(cmds, stdout=subprocess.PIPE)
         stdout, stderr = p.communicate()
+        for extra_cmds in extra_cmds_options:
+            if p.returncode == 0:
+                break
+            kwargs["log"](
+                "WARNING: coqc failed on '%s', retrying with extra %s" % (v_file, shlex_join(extra_cmds)),
+                level=LOG_ALWAYS,
+            )
+            kwargs["log"](shlex_join(cmds + extra_cmds))
+            p = subprocess.Popen(cmds + extra_cmds, stdout=subprocess.PIPE)
+            stdout, stderr = p.communicate()
         if os.path.exists(tmp_glob_file) and (
             p.returncode == 0 or not os.path.exists(glob_file) or clobber_glob_on_failure
         ):
             if os.path.exists(glob_file):
                 extra = " despite failure of coqc" if p.returncode != 0 else " because coqc succeeded"
                 kwargs["log"](
-                    f"WARNING: Clobbering '{glob_file}' ({os.path.getmtime(glob_file)}) from '{v_file_root + ext}' ({os.path.getmtime(v_file_root+ext)}){extra}",
+                    f"WARNING: Clobbering '{glob_file}' ({os.path.getmtime(glob_file)}) from '{v_file}' ({os.path.getmtime(v_file_root+ext)}){extra}",
                     level=LOG_ALWAYS,
                 )
             else:
@@ -735,7 +757,7 @@ def make_one_glob_file(v_file, clobber_glob_on_failure: bool = True, **kwargs):
                 )
         elif os.path.exists(tmp_glob_file):
             kwargs["log"](
-                f"WARNING: Not clobbering '{glob_file}' ({os.path.getmtime(glob_file)}) because coqc failed on '{v_file_root + ext}' ({os.path.getmtime(v_file_root+ext)})",
+                f"WARNING: Not clobbering '{glob_file}' ({os.path.getmtime(glob_file)}) because coqc failed on '{v_file}' ({os.path.getmtime(v_file_root+ext)})",
                 level=LOG_ALWAYS,
             )
         return stdout, stderr
@@ -746,11 +768,15 @@ def make_one_glob_file(v_file, clobber_glob_on_failure: bool = True, **kwargs):
             os.remove(tmp_glob_file)
 
 
+def is_subdirectory_of(filename, parent):
+    abs_filename = os.path.normpath(os.path.abspath(filename))
+    parent = os.path.normpath(os.path.abspath(parent))
+    common = os.path.normpath(os.path.commonprefix([parent, abs_filename]))
+    return common == parent
+
+
 def is_local(filename):
-    abs_filename = os.path.abspath(filename)
-    cwd = os.path.abspath(".")
-    common = os.path.commonprefix([cwd, abs_filename])
-    return common == cwd
+    return is_subdirectory_of(filename, ".")
 
 
 def remove_if_local(filename, **kwargs):

coq_tools/util.py

@@ -12,6 +12,7 @@
     "slice_string_at_bytes",
     "len_in_bytes",
     "shlex_quote",
+    "shlex_join",
     "resource_path",
     "group_by",
 ]
@@ -166,6 +167,13 @@ def color(str, col, on=True):
 
     shlex_quote = shlex.quote
 
+if sys.version_info < (3, 8):
+    shlex_join = lambda split_command: " ".join(shlex_quote(arg) for arg in split_command)
+else:
+    import shlex
+
+    shlex_join = shlex.join
+
 
 def resource_path(path):
     if os.path.exists(os.path.join(SCRIPT_DIRECTORY, path)):