From d11f6b341d262f3f81ad795b9abe244bd9340584 Mon Sep 17 00:00:00 2001 From: Ali Ghanbari Date: Mon, 28 Apr 2025 00:20:35 -0500 Subject: [PATCH 1/2] added physical-to-logical path mapping command-line option --- coqpyt/coq/base_file.py | 5 ++-- coqpyt/coq/lsp/client.py | 18 ++++++++++--- coqpyt/coq/proof_file.py | 57 +++++++++++++++++++++++++--------------- 3 files changed, 54 insertions(+), 26 deletions(-) diff --git a/coqpyt/coq/base_file.py b/coqpyt/coq/base_file.py index ecf8e9d..aff3a25 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,7 @@ 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..7f8fc61 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..3842b8d 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,7 @@ 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 +168,12 @@ 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 +223,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]: @@ -231,9 +234,12 @@ def get_library( cached_library = cls.get_from_disk_cache(library_hash) if cached_library is not None: return cached_library - aux_context = _AuxFile.__load_library( - library_name, library_file, library_hash, timeout, workspace=workspace - ) + aux_context = _AuxFile.__load_library(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: # https://coq.inria.fr/refman/language/core/modules.html?highlight=local#coq:attr.local @@ -259,14 +265,16 @@ def get_libraries(aux_file: "_AuxFile") -> List[str]: return list(map(lambda line: line.strip(), libraries.split("\n")[1:-1])) @staticmethod - def get_coq_context( - timeout: int, workspace: Optional[str] = None, use_disk_cache: bool = False - ) -> FileContext: + def get_coq_context(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: @@ -275,16 +283,13 @@ def get_coq_context( context = FileContext(temp_path) for i, library in enumerate(libraries): - v_file = aux_file.get_diagnostics( - "Locate Library", library, i + 1 - ).split()[-1][:-1] - terms = _AuxFile.get_library( - library, - v_file, - timeout, - workspace=workspace, - use_disk_cache=use_disk_cache, - ) + v_file = aux_file.get_diagnostics("Locate Library", library, i + 1).split()[-1][:-1] + terms = _AuxFile.get_library(library, + v_file, + timeout, + workspace=workspace, + use_disk_cache=use_disk_cache, + coq_lsp_options=coq_lsp_options) context.add_library(library, terms) return context @@ -304,6 +309,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 +339,18 @@ 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 +358,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 +626,7 @@ def __update_libraries(self): library, library_file, self.timeout, + tuple(self.__coq_lsp_options), workspace=self.workspace, use_disk_cache=self.__use_disk_cache, ) From 128b6d14cef573d6ea61104e282326db4e89634f Mon Sep 17 00:00:00 2001 From: anonimized Date: Sun, 4 May 2025 08:37:23 +0000 Subject: [PATCH 2/2] fixed a bug by removing unecessary type cast, reformatted the code using Black --- coqpyt/coq/base_file.py | 4 +- coqpyt/coq/lsp/client.py | 2 +- coqpyt/coq/proof_file.py | 88 +++++++++++++++++++++++++--------------- 3 files changed, 59 insertions(+), 35 deletions(-) diff --git a/coqpyt/coq/base_file.py b/coqpyt/coq/base_file.py index aff3a25..ddde2a9 100644 --- a/coqpyt/coq/base_file.py +++ b/coqpyt/coq/base_file.py @@ -68,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_options=coq_lsp_options, 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 7f8fc61..887e2ef 100644 --- a/coqpyt/coq/lsp/client.py +++ b/coqpyt/coq/lsp/client.py @@ -72,7 +72,7 @@ def __init__( else: hasDOption = False for option in coq_lsp_options: - if option.startswith('-D'): + if option.startswith("-D"): hasDOption = True break if not hasDOption: diff --git a/coqpyt/coq/proof_file.py b/coqpyt/coq/proof_file.py index 3842b8d..80b9be3 100644 --- a/coqpyt/coq/proof_file.py +++ b/coqpyt/coq/proof_file.py @@ -42,7 +42,9 @@ def __init__( uri = f"file://{workspace}" else: uri = f"file://{self.path}" - self.coq_lsp_client = CoqLspClient(uri, coq_lsp_options=coq_lsp_options, timeout=timeout) + self.coq_lsp_client = CoqLspClient( + uri, coq_lsp_options=coq_lsp_options, timeout=timeout + ) def __enter__(self): return self @@ -168,12 +170,16 @@ def __load_library( library_file: str, library_hash: str, timeout: int, - coq_lsp_options: Tuple[str]=None, + 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, coq_lsp_options=coq_lsp_options, 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 @@ -223,7 +229,7 @@ def get_library( library_name: str, library_file: str, timeout: int, - coq_lsp_options : Tuple[str], + coq_lsp_options: Tuple[str], workspace: Optional[str] = None, use_disk_cache: bool = False, ) -> Dict[str, Term]: @@ -234,12 +240,14 @@ def get_library( cached_library = cls.get_from_disk_cache(library_hash) if cached_library is not None: return cached_library - aux_context = _AuxFile.__load_library(library_name, - library_file, - library_hash, - timeout, - coq_lsp_options, - workspace=workspace) + aux_context = _AuxFile.__load_library( + 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: # https://coq.inria.fr/refman/language/core/modules.html?highlight=local#coq:attr.local @@ -265,16 +273,19 @@ def get_libraries(aux_file: "_AuxFile") -> List[str]: return list(map(lambda line: line.strip(), libraries.split("\n")[1:-1])) @staticmethod - def get_coq_context(timeout: int, - workspace: Optional[str] = None, - use_disk_cache: bool = False, - coq_lsp_options: Tuple[str] = None - ) -> FileContext: + def get_coq_context( + 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, coq_lsp_options=coq_lsp_options, 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: @@ -283,13 +294,17 @@ def get_coq_context(timeout: int, context = FileContext(temp_path) for i, library in enumerate(libraries): - v_file = aux_file.get_diagnostics("Locate Library", library, i + 1).split()[-1][:-1] - terms = _AuxFile.get_library(library, - v_file, - timeout, - workspace=workspace, - use_disk_cache=use_disk_cache, - coq_lsp_options=coq_lsp_options) + v_file = aux_file.get_diagnostics( + "Locate Library", library, i + 1 + ).split()[-1][:-1] + terms = _AuxFile.get_library( + library, + v_file, + timeout, + workspace=workspace, + use_disk_cache=use_disk_cache, + coq_lsp_options=coq_lsp_options, + ) context.add_library(library, terms) return context @@ -309,7 +324,7 @@ def __init__( timeout: int = 30, workspace: Optional[str] = None, coq_lsp: str = "coq-lsp", - coq_lsp_options : Tuple[str] = None, + coq_lsp_options: Tuple[str] = None, coqtop: str = "coqtop", error_mode: str = "strict", use_disk_cache: bool = False, @@ -339,14 +354,21 @@ def __init__( """ if not os.path.isabs(file_path): file_path = os.path.abspath(file_path) - 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) + 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() @@ -626,7 +648,7 @@ def __update_libraries(self): library, library_file, self.timeout, - tuple(self.__coq_lsp_options), + self.__coq_lsp_options, workspace=self.workspace, use_disk_cache=self.__use_disk_cache, )