Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

change cache to LRU cache #30

Merged
merged 1 commit into from
Dec 14, 2023
Merged

change cache to LRU cache #30

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
35 changes: 17 additions & 18 deletions coqpyt/coq/proof_file.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 (
Expand All @@ -27,9 +27,6 @@


class _AuxFile(object):
__CACHE: Dict[Tuple[str, str], FileContext] = {}
__CACHE_LOCK = threading.Lock()

def __init__(
self,
file_path,
Expand Down Expand Up @@ -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
Expand Down