change cache to lru_cache (#30)

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