Stream: PyCoq

Topic: pycoq module state?

Quinn (Nov 05 2021 at 13:03):

Drawing up a basic property test gave me this

Traceback (most recent call last):
  File "test/py/test_spec.py", line 41, in <module>
    test_lia()
  File "test/py/test_spec.py", line 8, in test_lia
    def test_lia(x: int, y: int):
  File "/home/quinn/.local/lib/python3.8/site-packages/hypothesis/core.py", line 1199, in wrapped_test
    raise the_error_hypothesis_found
  File "/home/quinn/.local/lib/python3.8/site-packages/hypothesis/core.py", line 890, in __flaky
    raise Flaky(message)
hypothesis.errors.Flaky: Hypothesis test_lia(x=1, y=11) produces unreliable results: Falsified on the first call but did not on a subsequent one

There's some impurity going on such that even in this _really_ simple test environment we don't have determinism. I think that's a bad sign.

Emilio Jesús Gallego Arias (Nov 05 2021 at 13:20):

Oh, indeed Coq is stateful, in the sense that if you add a lemma, for a next add, adding a lemma will fail due to a name clash.

Emilio Jesús Gallego Arias (Nov 05 2021 at 13:20):

For testing whitin the same coq isntance, I'd recommend using Cancel to undo the added sentences

Emilio Jesús Gallego Arias (Nov 05 2021 at 13:20):

This will restore the initial state reliably except in the case of loading of ML plugins [which is very rare]

Quinn (Nov 05 2021 at 13:24):

ok. We can live if we import coq from inside a pytest.fixture. But perhaps we should discuss a coq class so that there isn't one global instance

Quinn (Nov 05 2021 at 13:25):

I believe collections.deque has a solution where the module state is the contents of your queue, but the module is callable somehow so that every time you call it you spin up an isolated instance.

Emilio Jesús Gallego Arias (Nov 05 2021 at 13:27):

That'd be cool! Unfortunately as of today, Coq is limited to one instance per process tho; we hope to lift this limitation, but for now there is too much global state.

Emilio Jesús Gallego Arias (Nov 05 2021 at 13:28):

For tests, I'd just ensure they cancel the stuff, we can also add a special command to serapi that does that

Emilio Jesús Gallego Arias (Nov 05 2021 at 13:28):

the low-level API of Coq has a kind of "run this but don't record the changes" function

Emilio Jesús Gallego Arias (Nov 05 2021 at 13:28):

but this is hard to capture in the original RPC context

Wolf Honore (Nov 05 2021 at 14:43):

FWIW, in Coqtail I have a Coqtop class that spawns one Coq process per instance. Then in the integration tests I just spin up a new instance for every test using a function-scoped fixture. It's definitely not pretty, and maybe wouldn't work so well if you're running hundreds of property tests or something, but it's an option.

Emilio Jesús Gallego Arias (Nov 05 2021 at 14:49):

Indeed @Wolf Honore , that of course works, but in PyCoq / SerAPI is pretty easy to issue a Cancel for a part of document so you can gain quite a bit of speed on tests that may have a lot of context [such as importing large libs]

Last updated: Feb 09 2023 at 02:02 UTC