itp-interface 1.1.0

Generic interface for hooking up to any Interactive Theorem Prover (ITP) and collecting data for training ML models for AI in formal theorem proving.

itp-interface

Generic interface for hooking up to any Interactive Theorem Prover (ITP) and collecting data for training ML models for AI in formal theorem proving.

Quick Setup for Lean 4:

1. Install itp-interface using the following command:

pip install itp-interface

2. Run the following command to prepare the REPL for Lean 4. (The default version is 4.7.0-rc2. You can change the version by setting the LEAN_VERSION environment variable. If no version is set, then 4.7.0-rc2 is used.)

NOTE: The Lean 4 version must match the version of the Lean 4 project you are working with.

export LEAN_VERSION="4.15.0"
install-lean-repl

3. Run the following command to build the REPL for Lean 4. Make sure that lean --version returns the correct version before running the command below. If not then check if $HOME/.elan/bin is in your path. Recommended to run source $HOME/.elan/env before running the command below.

install-itp-interface

NOTE: These steps are only tested on Linux. For Windows, you can use WSL. These steps will not setup the Coq interface.

Full Setup for Coq and Lean:

1. Install OCaml first. Use the instructions here: https://opam.ocaml.org/doc/Install.html . The opam version used in this project is 2.1.3 (OCaml 4.14.0). Note that OCaml officially only supports Linux installations. One can use WSL on Windows machines.

2. Run the following to install Coq on Linux. The Coq version used in this project is <= 8.15.

sudo apt install build-essential unzip bubblewrap
sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)

3. Add the following to your .bashrc file: (sometimes the path ~/.opam/default might not exist, so use the directory with version number present in the ~/.opam directory)

export PATH="/home/$USER/.opam/default/bin:$PATH"

4. Create a Miniconda environment and activate it.

5. Run the commands for installing the Lean 4 interface as mentioned in Quick Setup for Lean 4.

6. Add the following to your .bashrc file for Lean:

export PATH="/home/$USER/.elan/bin:$PATH"

Running Simple Interactions:

1. Simple example for Lean 4 interaction:

import os
from itp_interface.rl.proof_state import ProofState
from itp_interface.rl.proof_action import ProofAction
from itp_interface.rl.simple_proof_env import ProofEnv
from itp_interface.tools.proof_exec_callback import ProofExecutorCallback
from itp_interface.rl.simple_proof_env import ProofEnvReRankStrategy

project_folder = "src/data/test/lean4_proj"
file_path = "src/data/test/lean4_proj/Lean4Proj/Basic.lean"
# Code for building the Lean project
# cd src/data/test/lean4_proj && lake build
with os.popen(f"cd {project_folder} && lake build") as proc:
    print("Building Lean4 project...")
    print('-'*15 + 'Build Logs' + '-'*15)
    print(proc.read())
    print('-'*15 + 'End Build Logs' + '-'*15)
# Skip the above code if the project is already built
language = ProofAction.Language.LEAN4
theorem_name = "test3"
# theorem test3 (p q : Prop) (hp : p) (hq : q)
# : p ∧ q ∧ p :=
proof_exec_callback = ProofExecutorCallback(
    project_folder=project_folder,
    file_path=file_path,
    language=language,
    always_use_retrieval=False,
    keep_local_context=True
)
always_retrieve_thms = False
retrieval_strategy = ProofEnvReRankStrategy.NO_RE_RANK
env = ProofEnv("test_lean4", proof_exec_callback, theorem_name, retrieval_strategy=retrieval_strategy, max_proof_depth=10, always_retrieve_thms=always_retrieve_thms)
proof_steps = [
    'apply And.intro',
    'exact hp',
    'apply And.intro',
    'exact hq',
    'exact hp'
]
with env:
    for proof_step in proof_steps:
        action = ProofAction(
            ProofAction.ActionType.RUN_TACTIC, 
            language, 
            tactics=[proof_step])
        state, _, next_state, _, done, info = env.step(action)
        if info.error_message is not None:
            print(f"Error: {info.error_message}")
        # This prints StateChanged, StateUnchanged, Failed, or Done
        print(info.progress)
        print('-'*30)
        if done:
            print("Proof Finished!!")
        else:
            s1 : ProofState = state
            s2 : ProofState = next_state
            print(f"Current Goal:")
            print('-'*30)
            for goal in s1.training_data_format.start_goals:
                hyps = '\n'.join([hyp for hyp in goal.hypotheses])
                print(hyps)
                print('|- ', end='')
                print(goal.goal)
            print(f"="*30)
            print(f"Action: {proof_step}")
            print(f"="*30)
            print(f"Next Goal:")
            print('-'*30)
            for goal in s2.training_data_format.start_goals:
                hyps = '\n'.join([hyp for hyp in goal.hypotheses])
                print(hyps)
                print('|- ', end='')
                print(goal.goal)
            print(f"="*30)

