From 8896814bbed00062fb64cf492dcd39dc806610fd Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Sun, 11 Aug 2024 21:13:44 +0000 Subject: [PATCH] fix minor bugs --- docs/source/conf.py | 2 +- pyproject.toml | 2 +- src/lean_dojo/constants.py | 2 +- src/lean_dojo/data_extraction/lean.py | 38 +++++++++++++++++++-------- 4 files changed, 30 insertions(+), 14 deletions(-) diff --git a/docs/source/conf.py b/docs/source/conf.py index e12d4d8..caed532 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -13,7 +13,7 @@ project = "LeanDojo" copyright = "2023, LeanDojo Team" author = "Kaiyu Yang" -release = "2.1.0" +release = "2.1.1" # -- General configuration --------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration diff --git a/pyproject.toml b/pyproject.toml index fec8ce5..0fa4339 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -12,7 +12,7 @@ exclude = [ [project] name = "lean-dojo" -version = "2.1.0" +version = "2.1.1" authors = [ { name="Kaiyu Yang", email="kaiyuy@meta.com" }, ] diff --git a/src/lean_dojo/constants.py b/src/lean_dojo/constants.py index 590c23a..b640a5e 100644 --- a/src/lean_dojo/constants.py +++ b/src/lean_dojo/constants.py @@ -14,7 +14,7 @@ load_dotenv() -__version__ = "2.1.0" +__version__ = "2.1.1" logger.remove() if "VERBOSE" in os.environ or "DEBUG" in os.environ: diff --git a/src/lean_dojo/data_extraction/lean.py b/src/lean_dojo/data_extraction/lean.py index e3aabc9..b86afd9 100644 --- a/src/lean_dojo/data_extraction/lean.py +++ b/src/lean_dojo/data_extraction/lean.py @@ -736,15 +736,23 @@ def _parse_lakefile_toml_dependencies( def get_license(self) -> Optional[str]: """Return the content of the ``LICENSE`` file.""" - assert "github.com" in self.url, f"Unsupported URL: {self.url}" - url = self.url.replace("github.com", "raw.githubusercontent.com") - license_url = f"{url}/{self.commit}/LICENSE" - try: - return read_url(license_url) - except urllib.error.HTTPError: # type: ignore - return None + if self.repo_type == RepoType.GITHUB: + assert "github.com" in self.url, f"Unsupported URL: {self.url}" + url = self.url.replace("github.com", "raw.githubusercontent.com") + license_url = f"{url}/{self.commit}/LICENSE" + try: + return read_url(license_url) + except urllib.error.HTTPError: # type: ignore + return None + else: + license_path = Path(self.repo.working_dir) / "LICENSE" + if license_path.exists(): + return license_path.open("r").read() + else: + return None def _get_config_url(self, filename: str) -> str: + assert self.repo_type == RepoType.GITHUB assert "github.com" in self.url, f"Unsupported URL: {self.url}" url = self.url.replace("github.com", "raw.githubusercontent.com") return f"{url}/{self.commit}/{filename}" @@ -767,13 +775,21 @@ def get_config(self, filename: str, num_retries: int = 2) -> Dict[str, Any]: def uses_lakefile_lean(self) -> bool: """Check if the repo uses a ``lakefile.lean``.""" - url = self._get_config_url("lakefile.lean") - return url_exists(url) + if self.repo_type == RepoType.GITHUB: + url = self._get_config_url("lakefile.lean") + return url_exists(url) + else: + lakefile_path = Path(self.repo.working_dir) / "lakefile.lean" + return lakefile_path.exists() def uses_lakefile_toml(self) -> bool: """Check if the repo uses a ``lakefile.toml``.""" - url = self._get_config_url("lakefile.toml") - return url_exists(url) + if self.repo_type == RepoType.GITHUB: + url = self._get_config_url("lakefile.toml") + return url_exists(url) + else: + lakefile_path = Path(self.repo.working_dir) / "lakefile.toml" + return lakefile_path.exists() @dataclass(frozen=True)