Add option to run tests for external libraries (#52)

* add option to run tests for external libraries

* black

Author: pcarrott

.github/workflows/test.yml

@@ -69,7 +69,7 @@ jobs:
       run: |
         eval $(opam env)
         cd coqpyt
-        pytest tests -s
+        pytest tests -s --runextra
 
     - name: Save opam
       id: cache-opam-save

README.md

@@ -189,9 +189,17 @@ with ProofFile(os.path.join(os.getcwd(), "examples/readme.v")) as proof_file:
 
 ## Tests
 
-To run the tests for CoqPyt go to the folder ``coqpyt`` and run:
+To run the core tests for CoqPyt go to the folder ``coqpyt`` and run:
 ```bash
-pytest tests -s
+pytest tests -rs
+```
+
+Skipped tests require the following external Coq libraries to run successfully:
+- [Coq-Equations](https://github.com/mattam82/Coq-Equations)
+
+To run all tests go to the folder ``coqpyt`` and run:
+```bash
+pytest tests -rs --runextra
 ```
 
 ## Contributing

coqpyt/tests/conftest.py

@@ -0,0 +1,23 @@
+import pytest
+
+
+def pytest_addoption(parser):
+    parser.addoption(
+        "--runextra",
+        action="store_true",
+        default=False,
+        help="run extra tests from external libraries",
+    )
+
+
+def pytest_configure(config):
+    config.addinivalue_line("markers", "extra: mark test as from external library")
+
+
+def pytest_collection_modifyitems(config, items):
+    if config.getoption("--runextra"):
+        return
+    skip_extra = pytest.mark.skip(reason="need --runextra option to run")
+    for item in items:
+        if "extra" in item.keywords:
+            item.add_marker(skip_extra)

coqpyt/tests/test_coq_file.py

@@ -280,8 +280,9 @@ def test_derive(setup, teardown):
         )
 
 
+@pytest.mark.extra
 @pytest.mark.parametrize("setup", ["test_equations.v"], indirect=True)
-def test_derive(setup, teardown):
+def test_equations(setup, teardown):
     coq_file.run()
     assert len(coq_file.context.terms) == 0
     assert coq_file.context.last_term is not None