Hit:1 http://security.ubuntu.com/ubuntu noble-security InRelease
Hit:2 http://archive.ubuntu.com/ubuntu noble InRelease
Hit:3 http://archive.ubuntu.com/ubuntu noble-updates InRelease
Hit:4 http://archive.ubuntu.com/ubuntu noble-backports InRelease
Reading package lists...
Reading package lists...
Building dependency tree...
Reading state information...
curl is already the newest version (8.5.0-2ubuntu10.8).
0 upgraded, 0 newly installed, 0 to remove and 58 not upgraded.
downloading uv 0.9.5 x86_64-unknown-linux-gnu
no checksums to verify
installing to /root/.local/bin
  uv
  uvx
everything's installed!
Downloading cpython-3.13.9-linux-x86_64-gnu (download) (32.0MiB)
 Downloading cpython-3.13.9-linux-x86_64-gnu (download)
Downloading pygments (1.2MiB)
 Downloading pygments
Installed 6 packages in 18ms
============================= test session starts ==============================
platform linux -- Python 3.13.9, pytest-8.4.1, pluggy-1.6.0
rootdir: /tests
plugins: json-ctrf-0.3.5
collected 4 items

../tests/test_outputs.py .FFF                                            [100%]

=================================== FAILURES ===================================
__________________________ test_compiled_proof_exists __________________________

    def test_compiled_proof_exists():
>       assert os.path.exists("plus_comm.vo"), (
            "The compiled proof file plus_comm.vo should exist"
        )
E       AssertionError: The compiled proof file plus_comm.vo should exist
E       assert False
E        +  where False = <function exists at 0x7fffff1e3240>('plus_comm.vo')
E        +    where <function exists at 0x7fffff1e3240> = <module 'posixpath' (frozen)>.exists
E        +      where <module 'posixpath' (frozen)> = os.path

/tests/test_outputs.py:12: AssertionError
_____________________________ test_proof_contents ______________________________

    def test_proof_contents():
        with open("plus_comm.v", "r") as f:
            content = f.read()
            assert "n + m = m + n" in content, (
                "The file should contain the plus_comm theorem"
            )
            assert "Proof." in content, "The file should contain a proof"
            assert "Qed." in content, "The proof should be completed with Qed"
>           assert "admit" not in content, "The proof should not contain any admits"
E           AssertionError: The proof should not contain any admits
E           assert 'admit' not in 'Require Imp...dmit.\nQed. '
E             
E             'admit' is contained here:
E               se *)
E                   admit.
E                 - simpl.
E                   (* Need to use the inductive hypothesis and plus_n_Sm *)
E                   admit.
E               Qed.

/tests/test_outputs.py:25: AssertionError
_________________________ test_compiled_proof_content __________________________

    def test_compiled_proof_content():
        # First verify the proof compiles without errors
        compile_result = subprocess.run(
            ["coqc", "plus_comm.v"],
            capture_output=True,
            text=True,
        )
>       assert compile_result.returncode == 0, "Proof should compile without errors"
E       AssertionError: Proof should compile without errors
E       assert 1 == 0
E        +  where 1 = CompletedProcess(args=['coqc', 'plus_comm.v'], returncode=1, stdout='', stderr='File "./plus_comm.v", line 14, charact...ttempt to save a proof with given up goals. If\nthis is really what you want to do, use Admitted in place of Qed.\n\n').returncode

/tests/test_outputs.py:35: AssertionError
==================================== PASSES ====================================
=========================== short test summary info ============================
PASSED ../tests/test_outputs.py::test_proof_file_exists
FAILED ../tests/test_outputs.py::test_compiled_proof_exists - AssertionError:...
FAILED ../tests/test_outputs.py::test_proof_contents - AssertionError: The pr...
FAILED ../tests/test_outputs.py::test_compiled_proof_content - AssertionError...
========================= 3 failed, 1 passed in 0.36s ==========================
