diff --git a/coqpyt/coq/base_file.py b/coqpyt/coq/base_file.py index ecf8e9d..ddde2a9 100644 --- a/coqpyt/coq/base_file.py +++ b/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() diff --git a/coqpyt/coq/lsp/client.py b/coqpyt/coq/lsp/client.py index b8ae3da..887e2ef 100644 --- a/coqpyt/coq/lsp/client.py +++ b/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, diff --git a/coqpyt/coq/proof_file.py b/coqpyt/coq/proof_file.py index 899d904..80b9be3 100644 --- a/coqpyt/coq/proof_file.py +++ b/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,11 +354,25 @@ 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 @@ -345,6 +380,7 @@ def __init__( _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, )