bugfix

Author: yangky11

docs/source/conf.py

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

pyproject.toml

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

src/lean_dojo/constants.py

@@ -14,7 +14,7 @@
 
 load_dotenv()
 
-__version__ = "2.1.3"
+__version__ = "2.2.0"
 
 logger.remove()
 if "VERBOSE" in os.environ or "DEBUG" in os.environ:
@@ -44,7 +44,7 @@
 MAX_NUM_PROCS = 32
 
 NUM_PROCS = int(os.getenv("NUM_PROCS", min(multiprocessing.cpu_count(), MAX_NUM_PROCS)))
-"""Number of threads to use
+"""Number of processes to use
 """
 
 NUM_WORKERS = NUM_PROCS - 1

src/lean_dojo/data_extraction/lean.py

@@ -353,6 +353,8 @@ def convert_pos(self, byte_idx: int) -> Pos:
         n = 0
         for i, num_bytes in enumerate(self.num_bytes, start=1):
             n += num_bytes
+            if n == byte_idx and i == self.num_lines:
+                byte_idx -= 1
             if n > byte_idx:
                 line_byte_idx = byte_idx - (n - num_bytes)
                 if line_byte_idx == 0: