diff --git a/coqpyt/coq/proof_file.py b/coqpyt/coq/proof_file.py index 5c43fd9..5aef324 100644 --- a/coqpyt/coq/proof_file.py +++ b/coqpyt/coq/proof_file.py @@ -3,6 +3,7 @@ import logging import tempfile import shutil +import pickle import uuid from functools import lru_cache from typing import Optional, Tuple, Union, List, Dict @@ -25,6 +26,8 @@ class _AuxFile(object): + CACHE_NAME = "coqpyt_cache" + def __init__( self, file_path, @@ -181,15 +184,52 @@ def set_cache_size(size: Optional[int]): _AuxFile.__load_library.__wrapped__, ) - @staticmethod + @classmethod + def get_coqpyt_disk_cache_loc(cls) -> Optional[str]: + if "HOME" in os.environ: + home_dir = os.environ["HOME"] + elif "USERPROFILE" in os.environ: + home_dir = os.environ["USERPROFILE"] + else: + return None + cache_loc = os.path.join(home_dir, ".cache", cls.CACHE_NAME) + return cache_loc + + @classmethod + def get_from_disk_cache(cls, library_hash: str) -> Optional[Dict[str, Term]]: + coqpyt_cache_loc = cls.get_coqpyt_disk_cache_loc() + if coqpyt_cache_loc is None: + return None + library_cache_loc = os.path.join(coqpyt_cache_loc, library_hash) + if os.path.exists(library_cache_loc): + with open(library_cache_loc, "rb") as f: + return pickle.load(f) + + @classmethod + def to_disk_cache(cls, library_hash: str, terms: Dict[str, Term]): + coqpyt_cache_loc = cls.get_coqpyt_disk_cache_loc() + if coqpyt_cache_loc is None: + return + library_cache_loc = os.path.join(coqpyt_cache_loc, library_hash) + os.makedirs(coqpyt_cache_loc, exist_ok=True) + with open(library_cache_loc, "wb") as f: + pickle.dump(terms, f) + + @classmethod def get_library( + cls, library_name: str, library_file: str, timeout: int, workspace: Optional[str] = None, + use_disk_cache: bool = False, ) -> Dict[str, Term]: with open(library_file, "r") as f: library_hash = hashlib.md5(f.read().encode("utf-8")).hexdigest() + if use_disk_cache: + 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 ) @@ -203,6 +243,8 @@ def get_library( for term in aux_context.terms.keys(): if terms[term].text.startswith("Local"): terms.pop(term) + if use_disk_cache: + cls.to_disk_cache(library_hash, terms) return terms @staticmethod @@ -216,7 +258,9 @@ 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) -> FileContext: + def get_coq_context( + timeout: int, workspace: Optional[str] = None, use_disk_cache: bool = False + ) -> FileContext: temp_path = os.path.join( tempfile.gettempdir(), "aux_" + str(uuid.uuid4()).replace("-", "") + ".v" ) @@ -234,7 +278,11 @@ def get_coq_context(timeout: int, workspace: Optional[str] = None) -> FileContex "Locate Library", library, i + 1 ).split()[-1][:-1] terms = _AuxFile.get_library( - library, v_file, timeout, workspace=workspace + library, + v_file, + timeout, + workspace=workspace, + use_disk_cache=use_disk_cache, ) context.add_library(library, terms) @@ -257,6 +305,7 @@ def __init__( coq_lsp: str = "coq-lsp", coqtop: str = "coqtop", error_mode: str = "strict", + use_disk_cache: bool = False, ): """Creates a ProofFile. @@ -275,18 +324,28 @@ def __init__( If "strict", an exception will be raised when an unexpected behavior occurs. If "warning", a warning will be logged instead (it only applies to recoverable errors). Defaults to "strict". + use_disk_cache (bool, optional): If True, the terms from each loaded library are stored + in a cache on disk. Then, when creating or manipulating future proof files, terms are + loaded from the cache if their corresponing library (file) has the same text. + Note that caching only depends on the text of the file, so if the Coq version changes, + or the version of coqpyt changes, the cache should be deleted. """ 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) self.__error_mode = error_mode + self.__use_disk_cache = use_disk_cache self.__aux_file.didOpen() try: # We need to update the context already defined in the CoqFile self.context.update( - _AuxFile.get_coq_context(self.timeout, workspace=self.workspace) + _AuxFile.get_coq_context( + self.timeout, + workspace=self.workspace, + use_disk_cache=self.__use_disk_cache, + ) ) except Exception as e: self.close() @@ -571,7 +630,11 @@ def __update_libraries(self): "Locate Library", library, last_line + i + 1 ).split()[-1][:-1] library_terms = _AuxFile.get_library( - library, library_file, self.timeout, workspace=self.workspace + library, + library_file, + self.timeout, + workspace=self.workspace, + use_disk_cache=self.__use_disk_cache, ) self.context.add_library(library, library_terms) diff --git a/coqpyt/tests/proof_file/test_cache.py b/coqpyt/tests/proof_file/test_cache.py new file mode 100644 index 0000000..4535b03 --- /dev/null +++ b/coqpyt/tests/proof_file/test_cache.py @@ -0,0 +1,37 @@ +from utility import * + + +class TestCache(SetupProofFile): + def setup_method(self, method): + self.setup( + "test_imports/test_import.v", + workspace="test_imports/", + use_disk_cache=False, + ) + self.no_cache_terms = self.proof_file.context.terms.copy() + self.no_cache_libs = self.proof_file.context.libraries.copy() + self.teardown_method(method) + + self.setup( + "test_imports/test_import.v", + workspace="test_imports/", + use_disk_cache=True, + ) + self.cache1_terms = self.proof_file.context.terms.copy() + self.cache1_libs = self.proof_file.context.libraries.copy() + self.teardown_method(method) + + self.setup( + "test_imports/test_import.v", + workspace="test_imports/", + use_disk_cache=True, + ) + self.cache2_terms = self.proof_file.context.terms.copy() + self.cache2_libs = self.proof_file.context.libraries.copy() + + def test_cache(self): + assert self.no_cache_terms == self.cache1_terms + assert self.cache1_terms == self.cache2_terms + + assert self.no_cache_libs == self.cache1_libs + assert self.cache1_libs == self.cache2_libs diff --git a/coqpyt/tests/proof_file/utility.py b/coqpyt/tests/proof_file/utility.py index 87183ac..0ce3a9b 100644 --- a/coqpyt/tests/proof_file/utility.py +++ b/coqpyt/tests/proof_file/utility.py @@ -15,7 +15,7 @@ class SetupProofFile(ABC): - def setup(self, file_path, workspace=None): + def setup(self, file_path, workspace=None, use_disk_cache: bool = False): if workspace is not None: self.workspace = os.path.join( tempfile.gettempdir(), "test" + str(uuid.uuid4()).replace("-", "") @@ -37,7 +37,10 @@ def setup(self, file_path, workspace=None): uri = "file://" + self.file_path self.proof_file = ProofFile( - self.file_path, timeout=60, workspace=self.workspace + self.file_path, + timeout=60, + workspace=self.workspace, + use_disk_cache=use_disk_cache, ) self.proof_file.run() self.versionId = VersionedTextDocumentIdentifier(uri, 1)