check_proofs.py

import os
import json
from glob import glob
from utils import get_code, SexpCache, set_paths, extract_code, dst_filename
from serapi import SerAPI
import pdb


def check_file(filename, sexp_cache, args):
    print("\n" + filename)
    coq_filename = os.path.splitext(filename)[0] + ".v"
    fields = coq_filename.split(os.path.sep)
    loc2code = get_code(open(coq_filename, "rb").read())
    file_data = {
        "filename": os.path.sep.join(fields[2:]),
        "coq_project": fields[1],
        "vernac_cmds": [],
        "num_extra_cmds": None,
        "proofs": [],
    }
    meta = open(filename).read()

    with SerAPI(args.timeout, args.debug) as serapi:
        # set the path
        file_data["vernac_cmds"].extend(set_paths(meta, serapi, sexp_cache))
        file_data["num_extra_cmds"] = len(file_data["vernac_cmds"])

        # extract the coq code
        coq_code = extract_code(meta, loc2code)

        # process the coq code
        for num_executed, (code_line, tags) in enumerate(coq_code):
            if "PROOF_NAME" in tags:
                if tags["PROOF_NAME"] not in file_data["proofs"]:
                    file_data["proofs"].append(tags["PROOF_NAME"])
            # execute until the proof editing mode starts
            if args.debug:
                print("%d: %s" % (num_executed, code_line))
            _, ast = serapi.execute(code_line, return_ast=True)
            file_data["vernac_cmds"].append(
                (code_line, tags["VERNAC_TYPE"], sexp_cache.dump(ast))
            )

    return file_data


def dump(file_data, args):
    path = os.path.join(
        args.data_path, file_data["coq_project"], file_data["filename"]
    )[:-2]
    try:
        os.makedirs(os.path.split(path)[0])
    except os.error:
        pass
    json.dump(file_data, open(path + ".json", "wt"))


def process_file(filename):
    # extract a Coq file
    db_path = dst_filename(filename, args.data_path) + "-sexp_cache"
    try:
        os.makedirs(os.path.split(db_path)[0])
    except os.error:
        pass
    sexp_cache = SexpCache(db_path)
    file_data = check_file(filename, sexp_cache, args)
    dump(file_data, args)


if __name__ == "__main__":
    import sys

    sys.setrecursionlimit(100000)
    import argparse

    arg_parser = argparse.ArgumentParser(
        description="Execute the Coq source code and locate the proofs"
    )
    arg_parser.add_argument(
        "--debug", action="store_true", help="print the executed Coq code"
    )
    arg_parser.add_argument(
        "--proj", type=str, help="The Coq project to process (default to all projects)"
    )
    arg_parser.add_argument(
        "--meta_files",
        type=str,
        help="The file containing the paths of *.meta files (default to all *.meta files)",
    )
    arg_parser.add_argument(
        "--file",
        type=str,
        help="The meta file to process (default to all *.meta files)",
    )
    arg_parser.add_argument(
        "--timeout", type=int, default=600, help="Timeout for SerAPI"
    )
    arg_parser.add_argument("--data_path", type=str, default="./data")
    args = arg_parser.parse_args()
    assert args.proj is None or args.meta_files is None

    # grab the *.meta files to process
    if args.proj:
        meta_files = list(glob("coq_projects/%s/**/*.meta" % args.proj, recursive=True))
    elif args.meta_files:
        meta_files = [line.strip() for line in open(args.meta_files)]
    elif args.file:
        meta_files = [args.file]
    else:
        meta_files = list(glob("coq_projects/**/*.meta", recursive=True))
    meta_files.sort()
    print("%d Coq files to process" % len(meta_files))

    # process each of them
    for filename in meta_files:
        process_file(filename)