run

#! /usr/bin/env python

import argparse
import os
import coloredlogs
import logging
import subprocess
import time

coloredlogs.install()

def collect_admitted_defs(data: list[str]) -> list[str]:
    admitted = []
    keywords = ["Definition", "Theorem", "Lemma", "Corollary", "Proposition", "Fact", "Fixpoint", "Instance"]

    for i in range(len(data)):
        if data[i].strip().startswith("Admitted."):
            # Find the definition name.
            for j in range(i, -1, -1):
                # Find the index of the keyword.
                if any(keyword in data[j] for keyword in keywords):
                    admitted.append("Line " + str(j) + ": " + data[j].strip())
                    break
    return admitted


def check(allow_admitted: bool, verbose: bool) -> None:
    dir = os.path.join(os.curdir, "theories")

    # Change the current working directory to the given path.
    os.chdir(dir)

    errs = {}
    for file in os.listdir():
        if file.endswith(".v"):
            logging.info("Checking file: " + file)
            with open(os.path.join(os.getcwd(), file)) as f:
                data = [data.strip() for data in f.readlines()]

                items = collect_admitted_defs(data)
                if items:
                    errs[file] = items
    if errs:
        if allow_admitted:
            logging.warning(
                "Admitted proofs found in files: "
                + ", ".join(errs)
                + ", since you allow admitted proofs, this may result in incorrect proofs.",
            )
            if verbose:
                for file, items in errs.items():
                    logging.warning(file + ": Admitted definitions:\n\t" + "\n\t".join(items))
        else:
            logging.error("Admitted proofs are not allowed: " + ", ".join(errs))
            if verbose:
                for file, items in errs.items():
                    logging.error(file + ": Admitted definitions:\n\t" + "\n\t".join(items))
            exit(1)

    if not os.path.exists("Makefile"):
        subprocess.run(["coq_makefile", "-f", "_CoqProject", "-o", "Makefile"])

    res = subprocess.run("make", stderr=subprocess.PIPE, stdout=subprocess.PIPE)

    if res.returncode != 0:
        logging.error("Proof check failed.")
        logging.error("\n" + res.stderr.decode("utf-8"))
    else:
        logging.info("Proof check succeeded.")


if __name__ == "__main__":
    # Check if Coq is installed.
    res = subprocess.call(["which", "coqc"])
    if res != 0:
        logging.error("Coq is not installed.")
        exit(1)
    logging.info("COQC found.")

    parser = argparse.ArgumentParser()
    parser.add_argument(
        "--allow_admitted", help="Allow admitted proofs.", action="store_true"
    )
    parser.add_argument(
        "-v", "--verbose", help="Print verbose output.", action="store_true"
    )

    args = parser.parse_args()

    t = time.time()
    check(args.allow_admitted, args.verbose)
    logging.info("Time taken: " + str(time.time() - t) + "s.")