Merge pull request #19 from sr-lab/small_refactor

Support versions prior to 8.18 and refactor directory structure

README.md

@@ -1,8 +1,8 @@
-# coq-lsp-pyclient
+# CoqPyt
 
-Python client for [coq-lsp](https://github.com/ejgallego/coq-lsp).
+Interact with Coq files and navigate through your proofs using our Python client for [coq-lsp](https://github.com/ejgallego/coq-lsp).
 
-Abstraction to interact with Coq files, get their context, execute them, among other operations.
+Execute Coq files, retrieve the generated context and edit proofs through addition and removal of steps.
 
 ## Installation
 
@@ -19,9 +19,9 @@ python -m pip install -e .
 ## Usage
 ```python
 import os
-from coqlspclient.coq_file import CoqFile
-from coqlspclient.proof_file import ProofFile
-from coqlspclient.coq_structs import TermType
+from coq.base_file import CoqFile
+from coq.proof_file import ProofFile
+from coq.structs import TermType
 
 # Open Coq file
 with CoqFile(os.path.join(os.getcwd(), "examples/example.v")) as coq_file:

coqlspclient/coq_file.py → coq/base_file.py

@@ -2,19 +2,21 @@
 import shutil
 import uuid
 import tempfile
-from pylspclient.lsp_structs import (
+import subprocess
+from lsp.structs import (
     TextDocumentItem,
     TextDocumentIdentifier,
     VersionedTextDocumentIdentifier,
     TextDocumentContentChangeEvent,
 )
-from pylspclient.lsp_structs import ResponseError, ErrorCodes, Diagnostic
-from coqlspclient.coq_lsp_structs import Position, GoalAnswer, RangedSpan, Range
-from coqlspclient.coq_structs import Step, FileContext, Term, TermType, SegmentType
-from coqlspclient.coq_lsp_client import CoqLspClient
-from coqlspclient.coq_exceptions import *
-from coqlspclient.coq_changes import *
-from typing import List, Optional, Callable
+from lsp.structs import ResponseError, ErrorCodes, Diagnostic
+from coq.lsp.structs import Position, GoalAnswer, RangedSpan
+from coq.structs import Step, FileContext, Term, TermType, SegmentType
+from coq.lsp.client import CoqLspClient
+from coq.exceptions import *
+from coq.changes import *
+from typing import List, Optional
+from packaging import version
 
 
 class CoqFile(object):
@@ -40,6 +42,8 @@ def __init__(
         library: Optional[str] = None,
         timeout: int = 30,
         workspace: Optional[str] = None,
+        coq_lsp: str = "coq-lsp",
+        coqtop: str = "coqtop",
     ):
         """Creates a CoqFile.
 
@@ -50,13 +54,17 @@ def __init__(
             workspace(Optional[str], optional): Absolute path for the workspace.
                 If the workspace is not defined, the workspace is equal to the
                 path of the file.
+            coq_lsp(str, optional): Path to the coq-lsp binary. Defaults to "coq-lsp".
+            coqtop(str, optional): Path to the coqtop binary used to compile the Coq libraries
+                imported by coq-lsp. This is NOT passed as a parameter to coq-lsp, it is
+                simply used to check the Coq version in use. Defaults to "coqtop".
         """
         self.__init_path(file_path, library)
         if workspace is not None:
             uri = f"file://{workspace}"
         else:
             uri = f"file://{self.__path}"
-        self.coq_lsp_client = CoqLspClient(uri, timeout=timeout)
+        self.coq_lsp_client = CoqLspClient(uri, timeout=timeout, coq_lsp=coq_lsp)
         uri = f"file://{self.__path}"
         text = self.__read()
 
@@ -70,6 +78,7 @@ def __init__(
         self.steps_taken: int = 0
         self.__init_steps(text, ast)
         self.__validate()
+        self.__init_coq_version(coqtop)
         self.curr_module: List[str] = []
         self.curr_module_type: List[str] = []
         self.curr_section: List[str] = []
@@ -161,6 +170,19 @@ def __validate(self):
                     step.diagnostics.append(diagnostic)
                     break
 
+    def __init_coq_version(self, coqtop):
+        output = subprocess.check_output(f"{coqtop} -v", shell=True)
+        coq_version = output.decode("utf-8").split("\n")[0].split()[-1]
+        outdated = version.parse(coq_version) < version.parse("8.18")
+
+        # For version 8.18, we ignore the tags [VernacSynterp] and [VernacSynPure]
+        # and use the "ntn_decl" prefix when handling where notations
+        # For older versions, we only tested 8.17, so we provide no claims about
+        # versions prior to that.
+
+        self.__expr = lambda e: e if outdated else e[1]
+        self.__where_notation_key = "decl_ntn" if outdated else "ntn_decl"
+
     @property
     def curr_step(self):
         return self.steps[self.steps_taken]
@@ -199,17 +221,15 @@ def get_v(el):
             return el[1]
         return None
 
-    @staticmethod
-    def expr(step: RangedSpan) -> Optional[List]:
+    def expr(self, step: RangedSpan) -> Optional[List]:
         if (
             step.span is not None
             and isinstance(step.span, dict)
             and "v" in step.span
             and isinstance(step.span["v"], dict)
             and "expr" in step.span["v"]
         ):
-            # We ignore the tags [VernacSynterp] and [VernacSynPure]
-            return step.span["v"]["expr"][1]
+            return self.__expr(step.span["v"]["expr"])
 
         return [None]
 
@@ -324,7 +344,8 @@ def __handle_where_notations(self, expr: List, term_type: TermType):
         # handles when multiple notations are defined
         for span in spans:
             name = FileContext.get_notation_key(
-                span["ntn_decl_string"]["v"], span["ntn_decl_scope"]
+                span[f"{self.__where_notation_key}_string"]["v"],
+                span[f"{self.__where_notation_key}_scope"],
             )
             self.__add_term(name, self.curr_step, TermType.NOTATION)
 
@@ -383,7 +404,7 @@ def traverse_expr(expr):
             ]:
                 if text.startswith(keyword):
                     return
-            expr = CoqFile.expr(self.curr_step.ast)
+            expr = self.expr(self.curr_step.ast)
             if expr == [None]:
                 return
             if expr[0] == "VernacExtend" and expr[1][0] == "VernacSolve":
@@ -688,9 +709,8 @@ def diagnostics(self) -> List[Diagnostic]:
         uri = f"file://{self.__path}"
         return self.coq_lsp_client.lsp_endpoint.diagnostics[uri]
 
-    @staticmethod
-    def get_term_type(ast: RangedSpan) -> TermType:
-        expr = CoqFile.expr(ast)
+    def get_term_type(self, ast: RangedSpan) -> TermType:
+        expr = self.expr(ast)
         if expr is not None:
             return CoqFile.__get_term_type(expr)
         return TermType.OTHER

coqlspclient/coq_lsp_client.py → coq/lsp/client.py

@@ -1,10 +1,10 @@
 import time
 import subprocess
-from pylspclient.json_rpc_endpoint import JsonRpcEndpoint
-from pylspclient.lsp_endpoint import LspEndpoint
-from pylspclient.lsp_client import LspClient
-from pylspclient.lsp_structs import *
-from coqlspclient.coq_lsp_structs import *
+from lsp.json_rpc_endpoint import JsonRpcEndpoint
+from lsp.endpoint import LspEndpoint
+from lsp.client import LspClient
+from lsp.structs import *
+from coq.lsp.structs import *
 
 
 class CoqLspClient(LspClient):
@@ -27,6 +27,7 @@ def __init__(
         root_uri: str,
         timeout: int = 30,
         memory_limit: int = 2097152,
+        coq_lsp: str = "coq-lsp",
         init_options: Dict = __DEFAULT_INIT_OPTIONS,
     ):
         """Creates a CoqLspClient
@@ -38,6 +39,7 @@ def __init__(
                 Defaults to 2.
             memory_limit (int, optional): RAM limit for the coq-lsp process
                 in kbytes. Defaults to 2097152.
+            coq_lsp(str, optional): Path to the coq-lsp binary. Defaults to "coq-lsp".
             init_options (Dict, optional): Initialization options for coq-lsp server.
                 Available options are:
                     max_errors (int): Maximum number of errors per file, after that,
@@ -56,7 +58,7 @@ def __init__(
         """
         self.file_progress: Dict[str, List[CoqFileProgressParams]] = {}
         proc = subprocess.Popen(
-            f"ulimit -v {memory_limit}; coq-lsp",
+            f"ulimit -v {memory_limit}; {coq_lsp}",
             stdout=subprocess.PIPE,
             stdin=subprocess.PIPE,
             shell=True,

coqlspclient/coq_lsp_structs.py → coq/lsp/structs.py

@@ -1,6 +1,6 @@
 from enum import Enum
 from typing import Dict, Optional, Any, List, Tuple
-from pylspclient.lsp_structs import Range, VersionedTextDocumentIdentifier, Position
+from lsp.structs import Range, VersionedTextDocumentIdentifier, Position
 
 
 class Hyp(object):

coqlspclient/proof_file.py → coq/proof_file.py

@@ -3,26 +3,26 @@
 import shutil
 import uuid
 import tempfile
-from pylspclient.lsp_structs import (
+from lsp.structs import (
     TextDocumentItem,
     VersionedTextDocumentIdentifier,
     TextDocumentContentChangeEvent,
     ResponseError,
     ErrorCodes,
 )
-from coqlspclient.coq_structs import (
+from coq.structs import (
     TermType,
     Step,
     Term,
     ProofStep,
     ProofTerm,
     FileContext,
 )
-from coqlspclient.coq_lsp_structs import Result, Query, GoalAnswer, Range
-from coqlspclient.coq_file import CoqFile
-from coqlspclient.coq_lsp_client import CoqLspClient
-from coqlspclient.coq_changes import *
-from coqlspclient.coq_exceptions import *
+from coq.lsp.structs import Result, Query, GoalAnswer, Range
+from coq.base_file import CoqFile
+from coq.lsp.client import CoqLspClient
+from coq.changes import *
+from coq.exceptions import *
 from typing import List, Dict, Optional, Tuple
 
 
@@ -199,6 +199,8 @@ def __init__(
         library: Optional[str] = None,
         timeout: int = 30,
         workspace: Optional[str] = None,
+        coq_lsp: str = "coq-lsp",
+        coqtop: str = "coqtop",
     ):
         """Creates a ProofFile.
 
@@ -209,8 +211,12 @@ def __init__(
             workspace(Optional[str], optional): Absolute path for the workspace.
                 If the workspace is not defined, the workspace is equal to the
                 path of the file.
+            coq_lsp(str, optional): Path to the coq-lsp binary. Defaults to "coq-lsp".
+            coqtop(str, optional): Path to the coqtop binary used to compile the Coq libraries
+                imported by coq-lsp. This is NOT passed as a parameter to coq-lsp, it is
+                simply used to check the Coq version in use. Defaults to "coqtop".
         """
-        super().__init__(file_path, library, timeout, workspace)
+        super().__init__(file_path, library, timeout, workspace, coq_lsp, coqtop)
         self.__aux_file = _AuxFile(timeout=self.timeout)
 
         try:
@@ -279,7 +285,7 @@ def __search_notation(call):
                             stack.append(v)
             return res
 
-        return traverse_expr(CoqFile.expr(step.ast))
+        return traverse_expr(self.expr(step.ast))
 
     def __get_last_term(self):
         terms = self.terms
@@ -313,9 +319,9 @@ def traverse_expr(expr):
         # 3 - Obligation N
         # 4 - Next Obligation of id
         # 5 - Next Obligation
-        tag = CoqFile.expr(self.prev_step.ast)[1][1]
+        tag = self.expr(self.prev_step.ast)[1][1]
         if tag in [0, 1, 4]:
-            id = traverse_expr(CoqFile.expr(self.prev_step.ast))
+            id = traverse_expr(self.expr(self.prev_step.ast))
             # This works because the obligation must be in the
             # same module as the program
             id = ".".join(self.curr_module + [id])
@@ -359,7 +365,7 @@ def __get_steps(
 
             self.__step()
             # Nested proofs
-            if CoqFile.get_term_type(self.prev_step.ast) != TermType.OTHER:
+            if self.get_term_type(self.prev_step.ast) != TermType.OTHER:
                 self.__get_proof(proofs)
                 # Pass Qed if it exists
                 while not self.in_proof and not self.checked:
@@ -377,17 +383,17 @@ def __get_steps(
             raise e
         if (
             self.steps_taken < len(self.steps)
-            and CoqFile.expr(self.curr_step.ast)[0] == "VernacEndProof"
+            and self.expr(self.curr_step.ast)[0] == "VernacEndProof"
         ):
             steps.append((self.curr_step, goals, []))
 
         return steps
 
     def __get_proof(self, proofs):
         term, statement_context = None, None
-        if CoqFile.get_term_type(self.prev_step.ast) == TermType.OBLIGATION:
+        if self.get_term_type(self.prev_step.ast) == TermType.OBLIGATION:
             term, statement_context = self.__get_program_context()
-        elif CoqFile.get_term_type(self.prev_step.ast) != TermType.OTHER:
+        elif self.get_term_type(self.prev_step.ast) != TermType.OTHER:
             term = self.__get_last_term()
             statement_context = self.__step_context(self.prev_step)
         # HACK: We ignore proofs inside a Module Type since they can't be used outside

coqlspclient/coq_structs.py → coq/structs.py

@@ -1,8 +1,8 @@
 import re
 from enum import Enum
 from typing import Dict, List, Union, Callable
-from coqlspclient.coq_lsp_structs import RangedSpan, GoalAnswer
-from pylspclient.lsp_structs import Diagnostic, Position
+from coq.lsp.structs import RangedSpan, GoalAnswer
+from lsp.structs import Diagnostic, Position
 
 
 class SegmentType(Enum):

lsp/__init__.py

@@ -0,0 +1,8 @@
+# from __future__ import absolute_import
+
+__all__ = []
+
+from lsp.json_rpc_endpoint import JsonRpcEndpoint
+from lsp.client import LspClient
+from lsp.endpoint import LspEndpoint
+from lsp import structs