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.
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.
For testing whitin the same coq isntance, I'd recommend using
Cancel to undo the added sentences
This will restore the initial state reliably except in the case of loading of ML plugins [which is very rare]
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
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.
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.
For tests, I'd just ensure they cancel the stuff, we can also add a special command to serapi that does that
the low-level API of Coq has a kind of "run this but don't record the changes" function
but this is hard to capture in the original RPC context
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.
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: May 20 2022 at 10:03 UTC