Skip to content

Commit

Permalink
Merge pull request #128 from albertqjiang/main
Browse files Browse the repository at this point in the history
Remove a bug where the path gets inappropriately used for string removal
  • Loading branch information
Kaiyu Yang authored Jan 18, 2024
2 parents b844a1c + 41f0d59 commit bab35fa
Showing 1 changed file with 8 additions and 3 deletions.
11 changes: 8 additions & 3 deletions src/lean_dojo/data_extraction/lean.py
Original file line number Diff line number Diff line change
Expand Up @@ -37,9 +37,9 @@
)


def cleanse_string(s: str) -> str:
def cleanse_string(s: str | Path) -> str:
"""Replace : and / with _ in a string."""
return s.replace("/", "_").replace(":", "_")
return str(s).replace("/", "_").replace(":", "_")


@cache
Expand Down Expand Up @@ -681,4 +681,9 @@ def __post_init__(self) -> None:
@property
def uid(self) -> str:
"""Unique identifier of the theorem."""
return f"{cleanse_string(self.repo.url)}@{cleanse_string(self.repo.commit)}:{cleanse_string(self.file_path)}:{cleanse_string(self.full_name)}"
return f"{cleanse_string(self.repo.url)}@{cleanse_string(self.repo.commit)}:{cleanse_string(self.file_path.__str__())}:{cleanse_string(self.full_name)}"

@property
def uhash(self) -> str:
"""Unique hash of the theorem."""
return str(hash(self.uid) ** 2)

0 comments on commit bab35fa

Please sign in to comment.