Skip to content

Commit 0fe4a40

Browse files
JasonGrossJasonGross
committed
Add --coqlib, --passing-coqlib
In preparation for threading them through more explicitly.
1 parent 65e0924 commit 0fe4a40

File tree

2 files changed

+138
-122
lines changed

2 files changed

+138
-122
lines changed

‎coq_tools/custom_arguments.py‎

Lines changed: 18 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -152,6 +152,13 @@ def add_libname_arguments_gen(parser, passing):
152152
help='Arguments to pass to coqc and coqtop; e.g., " -indices-matter" (leading and trailing spaces are stripped)'
153153
+ passing_for,
154154
)
155+
parser.add_argument(
156+
twodash_passing_dash + "coqlib",
157+
metavar="COQLIB",
158+
dest=passing_underscore + "coqlib",
159+
type=str,
160+
help="Coqlib argument to pass to Coq" + passing_for,
161+
)
155162
parser.add_argument(
156163
onedash_passing_dash + "f",
157164
metavar="FILE",
@@ -268,9 +275,13 @@ def argstring_to_iterable(arg):
268275
return arg.split(" ")
269276

270277

271-
def append_coq_arg(env, arg, passing=""):
278+
def append_coq_args_raw(env, *args, passing=""):
272279
for key in ("coqc_args", "coqtop_args"):
273-
env[passing + key] = tuple(list(env.get(passing + key, [])) + list(argstring_to_iterable(arg)))
280+
env[passing + key] = tuple(list(env.get(passing + key, [])) + list(args))
281+
282+
283+
def append_coq_arg(env, arg, passing=""):
284+
append_coq_args_raw(env, *argstring_to_iterable(arg), passing=passing)
274285

275286

276287
def process_CoqProject(env, contents, passing=""):
@@ -370,6 +381,11 @@ def do_with_path(path):
370381
do_with_path(coqpath if coqpath != "" else ".")
371382

372383

384+
def update_env_with_coqlib(passing_prefix, env):
385+
if env.get(passing_prefix + "coqlib"):
386+
append_coq_args_raw(env, "-coqlib", env[passing_prefix + "coqlib"], passing=passing_prefix)
387+
388+
373389
# http://stackoverflow.com/questions/5943249/python-argparse-and-controlling-overriding-the-exit-status-code
374390
class ArgumentParser(argparse.ArgumentParser):
375391
def _get_action_from_name(self, name):

‎coq_tools/find_bug.py‎

Lines changed: 120 additions & 120 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,7 @@
4444
add_passing_libname_arguments,
4545
update_env_with_libnames,
4646
update_env_with_coqpath_folders,
47+
update_env_with_coqlib,
4748
add_logging_arguments,
4849
process_logging_arguments,
4950
get_parser_name_mapping,
@@ -2085,6 +2086,8 @@ def prepend_coqbin(prog):
20852086
"admit_obligations": args.admit_obligations and args.admit_any,
20862087
"aggressive": args.aggressive,
20872088
"admit_transparent": args.admit_transparent and args.admit_any,
2089+
"coqlib": args.coqlib,
2090+
"passing_coqlib": args.passing_coqlib,
20882091
"coqc_args": tuple(
20892092
i.strip()
20902093
for i in (
@@ -2151,145 +2154,142 @@ def prepend_coqbin(prog):
21512154
"cli_mapping": get_parser_name_mapping(parser),
21522155
}
21532156

2154-
if bug_file_name[-2:] != ".v":
2155-
env["log"](
2156-
"\nError: BUGGY_FILE must end in .v (value: %s)" % bug_file_name, force_stdout=True, level=LOG_ALWAYS
2157-
)
2158-
sys.exit(1)
2159-
if output_file_name[-2:] != ".v":
2160-
env["log"](
2161-
"\nError: OUT_FILE must end in .v (value: %s)" % output_file_name, force_stdout=True, level=LOG_ALWAYS
2162-
)
2163-
sys.exit(1)
2164-
if os.path.exists(output_file_name):
2165-
env["log"](
2166-
"\nWarning: OUT_FILE (%s) already exists. Would you like to overwrite?\n" % output_file_name,
2167-
force_stdout=True,
2168-
level=LOG_ALWAYS,
2169-
)
2170-
if not yes_no_prompt(yes=env["yes"]):
2157+
try:
2158+
2159+
if bug_file_name[-2:] != ".v":
2160+
env["log"](
2161+
"\nError: BUGGY_FILE must end in .v (value: %s)" % bug_file_name, force_stdout=True, level=LOG_ALWAYS
2162+
)
2163+
sys.exit(1)
2164+
if output_file_name[-2:] != ".v":
2165+
env["log"](
2166+
"\nError: OUT_FILE must end in .v (value: %s)" % output_file_name, force_stdout=True, level=LOG_ALWAYS
2167+
)
21712168
sys.exit(1)
2172-
for k, arg in (("base_dir", "--base-dir"), ("passing_base_dir", "--passing-base-dir")):
2173-
if env[k] is not None and not os.path.isdir(env[k]):
2169+
if os.path.exists(output_file_name):
21742170
env["log"](
2175-
"\nError: Argument to %s (%s) must exist and be a directory." % (arg, env[k]),
2171+
"\nWarning: OUT_FILE (%s) already exists. Would you like to overwrite?\n" % output_file_name,
21762172
force_stdout=True,
21772173
level=LOG_ALWAYS,
21782174
)
2179-
sys.exit(1)
2180-
2181-
env["remove_temp_file"] = False
2182-
if env["temp_file_name"] == "":
2183-
temp_file = tempfile.NamedTemporaryFile(suffix=".v", dir=".", delete=False)
2184-
env["temp_file_name"] = temp_file.name
2185-
temp_file.close()
2186-
env["remove_temp_file"] = True
2187-
if env["temp_file_log_name"] == "":
2188-
env["temp_file_log_name"] = env["temp_file_name"] + ".log"
2189-
2190-
def make_make_coqc(coqc_prog, **kwargs):
2191-
if get_coq_accepts_compile(coqc_prog):
2192-
return f"{util.resource_path('coqtop-as-coqc.sh')} {coqc_prog}"
2193-
if "coqtop" in coqc_prog:
2194-
return coqc_prog.replace("coqtop", "coqc")
2195-
return "coqc"
2196-
2197-
if env["coqc_is_coqtop"]:
2198-
if env["coqc"] == "coqc":
2199-
env["coqc"] = env["coqtop"]
2200-
env["make_coqc"] = make_make_coqc(env["coqc"], **env)
2201-
if env["passing_coqc_is_coqtop"]:
2202-
if env["passing_coqc"] == "coqc":
2203-
if env["passing_coqtop"] is not None:
2204-
env["passing_coqc"] = env["passing_coqtop"]
2205-
else:
2206-
env["passing_coqc"] = env["coqtop"]
2207-
env["passing_make_coqc"] = make_make_coqc(env["passing_coqc"], **env)
2208-
2209-
coqc_help = get_coqc_help(get_preferred_passing("coqc", **env), **env)
2210-
coqc_version = get_coqc_version(env["coqc"], **env)
2175+
if not yes_no_prompt(yes=env["yes"]):
2176+
sys.exit(1)
2177+
for k, arg in (("base_dir", "--base-dir"), ("passing_base_dir", "--passing-base-dir")):
2178+
if env[k] is not None and not os.path.isdir(env[k]):
2179+
env["log"](
2180+
"\nError: Argument to %s (%s) must exist and be a directory." % (arg, env[k]),
2181+
force_stdout=True,
2182+
level=LOG_ALWAYS,
2183+
)
2184+
sys.exit(1)
22112185

2212-
update_env_with_libnames(
2213-
env,
2214-
args,
2215-
include_passing=env["passing_coqc"],
2216-
use_default=not has_dir_binding(env["coqc_args"], coqc_help=coqc_help, file_name=bug_file_name),
2217-
use_passing_default=not has_dir_binding(env["passing_coqc_args"], coqc_help=coqc_help, file_name=bug_file_name),
2218-
)
2186+
env["remove_temp_file"] = False
2187+
if env["temp_file_name"] == "":
2188+
temp_file = tempfile.NamedTemporaryFile(suffix=".v", dir=".", delete=False)
2189+
env["temp_file_name"] = temp_file.name
2190+
temp_file.close()
2191+
env["remove_temp_file"] = True
2192+
if env["temp_file_log_name"] == "":
2193+
env["temp_file_log_name"] = env["temp_file_name"] + ".log"
22192194

2220-
if args.inline_user_contrib:
22212195
for passing_prefix in ("", "passing_"):
2222-
if env[passing_prefix + "coqc"]:
2223-
coq_user_contrib_path = os.path.join(
2224-
get_coqc_coqlib(
2225-
env[passing_prefix + "coqc"], coq_args=env[passing_prefix + "coqc_args"], **env
2226-
),
2227-
"user-contrib",
2196+
update_env_with_coqlib(env, passing_prefix=passing_prefix)
2197+
2198+
def make_make_coqc(coqc_prog, **kwargs):
2199+
if get_coq_accepts_compile(coqc_prog):
2200+
return f"{util.resource_path('coqtop-as-coqc.sh')} {coqc_prog}"
2201+
if "coqtop" in coqc_prog:
2202+
return coqc_prog.replace("coqtop", "coqc")
2203+
return "coqc"
2204+
2205+
if env["coqc_is_coqtop"]:
2206+
if env["coqc"] == "coqc":
2207+
env["coqc"] = env["coqtop"]
2208+
env["make_coqc"] = make_make_coqc(env["coqc"], **env)
2209+
if env["passing_coqc_is_coqtop"]:
2210+
if env["passing_coqc"] == "coqc":
2211+
if env["passing_coqtop"] is not None:
2212+
env["passing_coqc"] = env["passing_coqtop"]
2213+
else:
2214+
env["passing_coqc"] = env["coqtop"]
2215+
env["passing_make_coqc"] = make_make_coqc(env["passing_coqc"], **env)
2216+
2217+
coqc_help = get_coqc_help(get_preferred_passing("coqc", **env), **env)
2218+
coqc_version = get_coqc_version(env["coqc"], **env)
2219+
2220+
update_env_with_libnames(
2221+
env,
2222+
args,
2223+
include_passing=env["passing_coqc"],
2224+
use_default=not has_dir_binding(env["coqc_args"], coqc_help=coqc_help, file_name=bug_file_name),
2225+
use_passing_default=not has_dir_binding(env["passing_coqc_args"], coqc_help=coqc_help, file_name=bug_file_name),
2226+
)
2227+
2228+
if args.inline_user_contrib:
2229+
for passing_prefix in ("", "passing_"):
2230+
if env[passing_prefix + "coqc"]:
2231+
coq_user_contrib_path = os.path.join(
2232+
get_coqc_coqlib(
2233+
env[passing_prefix + "coqc"], coq_args=env[passing_prefix + "coqc_args"], **env
2234+
),
2235+
"user-contrib",
2236+
)
2237+
update_env_with_coqpath_folders(
2238+
passing_prefix,
2239+
env,
2240+
coq_user_contrib_path,
22282241
)
2229-
update_env_with_coqpath_folders(
2230-
passing_prefix,
2231-
env,
2232-
coq_user_contrib_path,
2233-
)
2234-
env[passing_prefix + "coqpath_paths"].append(coq_user_contrib_path)
2242+
env[passing_prefix + "coqpath_paths"].append(coq_user_contrib_path)
22352243

2236-
if args.inline_coqlib or args.inline_stdlib:
2237-
for passing_prefix in ("", "passing_"):
2238-
if env[passing_prefix + "coqc"]:
2239-
coq_lib_path = get_coqc_coqlib(
2240-
env[passing_prefix + "coqc"], coq_args=env[passing_prefix + "coqc_args"], **env
2241-
)
2242-
coq_theories_path = os.path.join(coq_lib_path, "theories")
2243-
coq_user_contrib_path = os.path.join(os.path.join(coq_lib_path, "user-contrib"), "Stdlib")
2244-
coqpath_path = os.environ.get('COQPATH', '')
2245-
coqpath_paths = coqpath_path.split(os.pathsep) if coqpath_path else []
2246-
if args.inline_coqlib:
2247-
if coqc_version != "" and coqc_version[0] == '8':
2244+
if args.inline_coqlib or args.inline_stdlib:
2245+
for passing_prefix in ("", "passing_"):
2246+
if env[passing_prefix + "coqc"]:
2247+
coq_lib_path = get_coqc_coqlib(
2248+
env[passing_prefix + "coqc"], coq_args=env[passing_prefix + "coqc_args"], **env
2249+
)
2250+
coq_theories_path = os.path.join(coq_lib_path, "theories")
2251+
coq_user_contrib_path = os.path.join(os.path.join(coq_lib_path, "user-contrib"), "Stdlib")
2252+
coqpath_paths = os.environ.get('COQPATH', '').split(os.pathsep)
2253+
if args.inline_coqlib:
22482254
env[passing_prefix + "libnames"] = tuple(
22492255
list(env[passing_prefix + "libnames"]) + [(coq_theories_path, "Coq")]
22502256
)
2251-
else:
22522257
env[passing_prefix + "libnames"] = tuple(
2253-
list(env[passing_prefix + "libnames"]) + [(coq_theories_path, "Corelib")]
2258+
list(env[passing_prefix + "libnames"]) + [(coq_user_contrib_path, "Coq")]
22542259
)
2255-
env[passing_prefix + "libnames"] = tuple(
2256-
list(env[passing_prefix + "libnames"]) + [(coq_user_contrib_path, "Stdlib")]
2257-
)
2258-
for p in coqpath_paths:
2260+
for p in coqpath_paths:
2261+
env[passing_prefix + "libnames"] = tuple(
2262+
list(env[passing_prefix + "libnames"]) + [(os.path.join(p, "Stdlib"), "Coq")]
2263+
)
2264+
if args.inline_stdlib:
22592265
env[passing_prefix + "libnames"] = tuple(
2260-
list(env[passing_prefix + "libnames"]) + [(os.path.join(p, "Stdlib"), "Coq")]
2266+
list(env[passing_prefix + "libnames"]) + [(coq_theories_path, "Stdlib")]
22612267
)
2262-
if args.inline_stdlib:
2263-
env[passing_prefix + "libnames"] = tuple(
2264-
list(env[passing_prefix + "libnames"]) + [(coq_theories_path, "Stdlib")]
2265-
)
2266-
env[passing_prefix + "libnames"] = tuple(
2267-
list(env[passing_prefix + "libnames"]) + [(coq_user_contrib_path, "Stdlib")]
2268-
)
2269-
for p in coqpath_paths:
22702268
env[passing_prefix + "libnames"] = tuple(
2271-
list(env[passing_prefix + "libnames"]) + [(os.path.join(p, "Stdlib"), "Stdlib")]
2269+
list(env[passing_prefix + "libnames"]) + [(coq_user_contrib_path, "Stdlib")]
22722270
)
2273-
if args.inline_coqlib or args.inline_stdlib:
2274-
env[passing_prefix + "coqpath_paths"].append(coq_theories_path)
2275-
env[passing_prefix + "coqpath_paths"].append(coq_user_contrib_path)
2276-
env[passing_prefix + "coqpath_paths"].extend(coqpath_paths)
2277-
2278-
env["log"]("{", level=2)
2279-
for k, v in sorted(list(env.items())):
2280-
env["log"](" %s: %s" % (repr(k), repr(v)), level=2)
2281-
env["log"]("}", level=2)
2282-
2283-
for passing_prefix in ("", "passing_"):
2284-
if env[passing_prefix + "coqc"]:
2285-
args_key = passing_prefix + "coqc_args"
2286-
if "-native-compiler" not in env[args_key]:
2287-
env[args_key] = tuple(
2288-
list(env[args_key])
2289-
+ list(get_coq_native_compiler_ondemand_fragment(env[passing_prefix + "coqc"], **env))
2290-
)
2271+
for p in coqpath_paths:
2272+
env[passing_prefix + "libnames"] = tuple(
2273+
list(env[passing_prefix + "libnames"]) + [(os.path.join(p, "Stdlib"), "Stdlib")]
2274+
)
2275+
if args.inline_coqlib or args.inline_stdlib:
2276+
env[passing_prefix + "coqpath_paths"].append(coq_theories_path)
2277+
env[passing_prefix + "coqpath_paths"].append(coq_user_contrib_path)
2278+
env[passing_prefix + "coqpath_paths"].extend(coqpath_paths)
22912279

2292-
try:
2280+
env["log"]("{", level=2)
2281+
for k, v in sorted(list(env.items())):
2282+
env["log"](" %s: %s" % (repr(k), repr(v)), level=2)
2283+
env["log"]("}", level=2)
2284+
2285+
for passing_prefix in ("", "passing_"):
2286+
if env[passing_prefix + "coqc"]:
2287+
args_key = passing_prefix + "coqc_args"
2288+
if "-native-compiler" not in env[args_key]:
2289+
env[args_key] = tuple(
2290+
list(env[args_key])
2291+
+ list(get_coq_native_compiler_ondemand_fragment(env[passing_prefix + "coqc"], **env))
2292+
)
22932293

22942294
if env["temp_file_name"][-2:] != ".v":
22952295
env["log"](
@@ -2614,7 +2614,7 @@ def get_test_output(
26142614
env["log"](traceback.format_exc(), level=LOG_ALWAYS)
26152615
raise
26162616
finally:
2617-
if env["remove_temp_file"]:
2617+
if env.get("remove_temp_file"):
26182618
clean_v_file(env["temp_file_name"])
26192619
if os.path.exists(env["temp_file_log_name"]):
26202620
os.remove(env["temp_file_log_name"])

0 commit comments

Comments
 (0)