format code

lean-dojo · Mar 16, 2024 · 9e50187 · 9e50187
1 parent 18d41b7
commit 9e50187
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/scripts/generate-benchmark-lean4.ipynb b/scripts/generate-benchmark-lean4.ipynb
@@ -225,7 +225,9 @@
     "        raise ValueError(f\"Unable to find the dependency {thm.repo}\")\n",
     "\n",
     "\n",
-    "def export_proofs(splits: Dict[SPLIT_STRATEGY, SPLIT], dst_path: Path, traced_repo: TracedRepo) -> None:\n",
+    "def export_proofs(\n",
+    "    splits: Dict[SPLIT_STRATEGY, SPLIT], dst_path: Path, traced_repo: TracedRepo\n",
+    ") -> 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",
@@ -252,7 +254,7 @@
     "                    {\n",
     "                        \"url\": thm.repo.url,\n",
     "                        \"commit\": thm.repo.commit,\n",
-    "                        \"file_path\":  _get_file_path(traced_repo, thm),\n",
+    "                        \"file_path\": _get_file_path(traced_repo, thm),\n",
     "                        \"full_name\": thm.theorem.full_name,\n",
     "                        \"start\": list(thm.start),\n",
     "                        \"end\": list(thm.end),\n",