Add native Python coqchk support to find_bug.py

- Add get_coqchk_help and get_coqchk_version functions to coq_version.py
- Add coqchk_prog and coqchk_prog_args parameters to get_coq_output in diagnose_error.py
- Process coqchk output with Fatal Error handling
- Add --coqchk-args, --nonpassing-coqchk-args, --passing-coqchk-args CLI options
- Set coqchk/passing_coqchk to None when --chk is not specified
- Pass coqchk_prog and coqchk_prog_args explicitly to all get_coq_output calls
- Extend argument processing loops to handle coqchk args similar to coqtop

Author: JasonGross

coq_tools/custom_arguments.py

@@ -413,7 +413,7 @@ def argstring_to_iterable(arg):
 
 
 def append_coq_arg(env, arg, passing=""):
-    for key in ("coqc_args", "coqtop_args"):
+    for key in ("coqc_args", "coqtop_args", "coqchk_args"):
         env[passing + key] = tuple(
             list(env.get(passing + key, [])) + list(argstring_to_iterable(arg))
         )

coq_tools/diagnose_error.py

@@ -5,7 +5,11 @@
 from .file_util import clean_v_file
 from .util import re_escape, get_peak_rss_bytes, apply_memory_limit, cleanup_cgroup
 from .custom_arguments import LOG_ALWAYS
