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
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.
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: Feb 09 2023 at 02:02 UTC