Stream: Coq users

Topic: QuickChick anomaly

view this post on Zulip Huỳnh Trần Khanh (Aug 11 2022 at 07:34):

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

view this post on Zulip Michael Soegtrop (Aug 11 2022 at 07:44):

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?

view this post on Zulip Huỳnh Trần Khanh (Aug 11 2022 at 07:52):

That exact version, yeah. And most of the code is lifted from https://github.com/QuickChick/QuickChick/blob/533e009ff40432f16b15c3c4ee95e7cb237863bc/examples/sf/IndProp.v

view this post on Zulip Huỳnh Trần Khanh (Aug 11 2022 at 07:52):

My stuff is from line 24.

view this post on Zulip Huỳnh Trần Khanh (Aug 11 2022 at 07:53):

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.

view this post on Zulip Huỳnh Trần Khanh (Aug 11 2022 at 07:54):

After running Interpret to End in VS Code.

view this post on Zulip Michael Soegtrop (Aug 11 2022 at 08:01):

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)"

view this post on Zulip Michael Soegtrop (Aug 11 2022 at 08:02):

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.

view this post on Zulip Michael Soegtrop (Aug 11 2022 at 08:04):

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.

view this post on Zulip Michael Soegtrop (Aug 11 2022 at 08:05):

On MacOS Quickchick does generally work in VsCoq, but I don't use Derive.

view this post on Zulip Huỳnh Trần Khanh (Aug 11 2022 at 12:53):

Anyway, this seems like a bug. Should I file a bug on the QuickChick repository?

I filed a bug. https://github.com/QuickChick/QuickChick/issues/301

Last updated: Oct 13 2024 at 01:02 UTC