diff --git a/coqpyt/coq/proof_file.py b/coqpyt/coq/proof_file.py index d1c079d..5c3f7a9 100644 --- a/coqpyt/coq/proof_file.py +++ b/coqpyt/coq/proof_file.py @@ -3,7 +3,7 @@ import tempfile import shutil import uuid -import threading +from functools import lru_cache from typing import Optional, Tuple, Union, List, Dict from coqpyt.lsp.structs import ( @@ -27,9 +27,6 @@ class _AuxFile(object): - __CACHE: Dict[Tuple[str, str], FileContext] = {} - __CACHE_LOCK = threading.Lock() - def __init__( self, file_path, @@ -162,25 +159,27 @@ def close(self): self.coq_lsp_client.exit() os.remove(self.path) + @staticmethod + @lru_cache(maxsize=128) + def __load_library( + library_name: str, library_file: str, library_hash: str, timeout: int + ): + # NOTE: the library_hash attribute is only used for the LRU cache + coq_file = CoqFile(library_file, library=library_name, timeout=timeout) + coq_file.run() + context = coq_file.context + coq_file.close() + return context + @staticmethod def get_library( library_name: str, library_file: str, timeout: int ) -> Dict[str, Term]: with open(library_file, "r") as f: - hash = hashlib.md5(f.read().encode("utf-8")).hexdigest() - if (library_file, hash) in _AuxFile.__CACHE: - _AuxFile.__CACHE_LOCK.acquire() - aux_context = _AuxFile.__CACHE[(library_file, hash)] - _AuxFile.__CACHE_LOCK.release() - else: - coq_file = CoqFile(library_file, library=library_name, timeout=timeout) - coq_file.run() - aux_context = coq_file.context - _AuxFile.__CACHE_LOCK.acquire() - _AuxFile.__CACHE[(library_file, hash)] = aux_context - _AuxFile.__CACHE_LOCK.release() - coq_file.close() - + library_hash = hashlib.md5(f.read().encode("utf-8")).hexdigest() + aux_context = _AuxFile.__load_library( + library_name, library_file, library_hash, timeout + ) # 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