CoqGym

Code for the paper:

Learning to Prove Theorems via Interacting with Proof Assistants
Kaiyu Yang and Jia Deng
International Conference on Machine Learning (ICML) 2019

@inproceedings{yang2019coqgym,
  title={Learning to Prove Theorems via Interacting with Proof Assistants},
  author={Yang, Kaiyu and Deng, Jia},
  booktitle={International Conference on Machine Learning (ICML)},
  year={2019}
}

For potential bugs, please open an issue. For any other questions, please ask in Discussions.

Table of Contents

1. Installing CoqGym
       1.1 Dependencies
       1.2 Building Coq, SerAPI, CoqHammer, and the Coq Projects
       1.3 Extracting the Proofs from Coq Code
       1.4 Downloading the Pre-extracted Proofs
2. Using CoqGym in Docker
3. Data Format
       3.1 JSON Files
       3.2 LMDB File
       3.3 Gloassary
4. Data Utilities
       4.1 Interacting with CoqGym
       4.2 Parsing Coq Terms
       4.3 Computing Dataset Statistics
5. The ASTactic Model
       5.1 Prerequisites
       5.2 Extracting Proof Steps
       5.3 Training
       5.4 Testing
6. Credits
7. Contributing

---

1. Installing CoqGym

We recommend using CoqGym in Docker, as CoqGym has many dependencies and is nontrivial to set up correctly. If Docker is not an option, below are steps to obtain the CoqGym dataset and build the interaction environment natively:

1.1 Dependencies

• OPAM
• Anaconda Python 3
• LMDB
• Ruby

1.2 Building Coq, SerAPI, CoqHammer, and the Coq Projects

1. Create an OPAM switch for OCaml 4.07.1+flambda: opam switch create 4.07.1+flambda && eval $(opam env)
2. Upgrade the installed OPAM packages (optional): opam upgrade && eval $(opam env)
3. Clone the repository: git clone https://github.com/princeton-vl/CoqGym
4. Install Coq, SerAPI and CoqHammer: cd CoqGym && source install.sh
5. Build the Coq projects (can take a while): cd coq_projects && make && cd ..
6. Create and activate the conda environment: conda env create -f coq_gym.yml && conda activate coq_gym

Note: Coq, SerAPI, CoqHammer, and the Coq projects in coq_projects directory are independent software projects with their own code repositories, but please follow the instructions above to build the specific versions we need.

1.3 Extracting the Proofs from Coq Code (Optional)

We include the code for extracting CoqGym from Coq source code. However, it is not guaranteed to reproduce exactly the same data. The timeout and other miscellaneous errors during the data extraction may be machine-dependent. For example, a faster machine is likely to have fewer timeout errors and thus can extract more proofs. For benchmark purposes, please download and use our pre-extracted version of CoqGym.

