Add --coqlib, --passing-coqlib

In preparation for threading them through more explicitly.

Author: JasonGross

coq_tools/custom_arguments.py

@@ -152,6 +152,13 @@ def add_libname_arguments_gen(parser, passing):
         help='Arguments to pass to coqc and coqtop; e.g., " -indices-matter" (leading and trailing spaces are stripped)'
         + passing_for,
     )
+    parser.add_argument(
+        twodash_passing_dash + "coqlib",
+        metavar="COQLIB",
+        dest=passing_underscore + "coqlib",
+        type=str,
+        help="Coqlib argument to pass to Coq" + passing_for,
+    )
     parser.add_argument(
         onedash_passing_dash + "f",
         metavar="FILE",
@@ -268,9 +275,13 @@ def argstring_to_iterable(arg):
     return arg.split(" ")
 
 
-def append_coq_arg(env, arg, passing=""):
+def append_coq_args_raw(env, *args, passing=""):
     for key in ("coqc_args", "coqtop_args"):
-        env[passing + key] = tuple(list(env.get(passing + key, [])) + list(argstring_to_iterable(arg)))
+        env[passing + key] = tuple(list(env.get(passing + key, [])) + list(args))
+
+
+def append_coq_arg(env, arg, passing=""):
+    append_coq_args_raw(env, *argstring_to_iterable(arg), passing=passing)
 
 
 def process_CoqProject(env, contents, passing=""):
@@ -370,6 +381,11 @@ def do_with_path(path):
                 do_with_path(coqpath if coqpath != "" else ".")
 
 
+def update_env_with_coqlib(passing_prefix, env):
+    if env.get(passing_prefix + "coqlib"):
+        append_coq_args_raw(env, "-coqlib", env[passing_prefix + "coqlib"], passing=passing_prefix)
+
+
 # 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):

coq_tools/find_bug.py

@@ -44,6 +44,7 @@
     add_passing_libname_arguments,
     update_env_with_libnames,
     update_env_with_coqpath_folders,
+    update_env_with_coqlib,
     add_logging_arguments,
     process_logging_arguments,
     get_parser_name_mapping,
@@ -2085,6 +2086,8 @@ def prepend_coqbin(prog):
         "admit_obligations": args.admit_obligations and args.admit_any,
         "aggressive": args.aggressive,
         "admit_transparent": args.admit_transparent and args.admit_any,
+        "coqlib": args.coqlib,
+        "passing_coqlib": args.passing_coqlib,
         "coqc_args": tuple(
             i.strip()
             for i in (
@@ -2189,6 +2192,9 @@ def prepend_coqbin(prog):
         if env["temp_file_log_name"] == "":
             env["temp_file_log_name"] = env["temp_file_name"] + ".log"
 
+        for passing_prefix in ("", "passing_"):
+            update_env_with_coqlib(env=env, passing_prefix=passing_prefix)
+
         def make_make_coqc(coqc_prog, **kwargs):
             if get_coq_accepts_compile(coqc_prog):
                 return f"{util.resource_path('coqtop-as-coqc.sh')} {coqc_prog}"

coq_tools/inline_imports.py

@@ -7,6 +7,7 @@
     update_env_with_libnames,
     update_env_with_coqpath_folders,
     add_logging_arguments,
+    update_env_with_coqlib,
     process_logging_arguments,
     get_parser_name_mapping,
 )
@@ -141,6 +142,7 @@ def main():
         "walk_tree": args.walk_tree,
         "cli_mapping": get_parser_name_mapping(parser),
     }
+    update_env_with_coqlib("", env)
     update_env_with_libnames(env, args)
     if args.inline_user_contrib:
         update_env_with_coqpath_folders(