diff --git a/scripts/generate-benchmark-lean3.ipynb b/scripts/generate-benchmark-lean3.ipynb
index a1a3db3..7f6e933 100644
--- a/scripts/generate-benchmark-lean3.ipynb
+++ b/scripts/generate-benchmark-lean3.ipynb
@@ -21,7 +21,7 @@
},
{
"cell_type": "code",
- "execution_count": 8,
+ "execution_count": 1,
"id": "cda71d78",
"metadata": {},
"outputs": [],
@@ -39,7 +39,6 @@
"\n",
"import lean_dojo\n",
"from lean_dojo import *\n",
- "from lean_dojo.constants import LEAN3_PACKAGES_DIR\n",
"\n",
"random.seed(3407) # https://arxiv.org/abs/2109.08203\n",
"\n",
@@ -61,7 +60,7 @@
},
{
"cell_type": "code",
- "execution_count": 9,
+ "execution_count": 2,
"id": "acdb4e64",
"metadata": {},
"outputs": [],
@@ -83,7 +82,7 @@
},
{
"cell_type": "code",
- "execution_count": 10,
+ "execution_count": 3,
"id": "0d7bcf76",
"metadata": {},
"outputs": [],
@@ -123,7 +122,7 @@
},
{
"cell_type": "code",
- "execution_count": 11,
+ "execution_count": 4,
"id": "a9e1fe70",
"metadata": {},
"outputs": [],
@@ -178,7 +177,7 @@
},
{
"cell_type": "code",
- "execution_count": 12,
+ "execution_count": 5,
"id": "8509a475",
"metadata": {},
"outputs": [],
@@ -205,14 +204,12 @@
},
{
"cell_type": "code",
- "execution_count": 13,
+ "execution_count": 8,
"id": "ac984a99",
"metadata": {},
"outputs": [],
"source": [
- "def export_proofs(\n",
- " traced_repo: TracedRepo, splits: Dict[SPLIT_STRATEGY, SPLIT], dst_path: Path\n",
- ") -> None:\n",
+ "def export_proofs(splits: Dict[SPLIT_STRATEGY, SPLIT], dst_path: Path) -> None:\n",
" \"\"\"Export all proofs in a traced repo to ``dst_path''.\"\"\"\n",
" for strategy, split in splits.items():\n",
" split_dir = dst_path / strategy\n",
@@ -322,7 +319,7 @@
" shutil.rmtree(dst_path)\n",
"\n",
" # Export the proofs.\n",
- " export_proofs(traced_repo, splits, dst_path)\n",
+ " export_proofs(splits, dst_path)\n",
"\n",
" # Export the premises (theorems, definitions, etc.).\n",
" export_premises(traced_repo, dst_path)\n",
@@ -344,7 +341,7 @@
},
{
"cell_type": "code",
- "execution_count": 14,
+ "execution_count": 9,
"id": "59eaebb3",
"metadata": {
"scrolled": true
@@ -354,114 +351,113 @@
"name": "stderr",
"output_type": "stream",
"text": [
- "\u001b[32m2024-01-08 12:50:44.659\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36mlean_dojo.data_extraction.trace\u001b[0m:\u001b[36mtrace\u001b[0m:\u001b[36m193\u001b[0m - \u001b[1mLoading the traced repo from /home/kaiyu/.cache/lean_dojo/leanprover-community-mathlib-19c869efa56bbb8b500f2724c0b77261edbfa28c/mathlib\u001b[0m\n",
- "2024-01-08 12:50:49,468\tINFO worker.py:1715 -- Started a local Ray instance. View the dashboard at \u001b[1m\u001b[32m127.0.0.1:8265 \u001b[39m\u001b[22m\n",
- "100%|██████████| 3384/3384 [05:19<00:00, 10.58it/s] \n",
- "\u001b[32m2024-01-08 12:56:33.412\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_data\u001b[0m:\u001b[36m3\u001b[0m - \u001b[1m98734 theorems in total\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:33.414\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_randomly\u001b[0m:\u001b[36m18\u001b[0m - \u001b[1mSplitting the theorems randomly\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:33.454\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_by_premise\u001b[0m:\u001b[36m8\u001b[0m - \u001b[1mSplitting the theorems by premises\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:39.143\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_data\u001b[0m:\u001b[36m109\u001b[0m - \u001b[33m\u001b[1m../leandojo_benchmark already exists. Removing it now.\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.110\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.111\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.111\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.112\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.113\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.113\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.113\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.114\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.114\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.115\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.115\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.lift\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.115\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.lift\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.116\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.116\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.117\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.117\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.118\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.118\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.656\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:40.657\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:41.625\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.ind\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:43.772\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:44.077\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.ind\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:44.429\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:44.430\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:45.043\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:45.044\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:45.045\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:45.045\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:45.046\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:45.046\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:45.047\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:45.047\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:45.047\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:45.048\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:45.048\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.lift\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:45.049\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.lift\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:45.049\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:45.049\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:45.050\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:45.050\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:45.749\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.ind\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:46.377\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:46.379\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:46.649\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.ind\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:48.358\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:48.359\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:55.129\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m39\u001b[0m - \u001b[1m94734 theorems and 208460 tactics saved to ../leandojo_benchmark/random/train.json\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:55.668\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m39\u001b[0m - \u001b[1m2000 theorems and 4652 tactics saved to ../leandojo_benchmark/random/val.json\u001b[0m\n",
- "\u001b[32m2024-01-08 12:56:56.001\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m39\u001b[0m - \u001b[1m2000 theorems and 4664 tactics saved to ../leandojo_benchmark/random/test.json\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:00.367\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:00.369\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:00.442\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:00.443\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:00.710\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:01.998\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:01.999\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.000\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.000\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.000\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.001\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.001\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.002\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.002\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.003\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.003\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.lift\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.003\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.lift\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.004\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.004\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.005\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.005\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.006\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.006\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.038\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.ind\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.040\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.ind\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.104\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.ind\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.105\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.ind\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.107\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.107\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.108\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.108\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.108\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.109\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.109\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.110\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.110\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.110\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.111\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.lift\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.111\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.lift\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.111\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.112\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.112\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.113\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.113\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.113\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.114\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:02.114\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:09.583\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m39\u001b[0m - \u001b[1m94734 theorems and 191524 tactics saved to ../leandojo_benchmark/novel_premises/train.json\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:10.549\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m39\u001b[0m - \u001b[1m2000 theorems and 12678 tactics saved to ../leandojo_benchmark/novel_premises/val.json\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:11.383\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m39\u001b[0m - \u001b[1m2000 theorems and 13574 tactics saved to ../leandojo_benchmark/novel_premises/test.json\u001b[0m\n",
- "\u001b[32m2024-01-08 12:57:44.321\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_premises\u001b[0m:\u001b[36m63\u001b[0m - \u001b[1m130283 theorems/definitions from 3384 files saved to ../leandojo_benchmark/corpus.jsonl\u001b[0m\n"
+ "\u001b[32m2024-01-18 14:28:38.144\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36mlean_dojo.data_extraction.trace\u001b[0m:\u001b[36mtrace\u001b[0m:\u001b[36m193\u001b[0m - \u001b[1mLoading the traced repo from /home/kaiyu/.cache/lean_dojo/leanprover-community-mathlib-19c869efa56bbb8b500f2724c0b77261edbfa28c/mathlib\u001b[0m\n",
+ "2024-01-18 14:28:51,151\tINFO worker.py:1715 -- Started a local Ray instance. View the dashboard at \u001b[1m\u001b[32m127.0.0.1:8267 \u001b[39m\u001b[22m\n",
+ "100%|██████████| 3384/3384 [06:49<00:00, 8.26it/s] \n",
+ "\u001b[32m2024-01-18 14:36:17.531\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_data\u001b[0m:\u001b[36m3\u001b[0m - \u001b[1m98734 theorems in total\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:17.533\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_randomly\u001b[0m:\u001b[36m18\u001b[0m - \u001b[1mSplitting the theorems randomly\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:17.604\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_by_premise\u001b[0m:\u001b[36m8\u001b[0m - \u001b[1mSplitting the theorems by premises\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:26.327\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:26.330\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:27.701\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:27.702\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:30.947\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:30.948\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:30.949\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:30.949\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:30.950\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:30.950\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:30.952\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:30.952\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:30.953\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:30.953\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:30.953\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.lift\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:30.954\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.lift\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:30.954\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:30.955\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:30.956\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:30.956\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:30.956\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:30.962\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:30.993\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:32.694\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:32.695\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:34.340\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.ind\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:35.934\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.ind\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:37.960\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:37.961\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:40.257\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.ind\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:40.334\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:40.336\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:40.337\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:40.337\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:40.337\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:40.338\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:40.338\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:40.339\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:40.339\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:40.340\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:40.340\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.lift\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:40.341\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.lift\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:40.341\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:40.342\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:40.342\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:40.342\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:40.915\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.ind\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:50.157\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m94734 theorems and 208847 tactics saved to ../leandojo_benchmark/random/train.json\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:51.639\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m2000 theorems and 4540 tactics saved to ../leandojo_benchmark/random/val.json\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:52.209\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m2000 theorems and 4389 tactics saved to ../leandojo_benchmark/random/test.json\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:58.795\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:58.796\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:58.903\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:58.905\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:36:59.828\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.542\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.543\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.544\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.545\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.545\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.546\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.546\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.547\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.548\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.549\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.549\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.lift\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.550\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.lift\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.550\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.551\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.551\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.552\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.553\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.554\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.584\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.ind\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.587\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.ind\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.628\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.ind\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.630\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.ind\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.632\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.632\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.633\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.633\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.634\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.634\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.634\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.635\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.635\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.636\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.636\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.lift\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.636\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.lift\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.637\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.637\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.638\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.638\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.639\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.639\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.640\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:01.641\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:13.547\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m94734 theorems and 191574 tactics saved to ../leandojo_benchmark/novel_premises/train.json\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:14.790\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m2000 theorems and 12685 tactics saved to ../leandojo_benchmark/novel_premises/val.json\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:15.789\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m2000 theorems and 13517 tactics saved to ../leandojo_benchmark/novel_premises/test.json\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:37:52.423\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_premises\u001b[0m:\u001b[36m61\u001b[0m - \u001b[1m130283 theorems/definitions from 3384 files saved to ../leandojo_benchmark/corpus.jsonl\u001b[0m\n"
]
}
],
@@ -515,7 +511,7 @@
},
{
"cell_type": "code",
- "execution_count": 15,
+ "execution_count": 10,
"id": "b1b97c12",
"metadata": {},
"outputs": [
@@ -541,7 +537,7 @@
},
{
"cell_type": "code",
- "execution_count": 16,
+ "execution_count": 11,
"id": "0eefe7b8",
"metadata": {},
"outputs": [
@@ -551,7 +547,7 @@
"dict_keys(['path', 'imports', 'premises'])"
]
},
- "execution_count": 16,
+ "execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
@@ -573,21 +569,21 @@
},
{
"cell_type": "code",
- "execution_count": 17,
+ "execution_count": 12,
"id": "05e1740f",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "('src/linear_algebra/affine_space/affine_equiv.lean',\n",
+ "('src/group_theory/index.lean',\n",
" ['_target/deps/lean/library/init/default.lean',\n",
- " 'src/linear_algebra/general_linear_group.lean',\n",
- " 'src/linear_algebra/affine_space/affine_map.lean',\n",
- " 'src/algebra/invertible.lean'])"
+ " 'src/group_theory/finiteness.lean',\n",
+ " 'src/data/finite/card.lean',\n",
+ " 'src/group_theory/group_action/quotient.lean'])"
]
},
- "execution_count": 17,
+ "execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
@@ -598,17 +594,17 @@
},
{
"cell_type": "code",
- "execution_count": 18,
+ "execution_count": 13,
"id": "04e6e71f",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "94"
+ "75"
]
},
- "execution_count": 18,
+ "execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
@@ -627,21 +623,21 @@
},
{
"cell_type": "code",
- "execution_count": 19,
+ "execution_count": 14,
"id": "c4b447b0",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "{'full_name': 'affine_equiv',\n",
- " 'code': \"@[nolint has_nonempty_instance]\\nstructure affine_equiv (k P₁ P₂ : Type*) {V₁ V₂ : Type*} [ring k]\\n [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁]\\n [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] extends P₁ ≃ P₂ :=\\n(linear : V₁ ≃ₗ[k] V₂)\\n(map_vadd' : ∀ (p : P₁) (v : V₁), to_equiv (v +ᵥ p) = linear v +ᵥ to_equiv p)\",\n",
- " 'start': [46, 1],\n",
- " 'end': [51, 78],\n",
- " 'kind': 'structure'}"
+ "{'full_name': 'subgroup.index',\n",
+ " 'code': '@[to_additive \"The index of a subgroup as a natural number,\\nand returns 0 if the index is infinite.\"]\\nnoncomputable def index : ℕ :=\\nnat.card (G ⧸ H)',\n",
+ " 'start': [45, 1],\n",
+ " 'end': [48, 17],\n",
+ " 'kind': 'definition'}"
]
},
- "execution_count": 19,
+ "execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
@@ -665,7 +661,7 @@
},
{
"cell_type": "code",
- "execution_count": 20,
+ "execution_count": 15,
"id": "a59b38b6",
"metadata": {},
"outputs": [
@@ -675,7 +671,7 @@
"94734"
]
},
- "execution_count": 20,
+ "execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
@@ -696,7 +692,7 @@
},
{
"cell_type": "code",
- "execution_count": 21,
+ "execution_count": 16,
"id": "9dc67dd2",
"metadata": {},
"outputs": [
@@ -706,7 +702,7 @@
"dict_keys(['url', 'commit', 'file_path', 'full_name', 'start', 'end', 'traced_tactics'])"
]
},
- "execution_count": 21,
+ "execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
@@ -720,20 +716,20 @@
},
{
"cell_type": "code",
- "execution_count": 22,
+ "execution_count": 17,
"id": "cc2bc340",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "('https://github.com/leanprover-community/lean',\n",
- " 'cce7990ea86a78bdb383e38ed7f9b5ba93c60ce0',\n",
- " 'library/init/data/array/basic.lean',\n",
- " 'd_array.of_beq_aux_eq_tt')"
+ "('https://github.com/leanprover-community/mathlib',\n",
+ " '19c869efa56bbb8b500f2724c0b77261edbfa28c',\n",
+ " 'src/topology/basic.lean',\n",
+ " \"filter.lift'_closure_eq_bot\")"
]
},
- "execution_count": 22,
+ "execution_count": 17,
"metadata": {},
"output_type": "execute_result"
}
@@ -752,17 +748,17 @@
},
{
"cell_type": "code",
- "execution_count": 23,
+ "execution_count": 18,
"id": "00315e27",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "13"
+ "1"
]
},
- "execution_count": 23,
+ "execution_count": 18,
"metadata": {},
"output_type": "execute_result"
}
@@ -781,32 +777,32 @@
},
{
"cell_type": "code",
- "execution_count": 24,
+ "execution_count": 19,
"id": "52769d80",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "{'tactic': \"have h₂' : read a ⟨i, h₁⟩ = read b ⟨i, h₁⟩ ∧ d_array.beq_aux a b i _ = tt\",\n",
- " 'annotated_tactic': [\"have h₂' : read a ⟨i, h₁⟩ = read b ⟨i, h₁⟩ ∧ d_array.beq_aux a b i _ = tt\",\n",
- " [{'full_name': 'd_array.read',\n",
- " 'def_path': '_target/deps/lean/library/init/data/array/basic.lean',\n",
- " 'def_pos': [22, 5]},\n",
- " {'full_name': 'd_array.read',\n",
- " 'def_path': '_target/deps/lean/library/init/data/array/basic.lean',\n",
- " 'def_pos': [22, 5]},\n",
- " {'full_name': 'd_array.beq_aux',\n",
- " 'def_path': '_target/deps/lean/library/init/data/array/basic.lean',\n",
- " 'def_pos': [74, 15]},\n",
- " {'full_name': 'bool.tt',\n",
- " 'def_path': '_target/deps/lean/library/init/core.lean',\n",
- " 'def_pos': [242, 11]}]],\n",
- " 'state_before': \"n : ℕ,\\nα : fin n → Type u,\\n_inst_1 : Π (i : fin n), decidable_eq (α i),\\na b : d_array n α,\\nof_beq_aux_eq_tt :\\n ∀ (i : ℕ) (h : i ≤ n),\\n a.beq_aux b i h = tt → ∀ (j : ℕ) (h' : j < i), a.read ⟨j, _⟩ = b.read ⟨j, _⟩,\\ni : ℕ,\\nh₁ : i + 1 ≤ n,\\nh₂ : a.beq_aux b (i + 1) h₁ = tt,\\nj : ℕ,\\nh₃ : j < i + 1\\n⊢ a.read ⟨j, _⟩ = b.read ⟨j, _⟩\",\n",
- " 'state_after': \"3 goals\\nn : ℕ,\\nα : fin n → Type u,\\n_inst_1 : Π (i : fin n), decidable_eq (α i),\\na b : d_array n α,\\nof_beq_aux_eq_tt :\\n ∀ (i : ℕ) (h : i ≤ n),\\n a.beq_aux b i h = tt → ∀ (j : ℕ) (h' : j < i), a.read ⟨j, _⟩ = b.read ⟨j, _⟩,\\ni : ℕ,\\nh₁ : i + 1 ≤ n,\\nh₂ : a.beq_aux b (i + 1) h₁ = tt,\\nj : ℕ,\\nh₃ : j < i + 1\\n⊢ a.read ⟨i, h₁⟩ = b.read ⟨i, h₁⟩ ∧ a.beq_aux b i ?m_1 = tt\\n\\nn : ℕ,\\nα : fin n → Type u,\\n_inst_1 : Π (i : fin n), decidable_eq (α i),\\na b : d_array n α,\\nof_beq_aux_eq_tt :\\n ∀ (i : ℕ) (h : i ≤ n),\\n a.beq_aux b i h = tt → ∀ (j : ℕ) (h' : j < i), a.read ⟨j, _⟩ = b.read ⟨j, _⟩,\\ni : ℕ,\\nh₁ : i + 1 ≤ n,\\nh₂ : a.beq_aux b (i + 1) h₁ = tt,\\nj : ℕ,\\nh₃ : j < i + 1,\\nh₂' : a.read ⟨i, h₁⟩ = b.read ⟨i, h₁⟩ ∧ a.beq_aux b i ?m_1 = tt\\n⊢ a.read ⟨j, _⟩ = b.read ⟨j, _⟩\\n\\nn : ℕ,\\nα : fin n → Type u,\\n_inst_1 : Π (i : fin n), decidable_eq (α i),\\na b : d_array n α,\\nof_beq_aux_eq_tt :\\n ∀ (i : ℕ) (h : i ≤ n),\\n a.beq_aux b i h = tt → ∀ (j : ℕ) (h' : j < i), a.read ⟨j, _⟩ = b.read ⟨j, _⟩,\\ni : ℕ,\\nh₁ : i + 1 ≤ n,\\nh₂ : a.beq_aux b (i + 1) h₁ = tt,\\nj : ℕ,\\nh₃ : j < i + 1\\n⊢ i ≤ n\"}"
+ "{'tactic': \"rw [lift'_bot (monotone_closure _), closure_empty, principal_empty]\",\n",
+ " 'annotated_tactic': [\"rw [lift'_bot (monotone_closure _), closure_empty, principal_empty]\",\n",
+ " [{'full_name': \"filter.lift'_bot\",\n",
+ " 'def_path': 'src/order/filter/lift.lean',\n",
+ " 'def_pos': [298, 7]},\n",
+ " {'full_name': 'monotone_closure',\n",
+ " 'def_path': 'src/topology/basic.lean',\n",
+ " 'def_pos': [369, 7]},\n",
+ " {'full_name': 'closure_empty',\n",
+ " 'def_path': 'src/topology/basic.lean',\n",
+ " 'def_pos': [389, 15]},\n",
+ " {'full_name': 'filter.principal_empty',\n",
+ " 'def_path': 'src/order/filter/basic.lean',\n",
+ " 'def_pos': [589, 15]}]],\n",
+ " 'state_before': \"α : Type u,\\n_inst_1 : topological_space α,\\nl : filter α,\\nh : l = ⊥\\n⊢ ⊥.lift' closure = ⊥\",\n",
+ " 'state_after': 'no goals'}"
]
},
- "execution_count": 24,
+ "execution_count": 19,
"metadata": {},
"output_type": "execute_result"
}
@@ -835,7 +831,7 @@
},
{
"cell_type": "code",
- "execution_count": 25,
+ "execution_count": 22,
"id": "bc457ce9",
"metadata": {},
"outputs": [
@@ -843,14 +839,14 @@
"name": "stderr",
"output_type": "stream",
"text": [
- "\u001b[32m2024-01-08 13:03:50.671\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36mlean_dojo.data_extraction.trace\u001b[0m:\u001b[36mtrace\u001b[0m:\u001b[36m193\u001b[0m - \u001b[1mLoading the traced repo from /home/kaiyu/.cache/lean_dojo/facebookresearch-miniF2F-5271ddec788677c815cf818a06f368ef6498a106/miniF2F\u001b[0m\n",
- "2024-01-08 13:03:58,678\tINFO worker.py:1715 -- Started a local Ray instance. View the dashboard at \u001b[1m\u001b[32m127.0.0.1:8265 \u001b[39m\u001b[22m\n",
- "100%|██████████| 1159/1159 [02:29<00:00, 7.77it/s] \n",
- "\u001b[32m2024-01-08 13:06:43.405\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_data\u001b[0m:\u001b[36m109\u001b[0m - \u001b[33m\u001b[1m../leandojo_minif2f already exists. Removing it now.\u001b[0m\n",
- "\u001b[32m2024-01-08 13:06:43.435\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m39\u001b[0m - \u001b[1m244 theorems and 549 tactics saved to ../leandojo_minif2f/default/val.json\u001b[0m\n",
- "\u001b[32m2024-01-08 13:06:43.445\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
- "\u001b[32m2024-01-08 13:06:43.469\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m39\u001b[0m - \u001b[1m245 theorems and 781 tactics saved to ../leandojo_minif2f/default/test.json\u001b[0m\n",
- "\u001b[32m2024-01-08 13:06:58.519\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_premises\u001b[0m:\u001b[36m63\u001b[0m - \u001b[1m67170 theorems/definitions from 1159 files saved to ../leandojo_minif2f/corpus.jsonl\u001b[0m\n"
+ "\u001b[32m2024-01-18 17:11:01.175\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36mlean_dojo.data_extraction.trace\u001b[0m:\u001b[36mtrace\u001b[0m:\u001b[36m193\u001b[0m - \u001b[1mLoading the traced repo from /home/kaiyu/.cache/lean_dojo/facebookresearch-miniF2F-5271ddec788677c815cf818a06f368ef6498a106/miniF2F\u001b[0m\n",
+ "2024-01-18 17:11:14,392\tINFO worker.py:1715 -- Started a local Ray instance. View the dashboard at \u001b[1m\u001b[32m127.0.0.1:8265 \u001b[39m\u001b[22m\n",
+ "100%|██████████| 1159/1159 [00:36<00:00, 32.00it/s] \n",
+ "\u001b[32m2024-01-18 17:12:08.394\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_data\u001b[0m:\u001b[36m107\u001b[0m - \u001b[33m\u001b[1m../leandojo_minif2f already exists. Removing it now.\u001b[0m\n",
+ "\u001b[32m2024-01-18 17:12:08.430\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m244 theorems and 549 tactics saved to ../leandojo_minif2f/default/val.json\u001b[0m\n",
+ "\u001b[32m2024-01-18 17:12:08.446\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.traced_data\u001b[0m:\u001b[36m_callback3\u001b[0m:\u001b[36m226\u001b[0m - \u001b[33m\u001b[1mUnable to locate quot.mk\u001b[0m\n",
+ "\u001b[32m2024-01-18 17:12:08.477\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m245 theorems and 781 tactics saved to ../leandojo_minif2f/default/test.json\u001b[0m\n",
+ "\u001b[32m2024-01-18 17:12:25.299\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_premises\u001b[0m:\u001b[36m61\u001b[0m - \u001b[1m67170 theorems/definitions from 1159 files saved to ../leandojo_minif2f/corpus.jsonl\u001b[0m\n"
]
}
],
@@ -879,7 +875,7 @@
},
{
"cell_type": "code",
- "execution_count": 26,
+ "execution_count": 23,
"id": "12f436c7",
"metadata": {},
"outputs": [
@@ -887,18 +883,12 @@
"name": "stderr",
"output_type": "stream",
"text": [
- "\u001b[32m2024-01-08 13:07:00.088\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36mlean_dojo.data_extraction.trace\u001b[0m:\u001b[36mtrace\u001b[0m:\u001b[36m193\u001b[0m - \u001b[1mLoading the traced repo from /home/kaiyu/.cache/lean_dojo/zhangir-azerbayev-ProofNet-e8645aa830ce17c33a8b8482a8195f0f97d6a74a/ProofNet\u001b[0m\n"
- ]
- },
- {
- "name": "stderr",
- "output_type": "stream",
- "text": [
- "2024-01-08 13:07:09,769\tINFO worker.py:1715 -- Started a local Ray instance. View the dashboard at \u001b[1m\u001b[32m127.0.0.1:8265 \u001b[39m\u001b[22m\n",
- "100%|██████████| 1539/1539 [03:06<00:00, 8.25it/s] \n",
- "\u001b[32m2024-01-08 13:10:34.216\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_data\u001b[0m:\u001b[36m109\u001b[0m - \u001b[33m\u001b[1m../leandojo_proofnet already exists. Removing it now.\u001b[0m\n",
- "\u001b[32m2024-01-08 13:10:34.257\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m39\u001b[0m - \u001b[1m374 theorems and 460 tactics saved to ../leandojo_proofnet/default/test.json\u001b[0m\n",
- "\u001b[32m2024-01-08 13:10:52.466\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_premises\u001b[0m:\u001b[36m63\u001b[0m - \u001b[1m82365 theorems/definitions from 1539 files saved to ../leandojo_proofnet/corpus.jsonl\u001b[0m\n"
+ "\u001b[32m2024-01-18 17:12:25.313\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36mlean_dojo.data_extraction.trace\u001b[0m:\u001b[36mtrace\u001b[0m:\u001b[36m193\u001b[0m - \u001b[1mLoading the traced repo from /home/kaiyu/.cache/lean_dojo/zhangir-azerbayev-ProofNet-e8645aa830ce17c33a8b8482a8195f0f97d6a74a/ProofNet\u001b[0m\n",
+ "2024-01-18 17:12:39,801\tINFO worker.py:1715 -- Started a local Ray instance. View the dashboard at \u001b[1m\u001b[32m127.0.0.1:8265 \u001b[39m\u001b[22m\n",
+ "100%|██████████| 1539/1539 [04:28<00:00, 5.74it/s] \n",
+ "\u001b[32m2024-01-18 17:17:34.399\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_data\u001b[0m:\u001b[36m107\u001b[0m - \u001b[33m\u001b[1m../leandojo_proofnet already exists. Removing it now.\u001b[0m\n",
+ "\u001b[32m2024-01-18 17:17:34.455\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m374 theorems and 460 tactics saved to ../leandojo_proofnet/default/test.json\u001b[0m\n",
+ "\u001b[32m2024-01-18 17:18:04.487\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_premises\u001b[0m:\u001b[36m61\u001b[0m - \u001b[1m82365 theorems/definitions from 1539 files saved to ../leandojo_proofnet/corpus.jsonl\u001b[0m\n"
]
}
],
diff --git a/scripts/generate-benchmark-lean4.ipynb b/scripts/generate-benchmark-lean4.ipynb
index dd023cc..3e45221 100644
--- a/scripts/generate-benchmark-lean4.ipynb
+++ b/scripts/generate-benchmark-lean4.ipynb
@@ -207,7 +207,7 @@
},
{
"cell_type": "code",
- "execution_count": 6,
+ "execution_count": 8,
"id": "06e6fe8d",
"metadata": {},
"outputs": [],
@@ -322,7 +322,7 @@
" shutil.rmtree(dst_path)\n",
"\n",
" # Export the proofs.\n",
- " export_proofs(traced_repo, splits, dst_path)\n",
+ " export_proofs(splits, dst_path)\n",
"\n",
" # Export the premises (theorems, definitions, etc.).\n",
" export_premises(traced_repo, dst_path)\n",
@@ -336,7 +336,7 @@
},
{
"cell_type": "code",
- "execution_count": 7,
+ "execution_count": 9,
"id": "bc50220e",
"metadata": {
"scrolled": true
@@ -346,19 +346,19 @@
"name": "stderr",
"output_type": "stream",
"text": [
- "\u001b[32m2024-01-05 07:00:47.696\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36mlean_dojo.data_extraction.trace\u001b[0m:\u001b[36mtrace\u001b[0m:\u001b[36m182\u001b[0m - \u001b[1mLoading the traced repo from /home/kaiyu/.cache/lean_dojo/leanprover-community-mathlib4-3ce43c18f614b76e161f911b75a3e1ef641620ff/mathlib4\u001b[0m\n",
- "2024-01-05 07:00:49,725\tINFO worker.py:1715 -- Started a local Ray instance. View the dashboard at \u001b[1m\u001b[32m127.0.0.1:8265 \u001b[39m\u001b[22m\n",
- "100%|██████████| 4462/4462 [07:30<00:00, 9.91it/s] \n",
- "\u001b[32m2024-01-05 07:09:20.238\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_data\u001b[0m:\u001b[36m6\u001b[0m - \u001b[1m102514 theorems in total\u001b[0m\n",
- "\u001b[32m2024-01-05 07:09:20.239\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_randomly\u001b[0m:\u001b[36m18\u001b[0m - \u001b[1mSplitting the theorems randomly\u001b[0m\n",
- "\u001b[32m2024-01-05 07:09:20.280\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_by_premise\u001b[0m:\u001b[36m8\u001b[0m - \u001b[1mSplitting the theorems by premises\u001b[0m\n",
- "\u001b[32m2024-01-05 07:09:51.565\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m39\u001b[0m - \u001b[1m98514 theorems and 205056 tactics saved to ../leandojo_benchmark_4/random/train.json\u001b[0m\n",
- "\u001b[32m2024-01-05 07:09:52.297\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m39\u001b[0m - \u001b[1m2000 theorems and 4173 tactics saved to ../leandojo_benchmark_4/random/val.json\u001b[0m\n",
- "\u001b[32m2024-01-05 07:09:52.754\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m39\u001b[0m - \u001b[1m2000 theorems and 3990 tactics saved to ../leandojo_benchmark_4/random/test.json\u001b[0m\n",
- "\u001b[32m2024-01-05 07:10:13.319\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m39\u001b[0m - \u001b[1m98514 theorems and 195071 tactics saved to ../leandojo_benchmark_4/novel_premises/train.json\u001b[0m\n",
- "\u001b[32m2024-01-05 07:10:14.409\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m39\u001b[0m - \u001b[1m2000 theorems and 8843 tactics saved to ../leandojo_benchmark_4/novel_premises/val.json\u001b[0m\n",
- "\u001b[32m2024-01-05 07:10:15.358\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m39\u001b[0m - \u001b[1m2000 theorems and 9305 tactics saved to ../leandojo_benchmark_4/novel_premises/test.json\u001b[0m\n",
- "\u001b[32m2024-01-05 07:10:40.680\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_premises\u001b[0m:\u001b[36m63\u001b[0m - \u001b[1m152695 theorems/definitions from 4462 files saved to ../leandojo_benchmark_4/corpus.jsonl\u001b[0m\n"
+ "\u001b[32m2024-01-18 14:28:18.667\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36mlean_dojo.data_extraction.trace\u001b[0m:\u001b[36mtrace\u001b[0m:\u001b[36m193\u001b[0m - \u001b[1mLoading the traced repo from /home/kaiyu/.cache/lean_dojo/leanprover-community-mathlib4-3ce43c18f614b76e161f911b75a3e1ef641620ff/mathlib4\u001b[0m\n",
+ "2024-01-18 14:28:27,148\tINFO worker.py:1715 -- Started a local Ray instance. View the dashboard at \u001b[1m\u001b[32m127.0.0.1:8265 \u001b[39m\u001b[22m\n",
+ "100%|██████████| 4462/4462 [23:45<00:00, 3.13it/s] \n",
+ "\u001b[32m2024-01-18 14:53:12.008\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_data\u001b[0m:\u001b[36m6\u001b[0m - \u001b[1m106248 theorems in total\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:53:12.010\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_randomly\u001b[0m:\u001b[36m18\u001b[0m - \u001b[1mSplitting the theorems randomly\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:53:12.058\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_by_premise\u001b[0m:\u001b[36m8\u001b[0m - \u001b[1mSplitting the theorems by premises\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:57:45.598\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m102248 theorems and 212584 tactics saved to ../leandojo_benchmark_4/random/train.json\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:57:46.455\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m2000 theorems and 4340 tactics saved to ../leandojo_benchmark_4/random/val.json\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:57:47.126\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m2000 theorems and 3628 tactics saved to ../leandojo_benchmark_4/random/test.json\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:58:12.494\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m102248 theorems and 202196 tactics saved to ../leandojo_benchmark_4/novel_premises/train.json\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:58:13.907\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m2000 theorems and 9334 tactics saved to ../leandojo_benchmark_4/novel_premises/val.json\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:58:14.971\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m2000 theorems and 9022 tactics saved to ../leandojo_benchmark_4/novel_premises/test.json\u001b[0m\n",
+ "\u001b[32m2024-01-18 14:58:47.950\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_premises\u001b[0m:\u001b[36m61\u001b[0m - \u001b[1m152695 theorems/definitions from 4462 files saved to ../leandojo_benchmark_4/corpus.jsonl\u001b[0m\n"
]
}
],
@@ -408,7 +408,7 @@
},
{
"cell_type": "code",
- "execution_count": 8,
+ "execution_count": 10,
"id": "7427982d",
"metadata": {},
"outputs": [
@@ -434,7 +434,7 @@
},
{
"cell_type": "code",
- "execution_count": 9,
+ "execution_count": 11,
"id": "cbca21c9",
"metadata": {},
"outputs": [
@@ -444,7 +444,7 @@
"dict_keys(['path', 'imports', 'premises'])"
]
},
- "execution_count": 9,
+ "execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
@@ -466,22 +466,21 @@
},
{
"cell_type": "code",
- "execution_count": 10,
+ "execution_count": 12,
"id": "f5c1920a",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "('Mathlib/Analysis/SpecificLimits/Normed.lean',\n",
- " ['Mathlib/Analysis/Asymptotics/Asymptotics.lean',\n",
- " 'Mathlib/Data/List/TFAE.lean',\n",
+ "('Mathlib/Data/Polynomial/FieldDivision.lean',\n",
+ " ['Mathlib/RingTheory/EuclideanDomain.lean',\n",
" 'lake-packages/lean4/src/lean/Init.lean',\n",
- " 'Mathlib/Analysis/SpecificLimits/Basic.lean',\n",
- " 'Mathlib/Algebra/Order/Field/Basic.lean'])"
+ " 'Mathlib/Data/Polynomial/Derivative.lean',\n",
+ " 'Mathlib/Data/Polynomial/RingDivision.lean'])"
]
},
- "execution_count": 10,
+ "execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
@@ -492,17 +491,17 @@
},
{
"cell_type": "code",
- "execution_count": 11,
+ "execution_count": 13,
"id": "d801a0ae",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "59"
+ "67"
]
},
- "execution_count": 11,
+ "execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
@@ -521,21 +520,21 @@
},
{
"cell_type": "code",
- "execution_count": 12,
+ "execution_count": 14,
"id": "b533d342",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "{'full_name': 'tendsto_norm_atTop_atTop',\n",
- " 'code': 'theorem tendsto_norm_atTop_atTop : Tendsto (norm : ℝ → ℝ) atTop atTop',\n",
- " 'start': [30, 1],\n",
- " 'end': [31, 26],\n",
+ "{'full_name': 'Polynomial.derivative_rootMultiplicity_of_root',\n",
+ " 'code': 'theorem derivative_rootMultiplicity_of_root [CharZero R] {p : R[X]} {t : R} (hpt : p.IsRoot t) :\\n p.derivative.rootMultiplicity t = p.rootMultiplicity t - 1',\n",
+ " 'start': [34, 1],\n",
+ " 'end': [57, 20],\n",
" 'kind': 'commanddeclaration'}"
]
},
- "execution_count": 12,
+ "execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
@@ -559,17 +558,17 @@
},
{
"cell_type": "code",
- "execution_count": 13,
+ "execution_count": 15,
"id": "4fb19aa3",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "98514"
+ "102248"
]
},
- "execution_count": 13,
+ "execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
@@ -590,7 +589,7 @@
},
{
"cell_type": "code",
- "execution_count": 14,
+ "execution_count": 21,
"id": "3cc47f7e",
"metadata": {},
"outputs": [
@@ -600,13 +599,13 @@
"dict_keys(['url', 'commit', 'file_path', 'full_name', 'start', 'end', 'traced_tactics'])"
]
},
- "execution_count": 14,
+ "execution_count": 21,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- "for proof in proofs_train:\n",
+ "for proof in proofs_train[::-1]:\n",
" if proof[\"traced_tactics\"] != []:\n",
" break\n",
"proof.keys()"
@@ -614,7 +613,7 @@
},
{
"cell_type": "code",
- "execution_count": 15,
+ "execution_count": 22,
"id": "3c2c36a7",
"metadata": {},
"outputs": [
@@ -623,11 +622,11 @@
"text/plain": [
"('https://github.com/leanprover-community/mathlib4',\n",
" '3ce43c18f614b76e161f911b75a3e1ef641620ff',\n",
- " 'Mathlib/Analysis/LocallyConvex/WithSeminorms.lean',\n",
- " 'WithSeminorms.first_countable')"
+ " 'Mathlib/Order/Filter/Bases.lean',\n",
+ " \"Filter.countable_biInf_eq_iInf_seq'\")"
]
},
- "execution_count": 15,
+ "execution_count": 22,
"metadata": {},
"output_type": "execute_result"
}
@@ -646,17 +645,17 @@
},
{
"cell_type": "code",
- "execution_count": 16,
+ "execution_count": 23,
"id": "c29987ff",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "8"
+ "5"
]
},
- "execution_count": 16,
+ "execution_count": 23,
"metadata": {},
"output_type": "execute_result"
}
@@ -675,30 +674,30 @@
},
{
"cell_type": "code",
- "execution_count": 18,
+ "execution_count": 25,
"id": "a734d788",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "{'tactic': 'exact Filter.iInf.isCountablyGenerated _',\n",
- " 'annotated_tactic': ['exact Filter.iInf.isCountablyGenerated _',\n",
- " [{'full_name': 'Filter.iInf.isCountablyGenerated',\n",
- " 'def_path': 'Mathlib/Order/Filter/Bases.lean',\n",
- " 'def_pos': [1196, 10],\n",
- " 'def_end_pos': [1196, 35]}]],\n",
- " 'state_before': \"𝕜 : Type u_1\\n𝕜₂ : Type u_2\\n𝕝 : Type u_3\\n𝕝₂ : Type u_4\\nE : Type u_5\\nF : Type u_6\\nG : Type u_7\\nι : Type u_8\\nι' : Type u_9\\ninst✝⁵ : NontriviallyNormedField 𝕜\\ninst✝⁴ : AddCommGroup E\\ninst✝³ : Module 𝕜 E\\ninst✝² : Nonempty ι\\ninst✝¹ : Countable ι\\np : SeminormFamily 𝕜 E ι\\ninst✝ : TopologicalSpace E\\nhp : WithSeminorms p\\nthis✝ : TopologicalAddGroup E\\nx✝ : UniformSpace E := TopologicalAddGroup.toUniformSpace E\\nthis : UniformAddGroup E\\n⊢ IsCountablyGenerated (⨅ i, comap (↑(p i)) (𝓝 0))\",\n",
- " 'state_after': 'no goals'}"
+ "{'tactic': 'rw [hB, iInf_emptyset]',\n",
+ " 'annotated_tactic': ['rw [hB, iInf_emptyset]',\n",
+ " [{'full_name': 'iInf_emptyset',\n",
+ " 'def_path': 'Mathlib/Order/CompleteLattice.lean',\n",
+ " 'def_pos': [1466, 9],\n",
+ " 'def_end_pos': [1466, 22]}]],\n",
+ " 'state_before': \"case inl\\nα : Type u_1\\nβ : Type u_2\\nγ : Type u_3\\nι : Type u_4\\nι' : Sort u_5\\ninst✝ : CompleteLattice α\\nB : Set ι\\nBcbl : Set.Countable B\\nf : ι → α\\ni₀ : ι\\nh : f i₀ = ⊤\\nhB : B = ∅\\n⊢ ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)\",\n",
+ " 'state_after': \"case inl\\nα : Type u_1\\nβ : Type u_2\\nγ : Type u_3\\nι : Type u_4\\nι' : Sort u_5\\ninst✝ : CompleteLattice α\\nB : Set ι\\nBcbl : Set.Countable B\\nf : ι → α\\ni₀ : ι\\nh : f i₀ = ⊤\\nhB : B = ∅\\n⊢ ∃ x, ⊤ = ⨅ i, f (x i)\"}"
]
},
- "execution_count": 18,
+ "execution_count": 25,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
- "proof[\"traced_tactics\"][-1]"
+ "proof[\"traced_tactics\"][1]"
]
},
{
diff --git a/src/lean_dojo/data_extraction/lean.py b/src/lean_dojo/data_extraction/lean.py
index 0bd917a..d1731c9 100644
--- a/src/lean_dojo/data_extraction/lean.py
+++ b/src/lean_dojo/data_extraction/lean.py
@@ -581,7 +581,10 @@ def _parse_lakefile_dependencies(
elif len(rev) == 40 and _COMMIT_REGEX.fullmatch(rev):
commit = rev
else:
- commit = _to_commit_hash(url_to_repo(url), rev)
+ try:
+ commit = _to_commit_hash(url_to_repo(url), rev)
+ except ValueError:
+ commit = get_latest_commit(url)
assert _COMMIT_REGEX.fullmatch(commit)
deps.append((m["name"], LeanGitRepo(url, commit)))
@@ -606,9 +609,7 @@ def _get_lean4_dependencies(
else json.load((Path(path) / "lake-manifest.json").open())
)
for pkg in lake_manifest["packages"]:
- deps[pkg["git"]["name"]] = LeanGitRepo(
- pkg["git"]["url"], pkg["git"]["rev"]
- )
+ deps[pkg["name"]] = LeanGitRepo(pkg["url"], pkg["rev"])
except Exception:
lakefile = (
self.get_config("lakefile.lean")