-from .coq_version import group_coq_args, get_coqc_help, get_coq_accepts_Q
+from .coq_version import (
+    group_coq_args,
+    get_coqc_help,
+    get_coq_accepts_Q,
+)
 from . import util
 
 __all__ = [
@@ -42,6 +46,26 @@ def clean_output(output):
     return adjust_error_message_for_selected_errors(util.normalize_newlines(output))
 
 
+def process_coqchk_output(output, v_file_name, line_count):
+    """
+    Process coqchk output and insert error preamble before "Fatal Error:" lines.
+
+    When coqchk outputs a line starting with "Fatal Error:", we emit a fake Coq
+    error location pointing to the end of the .v file before that line.
+    """
+    lines = output.split("\n")
+    result_lines = []
+    for line in lines:
+        if line.startswith("Fatal Error:"):
+            # Insert fake Coq error location before the Fatal Error line
+            result_lines.append(
+                f'File "{v_file_name}", line {line_count}, characters 0-0:'
+            )
+            result_lines.append("Error:")
+        result_lines.append(line)
+    return "\n".join(result_lines)
+
+
 @memoize
 def get_coq_accepts_fine_grained_debug(coqc, debug_kind):
     temp_file = tempfile.NamedTemporaryFile(suffix=".v", dir=".", delete=True)
@@ -548,8 +572,11 @@ def reset_coq_output_cache(
     pass_on_stdin=False,
     verbose_base=1,
     ocamlpath=None,
+    coqchk_prog=None,
+    coqchk_prog_args=(),
     **kwargs,
 ):
+    key_extra = (coqchk_prog, tuple(coqchk_prog_args)) if coqchk_prog else ()
     key, file_name, cmds, input_val, cleaner, env = prepare_cmds_for_coq_output(
         coqc_prog,
         coqc_prog_args,
@@ -562,6 +589,7 @@ def reset_coq_output_cache(
         ocamlpath=ocamlpath,
         **kwargs,
     )
+    key = key + key_extra
     cleaner()
 
     if key in COQ_OUTPUT.keys():
@@ -581,10 +609,18 @@ def get_coq_output(
         lambda output: "is not a compiled interface for this version of OCaml" in output
     ),
     ocamlpath=None,
+    coqchk_prog=None,
+    coqchk_prog_args=(),
     **kwargs,
 ):
     """Returns the coqc output of running through the given
-    contents.  Pass timeout_val = None for no timeout."""
+    contents.  Pass timeout_val = None for no timeout.
+
+    If coqchk_prog is provided, after coqc succeeds, coqchk will be run on the
+    resulting .vo file. The output is combined, but if coqc fails, we end early.
+    When coqchk outputs "Fatal Error:", a fake Coq error location pointing to
+    the end of the .v file is inserted before that line.
+    """
     if (
         timeout_val is not None
         and timeout_val < 0
@@ -601,9 +637,12 @@ def get_coq_output(
             verbose_base=verbose_base,
             retry_with_debug_when=retry_with_debug_when,
             ocamlpath=ocamlpath,
+            coqchk_prog=coqchk_prog,
+            coqchk_prog_args=coqchk_prog_args,
             **kwargs,
         )
 
+    key_extra = (coqchk_prog, tuple(coqchk_prog_args)) if coqchk_prog else ()
     key, file_name, cmds, input_val, cleaner, env = prepare_cmds_for_coq_output(
         coqc_prog,
         coqc_prog_args,
@@ -617,6 +656,9 @@ def get_coq_output(
         **kwargs,
     )
 
+    # Extend key to include coqchk info
+    key = key + key_extra
+
     if key in COQ_OUTPUT.keys():
         cleaner()
         return COQ_OUTPUT[key][1]
@@ -659,10 +701,78 @@ def get_coq_output(
     )
     if get_timeout(coqc_prog) is None and timeout_val is not None:
         set_timeout(coqc_prog, 3 * max((1, int(math.ceil(finish - start)))), **kwargs)
+
+    combined_stdout = util.s(stdout)
+    combined_returncode = returncode
+    combined_runtime = runtime
+    combined_peak_rss_kb = peak_rss_kb
+
+    # If coqchk is enabled and coqc succeeded, run coqchk
+    if coqchk_prog is not None and returncode == 0:
+        # Build coqchk command: coqchk -o -silent <args> <vo_file>
+        vo_file = os.path.splitext(file_name)[0] + ".vo"
+        assert isinstance(coqchk_prog, tuple), coqchk_prog
+        coqchk_cmds = [*coqchk_prog, *coqchk_prog_args, vo_file]
+        chk_start = time.time()
+        ((chk_stdout, chk_stderr), chk_returncode, chk_peak_rss_bytes) = (
+            memory_robust_timeout_Popen_communicate(
+                kwargs["log"],
+                coqchk_cmds,
+                stderr=subprocess.STDOUT,
+                stdout=subprocess.PIPE,
+                stdin=subprocess.PIPE,
+                timeout=(
+                    timeout_val if timeout_val is not None and timeout_val > 0 else None
+                ),
+                cwd=cwd,
+                env=env,
+                **extra_kwargs,
+            )
+        )
+        chk_finish = time.time()
+        chk_runtime = chk_finish - chk_start
+        chk_peak_rss_kb = chk_peak_rss_bytes / 1024
+
+        kwargs["log"](
+            "\ncoqchk retcode: %d\nstdout:\n%s\n\nstderr:\n%s\nruntime:\n%f\npeak_rss:\n%f kb\n\n"
+            % (
+                chk_returncode,
+                util.s(chk_stdout),
+                util.s(chk_stderr),
+                chk_runtime,
+                chk_peak_rss_kb,
+            ),
+            level=verbose_base + 1,
+        )
+
+        # Count lines in the .v file for error location
+        line_count = contents.count("\n") + 1
+
+        # Process coqchk output to insert error preamble before "Fatal Error:" lines
+        processed_chk_output = process_coqchk_output(
+            util.s(chk_stdout), file_name, line_count
+        )
+
+        # Combine outputs
+        combined_stdout = combined_stdout + "\n" + processed_chk_output
+        combined_returncode = (
+            chk_returncode if chk_returncode != 0 else combined_returncode
+        )
+        combined_runtime = runtime + chk_runtime
+        combined_peak_rss_kb = max(peak_rss_kb, chk_peak_rss_kb)
+
+    # Now clean up after coqchk has run (or if coqchk wasn't needed)
     cleaner()
+
     COQ_OUTPUT[key] = (
         file_name,
-        (clean_output(util.s(stdout)), tuple(cmds), returncode, runtime, peak_rss_kb),
+        (
+            clean_output(combined_stdout),
+            tuple(cmds),
+            combined_returncode,
+            combined_runtime,
+            combined_peak_rss_kb,
+        ),
     )
     kwargs["log"](
         "Storing result: COQ_OUTPUT[%s]:\n%s" % (repr(key), repr(COQ_OUTPUT[key])),
@@ -684,6 +794,8 @@ def get_coq_output(
             verbose_base=verbose_base,
             retry_with_debug_when=(lambda output: False),
             ocamlpath=ocamlpath,
+            coqchk_prog=coqchk_prog,
+            coqchk_prog_args=coqchk_prog_args,
             **kwargs,
         )
     return COQ_OUTPUT[key][1]

coq_tools/find_bug.py

@@ -572,6 +572,30 @@
     action="append",
     help="The path to the coqchk program for the passing coqc (only used with --chk).",
 )
+parser.add_argument(
+    "--coqchk-args",
+    metavar="ARG",
+    dest="coqchk_args",
+    type=str,
+    action="append",
+    help='Arguments to pass to coqchk (both passing and nonpassing); e.g., " -silent" (leading and trailing spaces are stripped, only used with --chk)',
+)
+parser.add_argument(
+    "--nonpassing-coqchk-args",
+    metavar="ARG",
+    dest="nonpassing_coqchk_args",
+    type=str,
+    action="append",
+    help='Arguments to pass to nonpassing coqchk; e.g., " -silent" (leading and trailing spaces are stripped, only used with --chk)',
+)
+parser.add_argument(
+    "--passing-coqchk-args",
+    metavar="ARG",
+    dest="passing_coqchk_args",
+    type=str,
+    action="append",
+    help='Arguments to pass to passing coqchk; e.g., " -silent" (leading and trailing spaces are stripped, only used with --chk)',
+)
 parser.add_argument(
     "--passing-coqc",
     metavar="COQC",
@@ -1072,6 +1096,8 @@ def get_error_reg_string(output_file_name, **kwargs):
             verbose_base=1,
             cwd=kwargs["base_dir"],
             ocamlpath=kwargs["nonpassing_ocamlpath"],
+            coqchk_prog=kwargs["coqchk"],
+            coqchk_prog_args=kwargs["coqchk_args"],
             **kwargs,
         )
         result = ""
@@ -1313,6 +1339,8 @@ def get_padded_contents():
         is_coqtop=kwargs["coqc_is_coqtop"],
         verbose_base=2,
         ocamlpath=kwargs["nonpassing_ocamlpath"],
+        coqchk_prog=kwargs["coqchk"],
+        coqchk_prog_args=kwargs["coqchk_args"],
         **kwargs,
     )
     if not should_succeed and diagnose_error.has_error(
@@ -1346,6 +1374,8 @@ def get_padded_contents():
                 is_coqtop=kwargs["passing_coqc_is_coqtop"],
                 verbose_base=2,
                 ocamlpath=kwargs["passing_ocamlpath"],
+                coqchk_prog=kwargs["passing_coqchk"],
+                coqchk_prog_args=kwargs["passing_coqchk_args"],
                 **kwargs,
             )
             if not (
@@ -3413,6 +3443,8 @@ def minimize_file(
             verbose_base=2,
             cwd=env["base_dir"],
             ocamlpath=env["nonpassing_ocamlpath"],
+            coqchk_prog=env["coqchk"],
+            coqchk_prog_args=env["coqchk_args"],
             **env,
         )
         line_num = diagnose_error.get_error_line_number(output, env["error_reg_string"])
@@ -3809,6 +3841,8 @@ def get_test_output(
                     is_coqtop=kwargs["coqc_is_coqtop"],
                     verbose_base=2,
                     ocamlpath=kwargs["nonpassing_ocamlpath"],
+                    coqchk_prog=kwargs["coqchk"],
+                    coqchk_prog_args=kwargs["coqchk_args"],
                     **kwargs,
                 )
             )
@@ -4215,11 +4249,31 @@ def prepend_coqbin(prog):
         "coq_makefile": prepend_coqbin(args.coq_makefile or "coq_makefile"),
         "coqdep": prepend_coqbin(args.coqdep),
         "chk": args.chk,
-        "coqchk": prepend_coqbin(args.coqchk or "coqchk"),
+        "coqchk": (prepend_coqbin(args.coqchk or "coqchk") if args.chk else None),
         "passing_coqchk": (
-            prepend_coqbin(args.passing_coqchk)
-            if args.passing_coqchk
-            else prepend_coqbin(args.coqchk or "coqchk")
+            (
+                prepend_coqbin(args.passing_coqchk)
+                if args.passing_coqchk
+                else prepend_coqbin(args.coqchk or "coqchk")
+            )
+            if args.chk
+            else None
+        ),
+        "coqchk_args": tuple(
+            i.strip()
+            for i in (
+                list(process_maybe_list(args.nonpassing_coqchk_args, log=args.log))
+                + list(process_maybe_list(args.coqchk_args, log=args.log))
+                + list(process_maybe_list(args.coq_args, log=args.log))
+            )
+        ),
+        "passing_coqchk_args": tuple(
+            i.strip()
+            for i in (
+                list(process_maybe_list(args.passing_coqchk_args, log=args.log))
+                + list(process_maybe_list(args.coqchk_args, log=args.log))
+                + list(process_maybe_list(args.coq_args, log=args.log))
+            )
         ),
         "passing_coqc_args": tuple(
             i.strip()
@@ -4414,17 +4468,6 @@ def make_make_coqc(coqc_prog, **kwargs):
                     env["passing_coqc"] = env["coqtop"]
             env["passing_make_coqc"] = make_make_coqc(env["passing_coqc"], **env)
 
-        if env["chk"]:
-            # Wrap coqc with coqchk-as-coqc.sh to also run coqchk after coqc
-            coqchk_wrapper = str(util.resource_path("coqchk-as-coqc.sh"))
-            env["coqc"] = (coqchk_wrapper, *env["coqc"], *env["coqchk"])
-            if env["passing_coqc"] is not None:
-                env["passing_coqc"] = (
-                    coqchk_wrapper,
-                    *env["passing_coqc"],
-                    *env["passing_coqchk"],
-                )
-
         coqc_help = get_coqc_help(get_preferred_passing("coqc", **env), **env)
         coqc_version = get_coqc_version(env["coqc"], **env)
 
@@ -4559,6 +4602,17 @@ def make_make_coqc(coqc_prog, **kwargs):
                 env["passing_coqtop"] if env["passing_coqtop"] else env["coqtop"],
                 "passing_",
             ),
+        ) + (
+            (
+                ("coqchk_args", env["coqchk"], ""),
+                (
+                    "passing_coqchk_args",
+                    env["passing_coqchk"] if env["passing_coqchk"] else env["coqchk"],
+                    "passing_",
+                ),
+            )
+            if env["chk"]
+            else ()
         ):
             env[args_name] = tuple(list(env[args_name]) + list(extra_args))
             for dirname, libname in env.get(passing_prefix + "libnames", []):
@@ -4587,14 +4641,28 @@ def make_make_coqc(coqc_prog, **kwargs):
                 if arg[0] == "-I":
                     env.get(passing_prefix + "ocaml_dirnames", []).append(arg[1])
 
-        for args_name, coqtop_prog, coqc_prog, passing_prefix in (
-            ("coqtop_args", env["coqtop"], env["coqc"], ""),
+        for coqprog, args_name, coqtop_prog, coqc_prog, passing_prefix in (
+            ("coqtop", "coqtop_args", env["coqtop"], env["coqc"], ""),
             (
+                "coqtop",
                 "passing_coqtop_args",
                 env["passing_coqtop"] if env["passing_coqtop"] else env["coqtop"],
                 env["passing_coqc"] if env["passing_coqc"] else env["coqc"],
                 "passing_",
             ),
+        ) + (
+            (
+                ("coqchk", "coqchk_args", env["coqchk"], env["coqc"], ""),
+                (
+                    "passing_coqchk",
+                    "passing_coqchk_args",
+                    env["passing_coqchk"] if env["passing_coqchk"] else env["coqchk"],
+                    env["passing_coqc"] if env["passing_coqc"] else env["coqc"],
+                    "passing_",
+                ),
+            )
+            if env["chk"]
+            else ()
         ):
             coqc_prog_help = get_coqc_help(coqc_prog, **env)
             coqtop_prog_help = get_coqc_help(coqtop_prog, **env)
@@ -4607,8 +4675,7 @@ def make_make_coqc(coqc_prog, **kwargs):
             )
             if len(coqc_but_not_coqtop_args) > 0:
                 env["log"](
-                    "Warning: skipping arguments to coqtop that are only valid for coqc: %s"
-                    % repr(coqc_but_not_coqtop_args),
+                    f"Warning: skipping arguments to {coqprog} that are only valid for coqc: {coqc_but_not_coqtop_args!r}",
                     level=2,
                 )
             env[args_name] = tuple(