Merge pull request #23 from sr-lab/refactor_package

Refactor package, file context and ProofFile execution

.github/workflows/readme.yml

@@ -0,0 +1,41 @@
+name: Embed code in README
+
+on:
+  push:
+    branches:
+      - master
+    paths:
+      - "examples/readme.py"
+      - "README.md"
+  pull_request_target:
+    types:
+      - opened
+      - edited
+    paths:
+      - "examples/readme.py"
+      - "README.md"
+
+jobs:
+  embed:
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Checkout
+      uses: actions/checkout@v3.5.2
+
+    - name: Set up node
+      uses: actions/setup-node@v4
+      with: 
+        node-version: 20
+
+    - name: Install embedme
+      run: npm install -g embedme
+
+    - name: Embed code
+      run: embedme README.md
+
+    - name: Commit changes
+      uses: EndBug/add-and-commit@v9
+      with:
+        add: "README.md"
+        push: origin ${{ github.head_ref }}

.github/workflows/test.yml

@@ -37,10 +37,12 @@ jobs:
       run: |
         opam install coq-lsp
 
-    - name: Install coq-lsp-pyclient
+    - name: Install coqpyt
       run: |
         pip install -e .
 
     - name: Run tests
       run: |
-        eval $(opam env) && pytest -s
+        eval $(opam env)
+        cd coqpyt
+        pytest tests -s

README.md

@@ -2,7 +2,7 @@
 
 Interact with Coq files and navigate through your proofs using our Python client for [coq-lsp](https://github.com/ejgallego/coq-lsp).
 
-Execute Coq files, retrieve the generated context and edit proofs through addition and removal of steps.
+Execute Coq files, retrieve the generated context and edit proofs through insertion and removal of steps.
 
 ## Installation
 
@@ -17,45 +17,63 @@ python -m pip install -e .
 ```
 
 ## Usage
-```python
-import os
-from coq.base_file import CoqFile
-from coq.proof_file import ProofFile
-from coq.structs import TermType
 
+Import classes from the ``coqpyt`` package.
+
+<!-- embedme examples/readme.py#L3-L5 -->
+```py
+from coqpyt.coq.structs import TermType
+from coqpyt.coq.base_file import CoqFile
+from coqpyt.coq.proof_file import ProofFile
+```
+
+Create a CoqFile object, execute the file and extract the generated context.
+
+<!-- embedme examples/readme.py#L7-L40 -->
+```py
 # Open Coq file
-with CoqFile(os.path.join(os.getcwd(), "examples/example.v")) as coq_file:
+with CoqFile(os.path.join(os.getcwd(), "examples/readme.v")) as coq_file:
     coq_file.exec(nsteps=2)
     # Get all terms defined until now
     print("Number of terms:", len(coq_file.context.terms))
     # Filter by Tactics
-    print("Number of tactics:",
+    print(
+        "Number of tactics:",
         len(
-            list(filter(
-                lambda term: term.type == TermType.TACTIC,
-                coq_file.context.terms.values(),
-            ))
-        )
+            list(
+                filter(
+                    lambda term: term.type == TermType.TACTIC,
+                    coq_file.context.terms.values(),
+                )
+            )
+        ),
     )
 
     # Enter proof
     coq_file.exec(nsteps=4)
     print("In proof:", coq_file.in_proof)
     # Get current goals
-    print(coq_file.current_goals())
+    print(coq_file.current_goals)
 
     # Save compiled file
     coq_file.save_vo()
-    print("Compiled file exists:", os.path.exists("examples/example.vo"))
-    os.remove("examples/example.vo")
+    print("Compiled file exists:", os.path.exists("examples/readme.vo"))
+    os.remove("examples/readme.vo")
 
     # Run remaining file
     coq_file.run()
     print("Checked:", coq_file.checked)
     # Get all terms defined until now
     print("Number of terms:", len(coq_file.context.terms))
+```
+
+Create a ProofFile object (a CoqFile instance) and interact with the proofs.
 
-with ProofFile(os.path.join(os.getcwd(), "examples/example.v")) as proof_file:
+<!-- embedme examples/readme.py#L42-L72 -->
+```py
+# Open Proof file
+with ProofFile(os.path.join(os.getcwd(), "examples/readme.v")) as proof_file:
+    proof_file.run()
     # Number of proofs in the file
     print("Number of proofs:", len(proof_file.proofs))
     print("Proof:", proof_file.proofs[0].text)
@@ -73,18 +91,22 @@ with ProofFile(os.path.join(os.getcwd(), "examples/example.v")) as proof_file:
     # Print number of terms in context
     print("Number of terms:", len(proof_file.context.terms))
     # Filter for Notations only
-    print("Number of notations:",
+    print(
+        "Number of notations:",
         len(
-            list(filter(
-                lambda term: term.type == TermType.NOTATION,
-                proof_file.context.terms.values(),
-            ))
-        )
+            list(
+                filter(
+                    lambda term: term.type == TermType.NOTATION,
+                    proof_file.context.terms.values(),
+                )
+            )
+        ),
     )
 ```
 
-### Run tests
+## Tests
 
+To run the tests for CoqPyt go to the folder ``coqpyt`` and run:
 ```bash
 pytest tests -s
 ```