1. Check all Coq files and locate the proofs:
   For each *.meta file in ./coq_projects/, run python check_proofs.py --file /path/to/*.meta
   Now you have generated a *.json file in ./data/ corresponding to each *.meta file. The proofs field of the JSON object is a list containing the proof names.

2. Extract the proofs:
   For each *.meta file and each proof, run:
   python extract_proof.py --file /path/to/*.meta --proof $PROOF_NAME
python extract_synthetic_proofs.py --file /path/to/*.meta --proof $PROOF_NAME

3. Post-processing: python postprocess.py

Caveat: The steps above are computationally expensive. When we say "For each XXX, run YYY", the tasks are embarrassingly parallel, which means you can run them in parallel in any order. We do not provide the code for that because it depends on a particular HPC infrastructure.

1.4 Downloading the Pre-extracted Proofs (Recommended)

1. Download the CoqGym dataset from .

2. Unzip the data and set the paths: python unzip_data.py

Caveat: The second step sets the absolute paths in the data. You have to re-do it whenever the absolute path of the data/ directory changes (e.g. after moving the entire repo to another directory).

Now you are ready to interact with CoqGym! Run python eval_env.py to check if it terminates normally without raising an error.

---

2. Using CoqGym in Docker

As a less painful alternative to installing CoqGym from scratch, we provide a Docker image with everything pre-installed. The image was built from this Dockerfile. It includes the CoqGym dataset, proof steps extracted from the dataset, our pre-trained ASTactic model, and all necessary dependencies such as OPAM, Z3, CVC4, Vampire, and E Prover. You shouldn't need to download anything else if you choose to use the Docker image.

---

3. Data Format

The dataset contains three parts:

• The data directory: *.json files corresponding to the *.v files in Coq source code, whose format is explained below. The *.json files contain all important information about the proofs: environment, local context, goals, tactics, proof trees, etc.

• The sexp_cache directory: A LMDB file that serves as an index for the S-expressions in *.json files. The *.json files contain keys for querying sexp_cache

• projs_split.json: A JSON object containing the training/validation/testing split

3.1 JSON Files

Each *.json file in data/ corresponds to a Coq source file *.v in coq_projects/. For example, data/StructTact/Assoc.json corresponds to coq_projects/StructTact/Assoc.v.

The format of the JSON files is described below. The hash codes are used as keys to query the LMDB sexp_cache. Consult the glossary for the terminology.

{
    'filename': 'Assoc.v',            # the path of the Coq source file relative to the root directory of the Coq project
    'coq_project': 'StructTact',      # the name of the Coq project
    'vernac_cmds': [                  # a list of Coq commands [6] in the source file
        ['Cd "$COQGYM_ROOT/coq_projects/StructTact".', 'VernacChdir',  '3701e61f37b72b3e61788fce6317466b7bb92b55'],     # [raw command, command type, command AST (in hash code)]
        ['Arguments a_equiv {_} {_} _ _ _.', 'VernacArguments', '6777d3c472595dae20427d0892ad03d38f70fde9'],
        ...
        ['Arguments a_equiv {_} {_} _ _ _.', 'VernacArguments', '6777d3c472595dae20427d0892ad03d38f70fde9'],
    ],
   'num_extra_cmds': 107,             # the code in the original Coq file starts at vernac_cmds[num_extra_cmds]
   'proofs': [                        # a list of human-written proofs
       ...
    ],
    'synthetic_proofs': [             # a list of synthetic proofs
       ...
    ],
}

The format for a proof is as follows, taking the get_set_same in coq_projects/StructTact/Assoc.v as an example.

{
    'name': get_set_same,             # the name of the theorem
    'line_nb': 118,                   # the theorem is defined in $file_data['vernac_cmds'][$line_nb]
    
    'env_delta': {                          # the global environment relative to the previous proof in the same file
        'add' : {                           # entries that should be added to the environment
            'constants' : [
                {
                    'physical_path': 'coq/theories/Arith/PeanoNat.vo:Nat.mul_wd',       # the unique identifier
                    'short_ident': 'PeanoNat.Nat.mul_wd',                               # the short identifier
                    'qualid': 'Coq.Arith.PeanoNat.Nat.mul_wd',             # the qualified identifier [1]
                    'type': '@Morphisms.Proper (forall (_ : nat) (_ : nat), nat) (@Morphisms.respectful nat (forall _ : nat, nat) (@eq nat) (@Morphisms.respectful nat nat (@eq nat) (@eq nat))) Nat.mul',    # the type [7] of the constant
                    'sort': 'Prop',                                        # the sort [2] of the constant (the type of its type) [2]
                    'opaque': False,                                       # whether the constant is opaque or transparent [3]
                    'sexp': '333b2895c8e62d21856476bf89fa9681c9058bb9'     # the S-expression [4] of the constant produced by SerAPI
            },   
            ...
            ],
            'inductives' : [
                {
                    'physical_path' : 'coq/theories/Init/Wf.vo:Acc',
                    'blocks': [           # a list of blocks in a mutual inductive definition [5]. For regular inductive definitions (mos