search

sr-lab / coqpyt

Python client for coq-lsp
MIT License
25 stars 3 forks source link

failed tests and errors #45

Open jizej opened 3 months ago

jizej commented 3 months ago

Using the latest code on master, I tried running pytest test -s as instructed but had 3 failed tests and 2 tests with errors. Are these errors expected?

Here is the test summary: FAILED tests/test_coq_file.py::test_derive[test_derive.v] - TypeError: sequence item 0: expected str instance, NoneType found FAILED tests/test_readme.py::test_readme_example - AssertionError: assert 1 == 0 FAILED tests/proof_file/test_changes.py::TestProofChangeNestedProofs::test_change_nested_proofs - coqpyt.coq.exceptions.InvalidFileException: The file /tmp/teste79ae2f8a3334fce8831de9fcf0a6cd5.v is not valid. FAILED tests/proof_file/test_proof_file.py::TestProofNestedProofs::test_nested_proofs - AssertionError: assert 3 == 5 ERROR tests/proof_file/test_changes.py::TestProofChangeObligation::test_change_obligation - RuntimeError: Unknown obligation command with tag number 1: Obligation 2 of id2. ERROR tests/proof_file/test_proof_file.py::TestProofObligation::test_obligation - RuntimeError: Unknown obligation command with tag number 1: Obligation 2 of id2.

Nfsaavedra commented 3 months ago

Hi @jizej! Sorry for the late reply! These errors are not expected. All the tests pass in both the CI and my machine. Can you send me the versions of your python, coq-lsp, and Coq?