reformat code

src/lean_dojo/constants.py

@@ -1,6 +1,7 @@
 """Constants controlling LeanDojo's behaviors. 
 Many of them are configurable via :ref:`environment-variables`.
 """
+
 import os
 import re
 import sys

src/lean_dojo/container.py

@@ -2,6 +2,7 @@
 Currently, LeanDojo supports two types of containers: ``docker`` and ``native``. 
 The former is the default and recommended option, while the latter is experimental.
 """
+
 import os
 import shlex
 import signal

src/lean_dojo/data_extraction/ast/lean4/node.py

@@ -361,9 +361,9 @@ def from_data(cls, node_data: Dict[str, Any], lean_file: LeanFile) -> "GroupNode
 class MathlibTacticLemmaNode4(Node4):
     name: str
     full_name: Optional[str] = None
-    _is_private_decl: Optional[
-        bool
-    ] = False  # `_is_private` doesn't play well with lxml.
+    _is_private_decl: Optional[bool] = (
+        False  # `_is_private` doesn't play well with lxml.
+    )
 
     @classmethod
     def from_data(
@@ -1027,9 +1027,9 @@ def from_data(
 class CommandTheoremNode4(Node4):
     name: str
     full_name: Optional[str] = None
-    _is_private_decl: Optional[
-        bool
-    ] = False  # `_is_private` doesn't play well with lxml.
+    _is_private_decl: Optional[bool] = (
+        False  # `_is_private` doesn't play well with lxml.
+    )
 
     @classmethod
     def from_data(

src/lean_dojo/data_extraction/build_lean3_repo.py

@@ -2,6 +2,7 @@
 
 Only this file runs in Docker. So it must be self-contained.
 """
+
 import os
 import sys
 import toml

src/lean_dojo/data_extraction/build_lean4_repo.py

@@ -2,6 +2,7 @@
 
 Only this file runs in Docker. So it must be self-contained.
 """
+
 import os
 import re
 import shutil

src/lean_dojo/data_extraction/cache.py

@@ -1,5 +1,6 @@
 """Cache manager of traced repos.
 """
+
 import os
 import shutil
 import tarfile

src/lean_dojo/data_extraction/lean.py

@@ -1,6 +1,7 @@
 """This module define classes for repos, files, and theorems in Lean. 
 Objects of these classes contain only surface information, without extracting any trace.
 """
+
 import re
 import os
 import json

src/lean_dojo/data_extraction/trace.py

@@ -2,6 +2,7 @@
 To estimate the time for tracing a repo, a good rule of thumb is 1.5x the time for compiling the repo using :code:`leanpkg build`.
 A repo has to be traced only once, and the traced repo will be stored in a cache for fast access in the future.
 """
+
 import shutil
 from pathlib import Path
 from loguru import logger

src/lean_dojo/data_extraction/traced_data.py

@@ -1,5 +1,6 @@
 """This module defines traced repos/files/theorems.
 """
+
 import re
 import os
 import ray

src/lean_dojo/interaction/parse_goals.py

@@ -1,5 +1,6 @@
 """Utilities for parsing Lean's pretty-printed proof goals.
 """
+
 import re
 from typing import List
 from dataclasses import dataclass

src/lean_dojo/utils.py

@@ -1,5 +1,6 @@
 """Utility functions used internally by LeanDojo.
 """
+
 import re
 import os
 import ray