bugfix

Author: yangky11

docs/source/conf.py

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

docs/source/developer-guide.rst

@@ -21,8 +21,8 @@ We use `pytest <https://docs.pytest.org/>`_ for testing. You can run tests by:
 
 .. code-block:: bash
 
-   VERBOSE=1 CACHE_DIR=~/.cache/lean_dojo_testing DISABLE_REMOTE_CACHE=1 pytest -s tests
    rm -rf ~/.cache/lean_dojo_testing 
+   VERBOSE=1 CACHE_DIR=~/.cache/lean_dojo_testing DISABLE_REMOTE_CACHE=1 pytest -s tests
 
 The environment variable :code:`CACHE_DIR` makes sure the testing uses a temporary cache directory that 
 does not interfere with the deployed code. The temporary cache directory is deleted after the testing completes. 

pyproject.toml

@@ -12,7 +12,7 @@ exclude = [
 
 [project]
 name = "lean-dojo"
-version = "2.1.2"
+version = "2.1.3"
 authors = [
   { name="Kaiyu Yang", email="kaiyuy@meta.com" },
 ]

src/lean_dojo/constants.py

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

src/lean_dojo/data_extraction/lean.py

@@ -50,6 +50,9 @@
 LEAN4_REPO = None
 """The GitHub Repo for Lean 4 itself."""
 
+LEAN4_NIGHTLY_REPO = None
+"""The GitHub Repo for Lean 4 nightly releases."""
+
 _URL_REGEX = re.compile(r"(?P<url>.*?)/*")
 
 _SSH_TO_HTTPS_REGEX = re.compile(r"^git@github\.com:(.+)/(.+)(?:\.git)?$")
@@ -327,17 +330,19 @@ def start_pos(self) -> Pos:
     def end_pos(self) -> Pos:
         """Return the end position of a source file.
 
-        Args:
-            zero_indexed (bool, optional): Whether to use 0-index instead of 1-index. Defaults to False.
-
         Returns:
             Pos: A :class:`Pos` object representing the end of this file.
         """
         # Line and column numbers are 1-indexed by default.
+        if self.is_empty():
+            return self.start_pos
         line_nb = self.num_lines
         column_nb = 1 + len(self.code[-1])
         return Pos(line_nb, column_nb)
 
+    def is_empty(self) -> bool:
+        return len(self.code) == 0
+
     def convert_pos(self, byte_idx: int) -> Pos:
         """Convert a byte index (:code:`String.Pos` in Lean 4) to a :class:`Pos` object."""
         n = 0
@@ -442,7 +447,13 @@ def get_lean4_commit_from_config(config_dict: Dict[str, Any]) -> str:
     prefix = "leanprover/lean4:"
     assert config.startswith(prefix), f"Invalid Lean 4 version: {config}"
     version = config[len(prefix) :]
-    return _to_commit_hash(LEAN4_REPO, version)
+    if version.startswith("nightly-"):
+        global LEAN4_NIGHTLY_REPO
+        if LEAN4_NIGHTLY_REPO is None:
+            LEAN4_NIGHTLY_REPO = GITHUB.get_repo("leanprover/lean4-nightly")
+        return _to_commit_hash(LEAN4_NIGHTLY_REPO, version)
+    else:
+        return _to_commit_hash(LEAN4_REPO, version)
 
 
 URL = str

src/lean_dojo/data_extraction/traced_data.py

@@ -839,7 +839,7 @@ def _callback(node: ModuleImportNode, _) -> None:
     def get_premise_definitions(self) -> List[Dict[str, Any]]:
         """Return all theorems and definitions defined in the current file that
         can be potentially used as premises, including the premises in the theorem
-        statement and premises in the tactics used to prove the theorem. 
+        statement and premises in the tactics used to prove the theorem.
 
         Returns:
             List[Dict[str, Any]]: _description_