diff --git a/scripts/generate-benchmark-lean4.ipynb b/scripts/generate-benchmark-lean4.ipynb index 91850cf..e6e9d8e 100644 --- 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",