The bulk of this code is from an example file in the QuickChick repository. I only added a conjecture. When I try to check this conjecture, I get an "anomaly". Is this a real bug in QuickChick? Or it's just me doing something seriously wrong? https://gist.github.com/huynhtrankhanh/79662bb3c74ee2cc6143949583205e7b
With Coq Platform 2022.04.1 and Coq 8.15 I don't get over the
Derive SizedProofEqs for (fun n => ev n)..
Which version did you use?
That exact version, yeah. And most of the code is lifted from https://github.com/QuickChick/QuickChick/blob/533e009ff40432f16b15c3c4ee95e7cb237863bc/examples/sf/IndProp.v
My stuff is from line 24.
I wouldn't say that I don't get over the line you mentioned, but I do see red lines under line 19 and 20.
After running Interpret to End in VS Code.
I tried it in good old CoqIDE, and it throws an error on this line (and on any consecutive Derive line if I remove the second).
Then without the derive lines I get a usual QuickChick error.
QuickChecking conditional_prop_example Unable to satisfy the following constraints: ?arg_2 : "Checkable (forall x y : nat, x = y + y -> ev x)"
It would be nice if you could check if CoqIDE and VsCoq show different behavior here and in case report this at VsCoq. CoqIDE (or coqtop) is the reference.
Quickchick is a rather complicated plugin and one can't exclude that it doesn't work as intended in VsCoq. E.g. it depends on the PATH and things like that, which are heavily manipulated by VsCode.
On MacOS Quickchick does generally work in VsCoq, but I don't use Derive.
Anyway, this seems like a bug. Should I file a bug on the QuickChick repository?
Last updated: Jan 27 2023 at 01:03 UTC