Add support to Rocq 9.0.1 (#63)

Author: pcarrott

.github/workflows/lint.yml

@@ -17,4 +17,4 @@ jobs:
         uses: psf/black@stable
         with:
           options: "--check --verbose"
-          version: "23.3.0"
+          version: "25.9.0"

.github/workflows/test.yml

@@ -12,15 +12,23 @@ jobs:
     strategy:
       matrix:
         ocaml-compiler:
-          - "5.2.0"
+          - "5.3.0"
         coq-version:
-          - "8.17.1"
-          - "8.18.0"
-          - "8.19.2"
-          - "8.20.0"
+          - main: "8.17"
+            patch: "1"
+          - main: "8.18"
+            patch: "0"
+          - main: "8.19"
+            patch: "2"
+          - main: "8.20"
+            patch: "1"
+          - main: "9.0"
+            patch: "1"
+        coq-lsp-version:
+          - "0.2.3"
         python-version:
-          - '3.11'
           - '3.12'
+          - '3.13'
 
     steps:
     - name: Checkout
@@ -42,7 +50,7 @@ jobs:
       with:
         path: |
           /home/runner/work/coqpyt/coqpyt/_opam/
-        key: ${{ matrix.ocaml-compiler }}-${{ matrix.coq-version }}-opam
+        key: ${{ matrix.ocaml-compiler }}-${{ matrix.coq-version.main }}.${{ matrix.coq-version.patch }}-opam
 
     - name: Set-up OCaml
       uses: ocaml/setup-ocaml@v3
@@ -52,8 +60,8 @@ jobs:
     - name: Install coq-lsp
       if: steps.cache-opam-restore.outputs.cache-hit != 'true'
       run: |
-        opam pin add coq ${{ matrix.coq-version }}
-        opam install coq-lsp
+        opam pin add coq ${{ matrix.coq-version.main }}.${{ matrix.coq-version.patch }}
+        opam pin add coq-lsp ${{ matrix.coq-lsp-version }}+${{ matrix.coq-version.main }}
 
     - name: Add coq-released
       if: steps.cache-opam-restore.outputs.cache-hit != 'true'

README.md

@@ -20,9 +20,9 @@ If you use CoqPyt in an article, please cite:
 
 ## Installation
 
-[Python](https://www.python.org/) must be installed on version >= 3.11.
+[Python](https://www.python.org/) must be installed on version >= 3.12.
 
-[coq-lsp](https://github.com/ejgallego/coq-lsp) must be installed on version >= 0.1.7. Follow the installation instructions provided [here](https://github.com/ejgallego/coq-lsp#%EF%B8%8F-installation).
+[coq-lsp](https://github.com/ejgallego/coq-lsp) should be installed on version 0.2.3 (earlier versions are untested but may be compatible). Follow the installation instructions provided [here](https://github.com/ejgallego/coq-lsp#%EF%B8%8F-installation).
 
 ```bash
 pip install -r requirements.txt

coqpyt/coq/base_file.py

@@ -96,7 +96,7 @@ def __exit__(self, exc_type, exc_value, traceback):
 
     def __init_path(self, file_path, library):
         self.file_module = [] if library is None else library.split(".")
-        self.__from_lib = self.file_module[:2] == ["Coq", "Init"]
+        self.__from_lib = self.file_module[:2] in [["Coq", "Init"], ["Corelib", "Init"]]
         self.path = file_path
         if not self.__from_lib:
             self._path = file_path

coqpyt/coq/context.py

@@ -40,7 +40,48 @@ def __init_coq_version(self, coqtop):
         # from ProofFile to here.
         self.ext_index = lambda e: e["ext_index"] if post18 else e[1]
 
-        # We only tested versions 8.17/8.18/8.19, so we provide no claims about
+        # For versions 9.0+, the AST structure for fixpoints changed and obligation
+        # commands have less tags
+        rocq = version.parse(coq_version) >= version.parse("9.0")
+        self.__fixpoint_notations = lambda e: (
+            []
+            if len(e) < 3 or not isinstance(e[2], list)
+            else (
+                e[2][1][0]["notations"]
+                if (
+                    rocq
+                    and len(e[2]) > 1
+                    and isinstance(e[2][1], list)
+                    and len(e[2][1]) > 0
+                    and isinstance(e[2][1][0], dict)
+                    and "notations" in e[2][1][0]
+                    and isinstance(e[2][1][0]["notations"], list)
+                )
+                else (
+                    e[2][0]["notations"]
+                    if (
+                        not rocq
+                        and len(e[2]) > 0
+                        and isinstance(e[2][0], dict)
+                        and "notations" in e[2][0]
+                        and isinstance(e[2][0]["notations"], list)
+                    )
+                    else []
+                )
+            )
+        )
+        # FIXME: This should be made private once [__get_program_context] is extracted
+        # from ProofFile to here.
+        # Tags pre-Rocq:                    Tags post-Rocq:
+        # 0 - Obligation N of id : type
+        # 1 - Obligation N of id            0 - Obligation N of id
+        # 2 - Obligation N : type
+        # 3 - Obligation N                  1 - Obligation N
+        # 4 - Next Obligation of id         2 - Next Obligation of id
+        # 5 - Next Obligation               3 - Next Obligation
+        self.obligation_tag_with_id = lambda t: t in ([0, 2] if rocq else [0, 1, 4])
+
+        # We only tested versions 8.17 to 9.0, so we provide no claims about
         # versions prior to that.
 
     def __init_context(self, terms: Optional[Dict[str, Term]] = None):
@@ -188,17 +229,8 @@ def __handle_where_notations(self, step: Step, expr: List, term_type: TermType):
             and len(expr[2][0][1]) > 0
         ):
             spans = expr[2][0][1]
-        elif (
-            term_type == TermType.FIXPOINT
-            and len(expr) > 2
-            and isinstance(expr[2], list)
-            and len(expr[2]) > 0
-            and isinstance(expr[2][0], dict)
-            and "notations" in expr[2][0]
-            and isinstance(expr[2][0]["notations"], list)
-            and len(expr[2][0]["notations"]) > 0
-        ):
-            spans = expr[2][0]["notations"]
+        elif term_type == TermType.FIXPOINT:
+            spans = self.__fixpoint_notations(expr)
 
         # handles when multiple notations are defined
         for span in spans:

coqpyt/coq/proof_file.py

@@ -458,15 +458,8 @@ def __step_context(self, step: Step) -> List[Term]:
 
     def __get_program_context(self) -> Tuple[Term, List[Term]]:
         expr = self.context.expr(self.prev_step)
-        # Tags:
-        # 0 - Obligation N of id : type
-        # 1 - Obligation N of id
-        # 2 - Obligation N : type
-        # 3 - Obligation N
-        # 4 - Next Obligation of id
-        # 5 - Next Obligation
         tag = self.context.ext_index(expr[1])
-        if tag in [0, 1, 4]:
+        if self.context.obligation_tag_with_id(tag):
             stack = expr[:0:-1]
             while len(stack) > 0:
                 el = stack.pop()
@@ -483,7 +476,7 @@ def __get_program_context(self) -> Tuple[Term, List[Term]]:
                 for v in reversed(el):
                     if isinstance(v, list):
                         stack.append(v)
-        elif tag in [2, 3, 5]:
+        else:
             id = self.current_goals.program[0][0][1]
             # This works because the obligation must be in the
             # same module as the program
@@ -1047,3 +1040,9 @@ def change_steps(self, changes: List[CoqChange]):
     def close(self):
         super().close()
         self.__aux_file.close()
+
+    @staticmethod
+    def clear_disk_cache():
+        cache_loc = _AuxFile.get_coqpyt_disk_cache_loc()
+        if cache_loc is not None and os.path.exists(cache_loc):
+            shutil.rmtree(cache_loc, ignore_errors=True)

coqpyt/tests/proof_file/expected/imports.yml

@@ -173,6 +173,9 @@ proofs:
         "8.20.x":
           text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 10, x binder, y binder, P at level 200, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
           type: NOTATION
+        "9.0.x":
+          text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 10, x binder, y binder, P at level 200, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
+          type: NOTATION
         default:
           text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder, right associativity, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
           type: NOTATION

coqpyt/tests/proof_file/expected/valid_file.yml

@@ -204,6 +204,9 @@ proofs:
         "8.20.x":
           text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 10, x binder, y binder, P at level 200, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
           type: NOTATION
+        "9.0.x":
+          text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 10, x binder, y binder, P at level 200, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
+          type: NOTATION
         default:
           text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder, right associativity, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
           type: NOTATION
@@ -373,6 +376,9 @@ proofs:
         "8.20.x":
           text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 10, x binder, y binder, P at level 200, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
           type: NOTATION
+        "9.0.x":
+          text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 10, x binder, y binder, P at level 200, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
+          type: NOTATION
         default:
           text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder, right associativity, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
           type: NOTATION

coqpyt/tests/proof_file/test_cache.py

@@ -21,6 +21,8 @@ def term_files_eq(terms1: dict[str, Term], terms2: dict[str, Term]) -> bool:
         return True
 
     def test_cache(self):
+        ProofFile.clear_disk_cache()
+
         with ProofFile(
             "tests/resources/test_imports/test_import.v",
             workspace="tests/resources/test_import",

coqpyt/tests/proof_file/test_changes.py

@@ -5,6 +5,7 @@
 from coqpyt.coq.changes import *
 
 from utility import *
+from packaging import version
 
 
 class TestProofValidFile(SetupProofFile):
@@ -23,12 +24,18 @@ def test_delete_and_add(self):
             if i != len(test_proofs["proofs"][0]["steps"]) - 1:
                 step["goals"]["goals"]["goals"][0]["hyps"] = []
                 step["goals"]["goals"]["goals"][0]["ty"] = "∀ n : nat, 0 + n = n"
-        check_proof(test_proofs["proofs"][0], proof_file.proofs[0])
+        check_proof(
+            test_proofs["proofs"][0],
+            proof_file.proofs[0],
+        )
 
         proof_file.add_step(5, "\n      intros n.")
 
         test_proofs = get_test_proofs("tests/proof_file/expected/valid_file.yml")
-        check_proof(test_proofs["proofs"][0], proof_file.proofs[0])
+        check_proof(
+            test_proofs["proofs"][0],
+            proof_file.proofs[0],
+        )
 
         # Check if context is changed correctly
         proof_file.add_step(7, "\n      Print minus.")
@@ -53,7 +60,10 @@ def test_delete_and_add(self):
         test_proofs["proofs"][0]["steps"].insert(3, step)
         for i, step in enumerate(test_proofs["proofs"][0]["steps"][4:]):
             step["goals"]["position"]["line"] += 1
-        check_proof(test_proofs["proofs"][0], proof_file.proofs[0])
+        check_proof(
+            test_proofs["proofs"][0],
+            proof_file.proofs[0],
+        )
 
         # Add step in beginning of proof
         proof_file.add_step(26, "\n    Print plus.")
@@ -115,7 +125,10 @@ def test_change_steps(self):
         test_proofs["proofs"][0]["steps"].insert(3, step)
         for step in test_proofs["proofs"][0]["steps"][4:]:
             step["goals"]["position"]["line"] += 1
-        check_proof(test_proofs["proofs"][0], proof_file.proofs[0])
+        check_proof(
+            test_proofs["proofs"][0],
+            proof_file.proofs[0],
+        )
 
         # Add step in beginning of proof
         proof_file.change_steps([CoqAdd("\n    Print plus.", 26)])
@@ -558,6 +571,108 @@ class TestProofChangeObligation(SetupProofFile):
     def setup_method(self, method):
         self.setup("test_obligation.v")
 
+    def test_change_obligation(self):
+        proof_file = self.proof_file
+
+        # Delete unwanted steps
+        proof_file.change_steps([CoqDelete(2) for _ in range(30)])
+        proof_file.change_steps([CoqDelete(4) for _ in range(8)])
+        proof_file.change_steps([CoqDelete(16), CoqDelete(2)])
+        proof_file.change_steps([CoqDelete(12) for _ in range(3)])
+
+        # Add a Program definition
+        program = (
+            "\n\nProgram Definition idx (n : nat) : { x : nat | x = n } :="
+            + "\n  if dec (Nat.leb n 0) then 0%nat"
+            + "\n  else pred (S n)."
+        )
+        proof_file.add_step(8, program)
+
+        # Add a Program lemma and proof
+        lemma = "\nProgram Lemma id_lemma (n : nat) : id n = n."
+        lemma_proof = ["\nProof.", " destruct n; try reflexivity.", " Qed."]
+        proof_file.add_step(9, lemma)
+        proof_file.change_steps([CoqAdd(lemma_proof[i], 10 + i) for i in range(3)])
+
+        # Add a proof for each obligation of the new Program
+        proof = ["\nNext Obligation.", "\n  dummy_tactic n e.", "\nQed."]
+        for i, step in enumerate(proof):
+            proof_file.add_step(16 + i, step)
+        for i, step in enumerate(proof):
+            proof_file.add_step(19 + i, step)
+
+        texts = [
+            "Obligation 1 of id with reflexivity.",
+            "Obligation 1 of id.",
+            "Next Obligation.",
+            "Next Obligation.",
+        ]
+        programs = [
+            ("#[program]", "id", "pred (S n)"),
+            ("Program", "id", "S (pred n)"),
+            ("Program", "id", "S (pred n)"),
+            ("Program", "idx", "pred (S n)"),
+        ]
+
+        # Steps were added to the end of the file
+        proof_file.run()
+
+        # Check the proofs
+        assert len(proof_file.proofs) == 5
+        assert len(proof_file.open_proofs) == 0
+        proofs = proof_file.proofs[:1] + proof_file.proofs[2:]
+        for i, proof in enumerate(proofs):
+            assert proof.text == texts[i]
+            assert proof.program is not None
+            assert (
+                proof.program.text
+                == programs[i][0]
+                + " Definition "
+                + programs[i][1]
+                + " (n : nat) : { x : nat | x = n } := if dec (Nat.leb n 0) then 0%nat else "
+                + programs[i][2]
+                + "."
+            )
+            assert len(proof.steps) == 2
+            assert proof.steps[0].text == "\n  dummy_tactic n e."
+        assert proof_file.proofs[1].text == lemma[1:]
+        assert proof_file.proofs[1].program is None
+        for i, step in enumerate(proof_file.proofs[1].steps):
+            assert lemma_proof[i] == step.text
+
+        # Delete last Next Obligation proof
+        for i in range(3):
+            proof_file.delete_step(proof_file.steps_taken - 1)
+        # Delete new Program definition and new Program lemma and proof
+        proof_file.change_steps([CoqDelete(9) for _ in range(5)])
+
+        # Check the proofs
+        assert len(proof_file.proofs) == 3
+        assert len(proof_file.open_proofs) == 0
+        for i, proof in enumerate(proof_file.proofs):
+            assert proof.text == texts[i]
+            assert proof.program is not None
+            assert (
+                proof.program.text
+                == programs[i][0]
+                + " Definition "
+                + programs[i][1]
+                + " (n : nat) : { x : nat | x = n } := if dec (Nat.leb n 0) then 0%nat else "
+                + programs[i][2]
+                + "."
+            )
+            assert len(proof.steps) == 2
+            assert proof.steps[0].text == "\n  dummy_tactic n e."
+
+
+class TestProofChangeObligationWithType(SetupProofFile):
+    def setup_method(self, method):
+        self.setup("test_obligation_with_type.v")
+
+    @pytest.mark.skipif(
+        version.parse(SetupProofFile.COQ_VERSION) >= version.parse("9.0"),
+        reason='Obligations with " : type" are not included in Rocq 9.0+',
+    )
     def test_change_obligation(self):
         proof_file = self.proof_file