From 956e01a96e52f1ee943d9713709438e31b6488d5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 18 Oct 2024 18:25:19 -0700 Subject: [PATCH] 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 | 18 ++++++++++---- coq_tools/import_util.py | 52 ++++++++++++++++++++++++++++++---------- coq_tools/util.py | 8 +++++++ 3 files changed, 60 insertions(+), 18 deletions(-) diff --git a/coq_tools/find_bug.py b/coq_tools/find_bug.py index b489e46b..569face5 100755 --- a/coq_tools/find_bug.py +++ b/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())): diff --git a/coq_tools/import_util.py b/coq_tools/import_util.py index fabd373f..fc607655 100644 --- a/coq_tools/import_util.py +++ b/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,7 +645,7 @@ 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() @@ -652,13 +653,13 @@ def run_coq_makefile_and_make(v_files, targets, **kwargs): 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): diff --git a/coq_tools/util.py b/coq_tools/util.py index 2f6b11e1..af3cf65a 100644 --- a/coq_tools/util.py +++ b/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)):