From 44742d97544e902b66db77fb1516f40a5a966560 Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Mon, 5 Aug 2024 12:51:36 +0000 Subject: [PATCH] add @cache --- src/lean_dojo/data_extraction/lean.py | 1 + tests/interaction/test_tactics.py | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/lean_dojo/data_extraction/lean.py b/src/lean_dojo/data_extraction/lean.py index 010469a..35bb9d2 100644 --- 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 index c0a2ee8..66a347a 100644 --- 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