added physical-to-logical path mapping command-line option (#57)

---------

Co-authored-by: Ali Ghanbari <[email protected]>

Author: ali-ghanbari

coqpyt/coq/base_file.py

@@ -3,7 +3,7 @@
 import uuid
 import tempfile
 from copy import deepcopy
-from typing import Optional, List
+from typing import Optional, List, Tuple
 
 from coqpyt.lsp.structs import (
     TextDocumentItem,
@@ -43,6 +43,7 @@ def __init__(
         timeout: int = 30,
         workspace: Optional[str] = None,
         coq_lsp: str = "coq-lsp",
+        coq_lsp_options: Tuple[str] = None,
         coqtop: str = "coqtop",
     ):
         """Creates a CoqFile.
@@ -67,7 +68,9 @@ def __init__(
             uri = f"file://{workspace}"
         else:
             uri = f"file://{self._path}"
-        self.coq_lsp_client = CoqLspClient(uri, timeout=timeout, coq_lsp=coq_lsp)
+        self.coq_lsp_client = CoqLspClient(
+            uri, timeout=timeout, coq_lsp_options=coq_lsp_options, coq_lsp=coq_lsp
+        )
         uri = f"file://{self._path}"
         text = self.__read()
 

coqpyt/coq/lsp/client.py

@@ -31,7 +31,7 @@ def __init__(
         timeout: int = 30,
         memory_limit: int = 2097152,
         coq_lsp: str = "coq-lsp",
-        coq_lsp_options: str = "-D 0",
+        coq_lsp_options: Tuple[str] = None,
         init_options: Dict = __DEFAULT_INIT_OPTIONS,
     ):
         """Creates a CoqLspClient
@@ -63,9 +63,21 @@ def __init__(
         self.file_progress: Dict[str, List[CoqFileProgressParams]] = {}
 
         if sys.platform.startswith("linux"):
-            command = f"ulimit -v {memory_limit}; {coq_lsp} {coq_lsp_options}"
+            command = f"ulimit -v {memory_limit}; {coq_lsp}"
         else:
-            command = f"{coq_lsp} {coq_lsp_options}"
+            command = f"{coq_lsp}"
+
+        if coq_lsp_options is None:
+            command += " -D 0"
+        else:
+            hasDOption = False
+            for option in coq_lsp_options:
+                if option.startswith("-D"):
+                    hasDOption = True
+                    break
+            if not hasDOption:
+                command += " -D 0"
+            command += " " + " ".join(coq_lsp_options)
 
         proc = subprocess.Popen(
             command,

coqpyt/coq/proof_file.py

@@ -31,6 +31,7 @@ class _AuxFile(object):
     def __init__(
         self,
         file_path,
+        coq_lsp_options: Tuple[str],
         copy: bool = False,
         workspace: Optional[str] = None,
         timeout: int = 30,
@@ -41,7 +42,9 @@ def __init__(
             uri = f"file://{workspace}"
         else:
             uri = f"file://{self.path}"
-        self.coq_lsp_client = CoqLspClient(uri, timeout=timeout)
+        self.coq_lsp_client = CoqLspClient(
+            uri, coq_lsp_options=coq_lsp_options, timeout=timeout
+        )
 
     def __enter__(self):
         return self
@@ -167,11 +170,16 @@ def __load_library(
         library_file: str,
         library_hash: str,
         timeout: int,
+        coq_lsp_options: Tuple[str] = None,
         workspace: Optional[str] = None,
     ):
         # NOTE: the library_hash attribute is only used for the LRU cache
         coq_file = CoqFile(
-            library_file, workspace=workspace, library=library_name, timeout=timeout
+            library_file,
+            workspace=workspace,
+            coq_lsp_options=coq_lsp_options,
+            library=library_name,
+            timeout=timeout,
         )
         coq_file.run()
         context = coq_file.context
@@ -221,6 +229,7 @@ def get_library(
         library_name: str,
         library_file: str,
         timeout: int,
+        coq_lsp_options: Tuple[str],
         workspace: Optional[str] = None,
         use_disk_cache: bool = False,
     ) -> Dict[str, Term]:
@@ -232,7 +241,12 @@ def get_library(
             if cached_library is not None:
                 return cached_library
         aux_context = _AuxFile.__load_library(
-            library_name, library_file, library_hash, timeout, workspace=workspace
+            library_name,
+            library_file,
+            library_hash,
+            timeout,
+            coq_lsp_options,
+            workspace=workspace,
         )
         # FIXME: we ignore the usage of "Local" from imported files to
         # simplify the implementation. However, they can be used:
@@ -260,13 +274,18 @@ def get_libraries(aux_file: "_AuxFile") -> List[str]:
 
     @staticmethod
     def get_coq_context(
-        timeout: int, workspace: Optional[str] = None, use_disk_cache: bool = False
+        timeout: int,
+        workspace: Optional[str] = None,
+        use_disk_cache: bool = False,
+        coq_lsp_options: Tuple[str] = None,
     ) -> FileContext:
         temp_path = os.path.join(
             tempfile.gettempdir(), "aux_" + str(uuid.uuid4()).replace("-", "") + ".v"
         )
 
-        with _AuxFile(file_path=temp_path, timeout=timeout) as aux_file:
+        with _AuxFile(
+            file_path=temp_path, coq_lsp_options=coq_lsp_options, timeout=timeout
+        ) as aux_file:
             aux_file.didOpen()
             libraries = _AuxFile.get_libraries(aux_file)
             for library in libraries:
@@ -284,6 +303,7 @@ def get_coq_context(
                     timeout,
                     workspace=workspace,
                     use_disk_cache=use_disk_cache,
+                    coq_lsp_options=coq_lsp_options,
                 )
                 context.add_library(library, terms)
 
@@ -304,6 +324,7 @@ def __init__(
         timeout: int = 30,
         workspace: Optional[str] = None,
         coq_lsp: str = "coq-lsp",
+        coq_lsp_options: Tuple[str] = None,
         coqtop: str = "coqtop",
         error_mode: str = "strict",
         use_disk_cache: bool = False,
@@ -333,18 +354,33 @@ def __init__(
         """
         if not os.path.isabs(file_path):
             file_path = os.path.abspath(file_path)
-        super().__init__(file_path, library, timeout, workspace, coq_lsp, coqtop)
-        self.__aux_file = _AuxFile(file_path, timeout=self.timeout, workspace=workspace)
+        super().__init__(
+            file_path,
+            library=library,
+            timeout=timeout,
+            workspace=workspace,
+            coq_lsp=coq_lsp,
+            coqtop=coqtop,
+            coq_lsp_options=coq_lsp_options,
+        )
+        self.__aux_file = _AuxFile(
+            file_path,
+            timeout=self.timeout,
+            coq_lsp_options=coq_lsp_options,
+            workspace=workspace,
+        )
         self.__error_mode = error_mode
         self.__use_disk_cache = use_disk_cache
         self.__aux_file.didOpen()
+        self.__coq_lsp_options = coq_lsp_options
 
         try:
             # We need to update the context already defined in the CoqFile
             self.context.update(
                 _AuxFile.get_coq_context(
                     self.timeout,
                     workspace=self.workspace,
+                    coq_lsp_options=coq_lsp_options,
                     use_disk_cache=self.__use_disk_cache,
                 )
             )
@@ -612,6 +648,7 @@ def __update_libraries(self):
                 library,
                 library_file,
                 self.timeout,
+                self.__coq_lsp_options,
                 workspace=self.workspace,
                 use_disk_cache=self.__use_disk_cache,
             )