Support lakefile.toml and bump to v1.9.0

docs/source/conf.py

@@ -13,7 +13,7 @@
 project = "LeanDojo"
 copyright = "2023, LeanDojo Team"
 author = "Kaiyu Yang"
-release = "1.8.3"
+release = "1.9.0"
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

pyproject.toml

@@ -13,7 +13,7 @@ exclude = [
 
 [project]
 name = "lean-dojo"
-version = "1.8.3"
+version = "1.9.0"
 authors = [
   { name="Kaiyu Yang", email="kaiyuy@caltech.edu" },
 ]

src/lean_dojo/constants.py

@@ -14,7 +14,7 @@
 
 load_dotenv()
 
-__version__ = "1.8.3"
+__version__ = "1.9.0"
 
 logger.remove()
 if "VERBOSE" in os.environ or "DEBUG" in os.environ:

src/lean_dojo/data_extraction/lean.py

@@ -15,7 +15,7 @@
 from github import Github, Auth
 from dataclasses import dataclass, field
 from github.Repository import Repository
-from typing import List, Dict, Any, Generator, Union, Optional, Tuple
+from typing import List, Dict, Any, Generator, Union, Optional, Tuple, Iterator
 
 from ..utils import (
     execute,
@@ -360,10 +360,14 @@ class RepoInfoCache:
 info_cache = RepoInfoCache()
 
 
-_GIT_REQUIREMENT_REGEX = re.compile(
+_LAKEFILE_LEAN_GIT_REQUIREMENT_REGEX = re.compile(
     r"require\s+(?P<name>\S+)\s+from\s+git\s+\"(?P<url>.+?)\"(\s+@\s+\"(?P<rev>\S+)\")?"
 )
 
+_LAKEFILE_LEAN_LOCAL_REQUIREMENT_REGEX = re.compile(r"require \S+ from \"")
+
+_LAKEFILE_TOML_REQUIREMENT_REGEX = re.compile(r"(?<=\[\[require\]\]).+(?=\n\n)")
+
 
 def is_supported_version(v) -> bool:
     """Check if ``v`` is at least `v4.3.0-rc2`."""
@@ -511,12 +515,7 @@ def get_dependencies(
             for pkg in lake_manifest["packages"]:
                 deps[pkg["name"]] = LeanGitRepo(pkg["url"], pkg["rev"])
         except Exception:
-            lakefile = (
-                self.get_config("lakefile.lean")
-                if path is None
-                else {"content": (Path(path) / "lakefile.lean").open().read()}
-            )
-            for name, repo in self._parse_lakefile_dependencies(lakefile["content"]):
+            for name, repo in self._parse_lakefile_dependencies(path):
                 if name not in deps:
                     deps[name] = repo
                 for dd_name, dd_repo in repo.get_dependencies().items():
@@ -525,15 +524,33 @@ def get_dependencies(
         return deps
 
     def _parse_lakefile_dependencies(
-        self, lakefile: str
+        self, path: Union[str, Path, None]
     ) -> List[Tuple[str, "LeanGitRepo"]]:
-        _LOCAL_REQUIREMENT_REGEX = r"require \S+ from \""
-        if re.search(_LOCAL_REQUIREMENT_REGEX, lakefile):
+        if self.uses_lakefile_lean():
+            return self._parse_lakefile_lean_dependencies(path)
+        else:
+            return self._parse_lakefile_toml_dependencies(path)
+
+    def _parse_lakefile_lean_dependencies(
+        self, path: Union[str, Path, None]
+    ) -> List[Tuple[str, "LeanGitRepo"]]:
+        lakefile = (
+            self.get_config("lakefile.lean")["content"]
+            if path is None
+            else (Path(path) / "lakefile.lean").open().read()
+        )
+
+        if _LAKEFILE_LEAN_LOCAL_REQUIREMENT_REGEX.search(lakefile):
             raise ValueError("Local dependencies are not supported.")
 
+        return self._parse_deps(_LAKEFILE_LEAN_GIT_REQUIREMENT_REGEX.finditer(lakefile))
+
+    def _parse_deps(
+        self, matches: Union[Iterator[re.Match[str]], Dict[str, str]]
+    ) -> List[Tuple[str, "LeanGitRepo"]]:
         deps = []
 
-        for m in _GIT_REQUIREMENT_REGEX.finditer(lakefile):
+        for m in matches:
             url = m["url"]
             if url.endswith(".git"):
                 url = url[:-4]
@@ -556,6 +573,32 @@ def _parse_lakefile_dependencies(
 
         return deps
 
+    def _parse_lakefile_toml_dependencies(
+        self, path: Union[str, Path, None]
+    ) -> List[Tuple[str, "LeanGitRepo"]]:
+        lakefile = (
+            self.get_config("lakefile.toml")["content"]
+            if path is None
+            else (Path(path) / "lakefile.toml").open().read()
+        )
+        matches = dict()
+
+        for requirement in _LAKEFILE_TOML_REQUIREMENT_REGEX.finditer(lakefile):
+            for line in requirement.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
+
+        return self._parse_deps(lakefile, matches)
+
     def get_license(self) -> Optional[str]:
         """Return the content of the ``LICENSE`` file."""
         assert "github.com" in self.url, f"Unsupported URL: {self.url}"
@@ -582,6 +625,16 @@ def get_config(self, filename: str, num_retries: int = 2) -> Dict[str, Any]:
         else:
             return {"content": content}
 
+    def uses_lakefile_lean(self) -> bool:
+        """Check if the repo uses a ``lakefile.lean``."""
+        url = self._get_config_url("lakefile.lean")
+        return url_exists(url)
+
+    def uses_lakefile_toml(self) -> bool:
+        """Check if the repo uses a ``lakefile.toml``."""
+        url = self._get_config_url("lakefile.toml")
+        return url_exists(url)
+
 
 @dataclass(frozen=True)
 class Theorem:

src/lean_dojo/interaction/Lean4Repl.lean

@@ -1,4 +1,5 @@
 -- REPL for interacting with Lean 4 via the command line.
+import Lean.Message
 import Lean.Elab.Tactic
 import Lean.Elab.Frontend
 
@@ -228,7 +229,7 @@ private def handleRunTac (req : Request) : TacticReplM Response := do
         let s ← getThe Core.State
         if s.messages.hasErrors then
           let messages := s.messages.toList.filter fun m => m.severity == MessageSeverity.error
-          return { error := join $ ← (messages.map Message.data).mapM fun md => md.toString }
+          return { error := join $ ← (messages.map (·.data)).mapM fun md => md.toString }
       catch ex =>
         return {error := ← ex.toMessageData.toString}
 

src/lean_dojo/interaction/dojo.py

@@ -374,8 +374,15 @@ def _modify_file(self, traced_file: TracedFile) -> None:
 
         repl_file = "Lean4Repl.lean"
         repl_dst = Path(repl_file)
-        with open("lakefile.lean", "a") as oup:
-            oup.write("\nlean_lib Lean4Repl {\n\n}\n")
+
+        if os.path.exists("lakefile.lean"):
+            with open("lakefile.lean", "a") as oup:
+                oup.write("\nlean_lib Lean4Repl {\n\n}\n")
+        else:
+            assert os.path.exists("lakefile.toml")
+            with open("lakefile.toml", "a") as oup:
+                oup.write('\n[[lean_lib]]\nname = "Lean4Repl"\n')
+
         if os.path.exists("lakefile.olean"):
             os.remove("lakefile.olean")
         if os.path.exists(".lake/lakefile.olean"):

tests/interaction/test_tactics.py

@@ -279,20 +279,6 @@ def test_example_mem_eqLocus(mathlib4_repo: LeanGitRepo) -> None:
         assert dojo.is_successful
 
 
-def test_example_neg_lt_sub_right_of_lt_add(batteries_repo: LeanGitRepo) -> None:
-    thm = Theorem(
-        batteries_repo,
-        "Batteries/Data/Int/Order.lean",
-        "Int.neg_lt_sub_right_of_lt_add",
-    )
-    with Dojo(thm) as (dojo, s0):
-        s1 = dojo.run_tac(
-            s0, "exact Int.lt_sub_left_of_add_lt (Int.sub_right_lt_of_lt_add h)"
-        )
-        assert isinstance(s1, ProofFinished)
-        assert dojo.is_successful
-
-
 def test_example_eq(mathlib4_repo: LeanGitRepo) -> None:
     thm = Theorem(
         mathlib4_repo,