diff --git a/src/lean_dojo/constants.py b/src/lean_dojo/constants.py index 838e8571..e4cef1bd 100644 --- a/src/lean_dojo/constants.py +++ b/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 diff --git a/src/lean_dojo/container.py b/src/lean_dojo/container.py index d3d7c7b7..9853b0d5 100644 --- a/src/lean_dojo/container.py +++ b/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 diff --git a/src/lean_dojo/data_extraction/ast/lean4/node.py b/src/lean_dojo/data_extraction/ast/lean4/node.py index 45b8c40a..61a9261d 100644 --- a/src/lean_dojo/data_extraction/ast/lean4/node.py +++ b/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( diff --git a/src/lean_dojo/data_extraction/build_lean3_repo.py b/src/lean_dojo/data_extraction/build_lean3_repo.py index 2bc1b127..d687ff47 100644 --- a/src/lean_dojo/data_extraction/build_lean3_repo.py +++ b/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 diff --git a/src/lean_dojo/data_extraction/build_lean4_repo.py b/src/lean_dojo/data_extraction/build_lean4_repo.py index b0468cf4..6593c56c 100644 --- a/src/lean_dojo/data_extraction/build_lean4_repo.py +++ b/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 diff --git a/src/lean_dojo/data_extraction/cache.py b/src/lean_dojo/data_extraction/cache.py index 52afb761..71375391 100644 --- a/src/lean_dojo/data_extraction/cache.py +++ b/src/lean_dojo/data_extraction/cache.py @@ -1,5 +1,6 @@ """Cache manager of traced repos. """ + import os import shutil import tarfile diff --git a/src/lean_dojo/data_extraction/lean.py b/src/lean_dojo/data_extraction/lean.py index 258a8dee..4af5325b 100644 --- a/src/lean_dojo/data_extraction/lean.py +++ b/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 diff --git a/src/lean_dojo/data_extraction/trace.py b/src/lean_dojo/data_extraction/trace.py index fb9f1327..367ba72e 100644 --- a/src/lean_dojo/data_extraction/trace.py +++ b/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 diff --git a/src/lean_dojo/data_extraction/traced_data.py b/src/lean_dojo/data_extraction/traced_data.py index 8ad9f07c..ec42a9a6 100644 --- a/src/lean_dojo/data_extraction/traced_data.py +++ b/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 diff --git a/src/lean_dojo/interaction/parse_goals.py b/src/lean_dojo/interaction/parse_goals.py index 42bede04..64727315 100644 --- a/src/lean_dojo/interaction/parse_goals.py +++ b/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 diff --git a/src/lean_dojo/utils.py b/src/lean_dojo/utils.py index 0f792e60..08917615 100644 --- a/src/lean_dojo/utils.py +++ b/src/lean_dojo/utils.py @@ -1,5 +1,6 @@ """Utility functions used internally by LeanDojo. """ + import re import os import ray