diff --git a/src/lean_dojo/data_extraction/lean.py b/src/lean_dojo/data_extraction/lean.py index a6d3a632..c249c13a 100644 --- a/src/lean_dojo/data_extraction/lean.py +++ b/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) diff --git a/src/lean_dojo/interaction/dojo.py b/src/lean_dojo/interaction/dojo.py index ba8bb15f..378efb0e 100644 --- a/src/lean_dojo/interaction/dojo.py +++ b/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: diff --git a/tests/conftest.py b/tests/conftest.py index 26fbb1d3..bf645813 100644 --- a/tests/conftest.py +++ b/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 diff --git a/tests/data_extraction/test_cache.py b/tests/data_extraction/test_cache.py index e80d0f8d..8c4c43bc 100644 --- a/tests/data_extraction/test_cache.py +++ b/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 diff --git a/tests/data_extraction/test_trace.py b/tests/data_extraction/test_trace.py index 0c9710a8..10d45a55 100644 --- a/tests/data_extraction/test_trace.py +++ b/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: diff --git a/tests/interaction/test_interaction.py b/tests/interaction/test_interaction.py index 83b1c454..40e486aa 100644 --- a/tests/interaction/test_interaction.py +++ b/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: