format code

generator/datamodule.py

@@ -1,4 +1,5 @@
 """Data module for the tactic generator."""
+
 import os
 import json
 import pickle

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

generator/model.py

@@ -1,4 +1,5 @@
 """Lightning module for the tactic generator."""
+
 import torch
 import openai
 import pickle

prover/evaluate.py

@@ -1,5 +1,6 @@
 """Script for evaluating the prover on theorems extracted by LeanDojo.
 """
+
 import os
 import uuid
 import json

prover/proof_search.py

@@ -1,5 +1,6 @@
 """Proof search using best-first search.
 """
+
 import os
 import sys
 import ray

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 (

retrieval/bm25/main.py

@@ -1,4 +1,5 @@
 """Script for training the BM25 premise retriever."""
+
 import os
 import ray
 import json

retrieval/datamodule.py

@@ -1,4 +1,5 @@
 """Datamodule for the premise retrieval."""
+
 import os
 import json
 import torch

retrieval/evaluate.py

@@ -1,4 +1,5 @@
 """Script for evaluating the premise retriever."""
+
 import os
 import json
 import pickle

retrieval/index.py

@@ -1,5 +1,6 @@
 """Script for indexing the corpus using the retriever.
 """
+
 import torch
 import pickle
 import argparse

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

retrieval/model.py

@@ -1,4 +1,5 @@
 """Ligihtning module for the premise retriever."""
+
 import os
 import math
 import torch

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

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",
 }