Skip to content

Commit

Permalink
Warn when .glob files are clobbered (#232)
Browse files Browse the repository at this point in the history
  • Loading branch information
JasonGross authored Oct 17, 2024
1 parent 9af88b7 commit 3be8dc6
Showing 1 changed file with 7 additions and 1 deletion.
8 changes: 7 additions & 1 deletion coq_tools/import_util.py
Original file line number Diff line number Diff line change
Expand Up @@ -700,14 +700,20 @@ def make_one_glob_file(v_file, **kwargs):
cmds += list(get_maybe_passing_arg(kwargs, "coqc_args"))
v_file_root, ext = os.path.splitext(fix_path(v_file))
o_file = os.path.join(tempfile.gettempdir(), os.path.basename(v_file_root) + ".vo")
glob_file = v_file_root + ".glob"
if get_coq_accepts_o(coqc_prog, **kwargs):
cmds += ["-o", o_file]
else:
kwargs["log"](
"WARNING: Clobbering '%s' because coqc does not support -o" % o_file,
level=LOG_ALWAYS,
)
cmds += ["-dump-glob", v_file_root + ".glob", v_file_root + ext]
cmds += ["-dump-glob", glob_file, v_file_root + ext]
if os.path.exists(glob_file):
kwargs["log"](
f"WARNING: Clobbering '{glob_file}' ({os.path.getmtime(glob_file)}) from '{v_file_root + ext}' ({os.path.getmtime(v_file_root+ext)})",
level=LOG_ALWAYS,
)
kwargs["log"](" ".join(cmds))
try:
p = subprocess.Popen(cmds, stdout=subprocess.PIPE)
Expand Down

0 comments on commit 3be8dc6

Please sign in to comment.