2. One can also backtrack the last proof action using the following code:

action = ProofAction(ProofAction.ActionType.BACKTRACK, language)
state, _, next_state, _, done, info = env.step(action)

3. The code for Coq interaction is similar to the Lean 4 interaction. The only difference is the language used in the ProofAction object. The language for Coq is ProofAction.Language.COQ. We also need to make sure that the Coq project is built before running the code. Please note that it is important to install the correct version of Coq and Coq LSP for the Coq project. The following code snippet shows how to interact with Coq:

project_folder = "src/data/test/coq/custom_group_theory/theories"
file_path = "src/data/test/coq/custom_group_theory/theories/grpthm.v"

# IMPORTANT NOTE: The Coq project must be built before running the code.
# Create a switch for building the Coq project
if os.system("opam switch simple_grp_theory") != 0:
    cmds = [
        'opam switch create simple_grp_theory 4.14.2',
        'opam switch simple_grp_theory', 
        'eval $(opam env)',
        'opam repo add coq-released https://coq.inria.fr/opam/released',
        'opam pin add -y coq-lsp 0.1.8+8.18'
    ]
    final_cmd = ' && '.join(cmds)
    os.system(final_cmd)
# IMPORTANT NOTE: Make sure to switch to the correct switch before running the code.
os.system("opam switch simple_grp_theory && eval $(opam env)")
# Clean the project
os.system(f"cd {project_folder} && make clean")
# Build the project
with os.popen(f"cd {project_folder} && make") as proc:
    print("Building Coq project...")
    print('-'*15 + 'Build Logs' + '-'*15)
    print(proc.read())
    print('-'*15 + 'End Build Logs' + '-'*15)
# Skip the above code if the project is already built
language = ProofAction.Language.COQ # IMPORTANT NOTE: The language will change here to COQ
theorem_name = "algb_identity_sum"
# ....

# IMPORTANT NOTE: As a result of language change, the `ProofExecutorCallback` object will also change.
proof_exec_callback = ProofExecutorCallback(
    project_folder=project_folder,
    file_path=file_path,
    language=language, # The language will change here to COQ
    always_use_retrieval=False,
    keep_local_context=True
)

# IMPORTANT NOTE: The proof steps will also change for Coq.
proof_steps = [
    'intros.',
    'destruct a.',
    '- reflexivity.',
    '- reflexivity.'
]

# IMPORTANT NOTE: As a result of language change, the `action` object will also change.
action = ProofAction(
    ProofAction.ActionType.RUN_TACTIC, 
    language, # The language will change here to COQ
    tactics=[proof_step]
)

4. See the file src/test/simple_env_test.py for more examples for Lean 4 interaction and Coq interaction.

Generating Proof Step Data:

1.a. You need to run the following command to generate sample proof step data for Lean 4:

python src/itp_interface/main/run_tool.py --config-name simple_lean_data_gen

Check the simple_lean_data_gen.yaml configuration in the src/itp_interface/configs directory for more details. These config files are based on the hydra library (see here).

1.b. You need to run the following command to generate sample proof step data for Coq:

python src/itp_interface/main/run_tool.py --config-name simple_coq_data_gen

Check the simple_coq_data_gen.yaml configuration in the src/itp_interface/configs directory for more details about where the generated data is stored and where the different ITP (Coq and Lean) projects are located in the file system.

Important Note:

The ITP projects must be built before running proof step data generation. Make sure that the switch is set correctly while generating data for Coq projects because the Coq projects can be using different versions of Coq. Instructions for Coq project setup are listed in src/itp_interface/main/config/repo/coq_repos.yaml file.