fix trace_repo errors

Author: yangky11

tests/conftest.py

@@ -9,7 +9,6 @@
 MATHLIB4_URL = "https://github.com/leanprover-community/mathlib4"
 LEAN4_EXAMPLE_URL = "https://github.com/yangky11/lean4-example"
 EXAMPLE_COMMIT_HASH = "e2602e8d4b1d9cf9240f1a20160a47cfc35165b8"
-REMOTE_EXAMPLE_URL = "https://gitee.com/rexzong/lean4-example"
 URLS = [
     MINIF2F_URL,
     BATTERIES_URL,
@@ -19,11 +18,6 @@
 ]
 
 
-@pytest.fixture(scope="session")
-def remote_example_url():
-    return REMOTE_EXAMPLE_URL
-
-
 @pytest.fixture(scope="session")
 def example_commit_hash():
     return EXAMPLE_COMMIT_HASH
@@ -48,26 +42,22 @@ def lean4_example_repo():
 
 @pytest.fixture(scope="session")
 def batteries_repo():
-    commit = get_latest_commit(BATTERIES_URL)
-    return LeanGitRepo(BATTERIES_URL, commit)
+    return LeanGitRepo(BATTERIES_URL, "stable")
 
 
 @pytest.fixture(scope="session")
 def mathlib4_repo():
-    commit = get_latest_commit(MATHLIB4_URL)
-    return LeanGitRepo(MATHLIB4_URL, commit)
+    return LeanGitRepo(MATHLIB4_URL, "stable")
 
 
 @pytest.fixture(scope="session")
 def aesop_repo():
-    commit = get_latest_commit(AESOP_URL)
-    return LeanGitRepo(AESOP_URL, commit)
+    return LeanGitRepo(AESOP_URL, "stable")
 
 
 @pytest.fixture(scope="session", params=URLS)
 def traced_repo(request):
     url = request.param
-    commit = get_latest_commit(url)
-    repo = LeanGitRepo(url, commit)
+    repo = LeanGitRepo(url, "stable")
     traced_repo = trace(repo)
     yield traced_repo

tests/data_extraction/test_cache.py

@@ -21,20 +21,3 @@ def test_local_repo_cache(lean4_example_url, example_commit_hash):
     # get the cache
     repo_cache_dir = cache.get(rel_cache_dir)
     assert repo_cache_dir is not None
-
-
-def test_remote_repo_cache(remote_example_url):
-    prefix = "repos"
-    repo_name = "lean4-example"
-    with working_directory() as tmp_dir:
-        repo = Repo.clone_from(remote_example_url, repo_name)
-        tmp_remote_dir = tmp_dir / repo_name
-        rel_cache_dir = (
-            prefix
-            / Path(f"gitpython-{repo_name}-{repo.head.commit.hexsha}")
-            / repo_name
-        )
-        cache.store(tmp_remote_dir, rel_cache_dir)
-    # get the cache
-    repo_cache = cache.get(rel_cache_dir)
-    assert repo_cache is not None

tests/data_extraction/test_trace.py

@@ -15,15 +15,6 @@ def test_github_trace(lean4_example_url):
     assert path is not None
 
 
-def test_remote_trace(remote_example_url):
-    # remote
-    remote_repo = LeanGitRepo(remote_example_url, "main")
-    assert remote_repo.repo_type == RepoType.REMOTE
-    trace_repo = trace(remote_repo)
-    path = cache.get(remote_repo.get_cache_dirname() / remote_repo.name)
-    assert path is not None
-
-
 def test_local_trace(lean4_example_url):
     # local
     with working_directory() as tmp_dir:

tests/interaction/test_interaction.py

@@ -26,23 +26,6 @@ def test_github_interact(lean4_example_url):
     assert isinstance(final_state, ProofFinished)
 
 
-def test_remote_interact(remote_example_url):
-    repo = LeanGitRepo(url=remote_example_url, commit="main")
-    assert repo.repo_type == RepoType.REMOTE
-    theorem = Theorem(repo, "Lean4Example.lean", "hello_world")
-    # initial state
-    dojo, state_0 = Dojo(theorem).__enter__()
-    assert state_0.pp == "a b c : Nat\n⊢ a + b + c = a + c + b"
-    # state after running a tactic
-    state_1 = dojo.run_tac(state_0, "rw [add_assoc]")
-    assert state_1.pp == "a b c : Nat\n⊢ a + (b + c) = a + c + b"
-    # state after running another a sorry tactic
-    assert dojo.run_tac(state_1, "sorry") == ProofGivenUp()
-    # finish proof
-    final_state = dojo.run_tac(state_1, "rw [add_comm b, ←add_assoc]")
-    assert isinstance(final_state, ProofFinished)
-
-
 def test_local_interact(lean4_example_url):
     # Clone the GitHub repository to the local path
     with working_directory() as tmp_dir: