Merge branch 'main' into dev

README.md

@@ -15,12 +15,12 @@ ______________________________________________________________________
 
 ## Requirements
 
-* Supported platforms: Linux, Windows (WSL), and macOS (:warning: experimental for Apple silicon)
+* Supported platforms: Linux, Windows WSL, and macOS
 * Git >= 2.25
 * 3.9 <= Python < 3.11
 * wget
 * [elan](https://github.com/leanprover/elan)
-* Docker strongly recommended when using LeanDojo with Lean 3
+* Docker is strongly recommended when using LeanDojo with Lean 3
 * Recommended: Generate a [GitHub personal access token](https://docs.github.com/en/authentication/keeping-your-account-and-data-secure/managing-your-personal-access-tokens#personal-access-tokens-classic) and set the environment variable `GITHUB_ACCESS_TOKEN` to it
 
 

docs/source/getting-started.rst

@@ -15,7 +15,7 @@ Requirements
 * 3.9 <= Python < 3.11
 * wget
 * `elan <https://github.com/leanprover/elan>`_
-* `Docker <https://www.docker.com/>`_ strongly recommended when using LeanDojo with Lean 3. See :ref:`running-within-docker` if it is not an option for you
+* `Docker <https://www.docker.com/>`_ is strongly recommended when using LeanDojo with Lean 3. See :ref:`running-within-docker` if it is not an option for you
 * Recommended: Generate a `GitHub personal access token <https://docs.github.com/en/authentication/keeping-your-account-and-data-secure/managing-your-personal-access-tokens#personal-access-tokens-classic>`_ and set the environment variable :code:`GITHUB_ACCESS_TOKEN` to it
 
 Installation

src/lean_dojo/data_extraction/build_lean4_repo.py

@@ -134,7 +134,9 @@ def is_new_version(v) -> bool:
     assert major == 4 and minor == 3 and patch == 0
     if "4.3.0-rc" in v:
         rc = int(v.split("-")[1][2:])
-    return rc >= 2
+        return rc >= 2
+    else:
+        return True
 
 
 def main() -> None:

src/lean_dojo/data_extraction/traced_data.py

@@ -1371,7 +1371,7 @@ def check_sanity(self) -> None:
                 ), to_xml_path(self.root_dir, path, self.repo)
 
     @classmethod
-    def from_traced_files(cls, root_dir: Union[str, Path]) -> None:
+    def from_traced_files(cls, root_dir: Union[str, Path]) -> "TracedRepo":
         """Construct a :class:`TracedRepo` object by parsing :file:`*.ast.json` and :file:`*.path` files
            produced by :code:`lean --ast --tsast --tspp` (Lean 3) or :file:`ExtractData.lean` (Lean 4).