Bugfixes

src/lean_dojo/data_extraction/lean.py

@@ -709,8 +709,10 @@ def _parse_deps(
                 url = url[:-4]
             if url.startswith("git@"):
                 url = "https://" + url[4:].replace(":", "/")
-
-            rev = m["rev"]  # type: ignore
+            try:
+                rev = m["rev"]  # type: ignore
+            except KeyError:
+                rev = None
             if rev is None:
                 commit = get_latest_commit(url)
             elif len(rev) == 40 and _COMMIT_REGEX.fullmatch(rev):
@@ -730,25 +732,29 @@ def _parse_lakefile_toml_dependencies(
         self, path: Union[str, Path, None]
     ) -> List[Tuple[str, "LeanGitRepo"]]:
         lakefile = (
-            self.get_config("lakefile.toml")["content"]
+            self.get_config("lakefile.toml")
             if path is None
             else (Path(path) / "lakefile.toml").open().read()
         )
-        matches = dict()
-
-        for req in _LAKEFILE_TOML_REQUIREMENT_REGEX.finditer(lakefile):
-            for line in req.group().strip().splitlines():
-                key, value = line.split("=")
-                key = key.strip()
-                value = value.strip()
-                if key == "path":
-                    raise ValueError("Local dependencies are not supported.")
-                if key == "git":
-                    matches["url"] = value
-                if key == "rev":
-                    matches["rev"] = value
-                if key == "name":
-                    matches["name"] = value
+        # Parsing worked
+        if isinstance(lakefile, dict) and "require" in lakefile:
+            matches = lakefile["require"]
+        else:
+            if "content" in lakefile:
+                lakefile = lakefile["content"]
+            matches = []
+            for req in _LAKEFILE_TOML_REQUIREMENT_REGEX.finditer(lakefile):
+                match = {}
+                for line in req.group().strip().splitlines():
+                    key, value = line.split("=")
+                    match[key.strip()] = value.strip()
+                matches.append(match)
+        for match in matches:
+            if "path" in match:
+                raise ValueError("Local dependencies are not supported.")
+            if "git" in match:
+                match["url"] = match["git"]
+                del match["git"]
 
         return self._parse_deps(matches)
 

src/lean_dojo/interaction/dojo.py

@@ -284,7 +284,6 @@ def __enter__(self) -> Tuple["Dojo", State]:
 
         assert res["error"] is None
 
-        # logger.debug(f"Response: {res}")
         if self.uses_tactics:
             assert res["tacticState"] != "no goals"
             init_state: State = TacticState(
@@ -472,6 +471,7 @@ def _submit_request(self, req: str) -> Dict[str, Any]:
             raise DojoCrashError(f"Invalid JSON: {res}")
 
         result["message"] = msg
+        logger.debug(result)
         return result
 
     def _check_alive(self) -> None:

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: