add @cache

lean-dojo · Aug 5, 2024 · 44742d9 · 44742d9
1 parent 819ed53
commit 44742d9
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/src/lean_dojo/data_extraction/lean.py b/src/lean_dojo/data_extraction/lean.py
@@ -181,6 +181,7 @@ def cleanse_string(s: Union[str, Path]) -> str:
     return str(s).replace("/", "_").replace(":", "_")
 
 
+@cache
 def _to_commit_hash(repo: Union[Repository, Repo], label: str) -> str:
     """Convert a tag or branch to a commit hash."""
     if isinstance(repo, Repository):  # GitHub repository

diff --git a/tests/interaction/test_tactics.py b/tests/interaction/test_tactics.py
@@ -37,10 +37,10 @@ def test_example_append_subset(batteries_repo: LeanGitRepo) -> None:
     thm = Theorem(
         batteries_repo,
         "Batteries/Data/List/Lemmas.lean",
-        "List.append_subset",
+        "List.disjoint_append_left",
     )
     with Dojo(thm) as (dojo, s0):
-        s1 = dojo.run_tac(s0, "simp [subset_def, or_imp, forall_and]")
+        s1 = dojo.run_tac(s0, "simp [Disjoint, or_imp, forall_and]")
         assert isinstance(s1, ProofFinished)
         assert dojo.is_successful