diff --git a/generator/datamodule.py b/generator/datamodule.py index e28202e..d0654f7 100644 --- a/generator/datamodule.py +++ b/generator/datamodule.py @@ -1,4 +1,5 @@ """Data module for the tactic generator.""" + import os import json import pickle diff --git a/generator/main.py b/generator/main.py index 518c0b6..9ae06c8 100644 --- a/generator/main.py +++ b/generator/main.py @@ -1,4 +1,5 @@ """Script for training the tactic generator.""" + import os from loguru import logger from pytorch_lightning.cli import LightningCLI diff --git a/generator/model.py b/generator/model.py index 9cd542d..97aabc8 100644 --- a/generator/model.py +++ b/generator/model.py @@ -1,4 +1,5 @@ """Lightning module for the tactic generator.""" + import torch import openai import pickle diff --git a/prover/evaluate.py b/prover/evaluate.py index 21c709a..044a367 100644 --- a/prover/evaluate.py +++ b/prover/evaluate.py @@ -1,5 +1,6 @@ """Script for evaluating the prover on theorems extracted by LeanDojo. """ + import os import uuid import json diff --git a/prover/proof_search.py b/prover/proof_search.py index 5fe7262..dcf6c97 100644 --- a/prover/proof_search.py +++ b/prover/proof_search.py @@ -1,5 +1,6 @@ """Proof search using best-first search. """ + import os import sys import ray diff --git a/prover/search_tree.py b/prover/search_tree.py index 8b5b79e..3174e67 100644 --- a/prover/search_tree.py +++ b/prover/search_tree.py @@ -1,5 +1,6 @@ """Definitions of the search tree used by the prover. """ + import math from enum import Enum from lean_dojo import ( diff --git a/retrieval/bm25/main.py b/retrieval/bm25/main.py index 3ad4086..49e6b12 100644 --- a/retrieval/bm25/main.py +++ b/retrieval/bm25/main.py @@ -1,4 +1,5 @@ """Script for training the BM25 premise retriever.""" + import os import ray import json diff --git a/retrieval/datamodule.py b/retrieval/datamodule.py index 5c916c1..442e057 100644 --- a/retrieval/datamodule.py +++ b/retrieval/datamodule.py @@ -1,4 +1,5 @@ """Datamodule for the premise retrieval.""" + import os import json import torch diff --git a/retrieval/evaluate.py b/retrieval/evaluate.py index 1bec77c..2766ef6 100644 --- a/retrieval/evaluate.py +++ b/retrieval/evaluate.py @@ -1,4 +1,5 @@ """Script for evaluating the premise retriever.""" + import os import json import pickle diff --git a/retrieval/index.py b/retrieval/index.py index 9b29f2c..59e333b 100644 --- a/retrieval/index.py +++ b/retrieval/index.py @@ -1,5 +1,6 @@ """Script for indexing the corpus using the retriever. """ + import torch import pickle import argparse diff --git a/retrieval/main.py b/retrieval/main.py index 55390c1..efa9e30 100644 --- a/retrieval/main.py +++ b/retrieval/main.py @@ -1,5 +1,6 @@ """Script for training the premise retriever. """ + import os from loguru import logger from pytorch_lightning.cli import LightningCLI diff --git a/retrieval/model.py b/retrieval/model.py index 25cf385..174be09 100644 --- a/retrieval/model.py +++ b/retrieval/model.py @@ -1,4 +1,5 @@ """Ligihtning module for the premise retriever.""" + import os import math import torch diff --git a/scripts/data_stats.py b/scripts/data_stats.py index 03e7cc9..05037fe 100644 --- a/scripts/data_stats.py +++ b/scripts/data_stats.py @@ -1,4 +1,5 @@ """Scripts for computing some simple statistics about the data.""" + import json import argparse import numpy as np diff --git a/scripts/download_data.py b/scripts/download_data.py index 256ed9c..0a96b42 100644 --- a/scripts/download_data.py +++ b/scripts/download_data.py @@ -1,4 +1,5 @@ """Script to download LeanDojo Benchmark and LeanDojo Benchmark 4 into `./data`.""" + import os import argparse from hashlib import md5 @@ -9,11 +10,11 @@ "https://zenodo.org/records/10114157/files/leandojo_benchmark_v5.tar.gz" ) LEANDOJO_BENCHMARK_4_URL = ( - "https://zenodo.org/records/10114185/files/leandojo_benchmark_4_v5.tar.gz" + "https://zenodo.org/records/10811294/files/leandojo_benchmark_4_v7.tar.gz" ) DOWNLOADS = { LEANDOJO_BENCHMARK_URL: "4b256200618d4668b12a9cfe8c4df4d3", - LEANDOJO_BENCHMARK_4_URL: "5c1bb0ce1fd1572e8c3d0c3a642e356f", + LEANDOJO_BENCHMARK_4_URL: "cfb5ac28847b5a7c7856d7b28eefdc1b", }