Stream: Coq users

Topic: Software Foundations - QuickChick Introduction.v - error


view this post on Zulip jco (Jun 19 2020 at 13:24):

I am trying to get started with the QuickChick module for software foundations. My opam had issues, so I deleted ~/.opam and reinstalled...though now I'm on coq 8.11.2, which is a potential issue? I'm on a Mac.

When I run make, I get this

W: This Makefile was generated by Coq 8.11.1 W: while the current Coq version is 8.11.2

Not necessarily a sign that there's an issue, given it's just a minor version difference, but I can install 8.11.1 if y'all recommend?

When I try to run "QuickCheck removeP", I get the following

`The following logical axioms were
encountered: semBindOptSizeMonotonicIncl_r semBindOptSizeMonotonicIncl_l.
Having
invalid logical axiom in the environment when extracting may lead to
incorrect or non-terminating ML terms.
[extraction-logical-axiom,extraction]

The identifier Eq__Dec contains __ which is reserved for the extraction
[extraction-reserved-identifier,extraction]`

I tried adding the following to the beginning of the file, but it didn't work.

Set Warnings "-extraction-logical-axiom,extraction". Set Warnings "-extraction-reserved-identifier,extraction".

Any advice? Thanks in advance

view this post on Zulip Enrico Tassi (Jun 19 2020 at 13:31):

WRT the makefile warning you can just regenerate the makefile using coq_makefile (from coq 8.11.2)

view this post on Zulip jco (Jun 19 2020 at 13:45):

Enrico Tassi said:

WRT the makefile warning you can just regenerate the makefile using coq_makefile (from coq 8.11.2)

Ah thank you! I deleted all the .vo* files, the Makefile, then ran coq_makefile *.v > Makefile. It seems to compile normally (without a warning), though the error mentioned above is still present

view this post on Zulip jco (Jun 19 2020 at 13:46):

Ah, hmm, it looks like QuickChick may require Coq 8.8?

view this post on Zulip jco (Jun 19 2020 at 13:46):

hmm though there is a 8.11 branch

view this post on Zulip jco (Jun 19 2020 at 13:46):

I'm not sure if opam is smart enough to make sure that things are compatible, version wise (at least how they were publisehd). I'm assuming yes

view this post on Zulip jco (Jun 19 2020 at 13:49):

Ah! looking through the issue tracker, it looks like it may be an issue with Coq for VIM and QuickChick...hmm!

view this post on Zulip jco (Jun 19 2020 at 13:56):

well it says it doesn't work with CoqIDE, which I mistakenly thought were the bindings that vim uses. Vim uses coqtail, but I think it may be affected by the same issue? hrm

view this post on Zulip Li-yao (Jun 19 2020 at 13:59):

that looks like a warning message you can just ignore

view this post on Zulip Li-yao (Jun 19 2020 at 14:01):

If you've installed it via opam you got the right version

view this post on Zulip jco (Jun 19 2020 at 14:02):

but I do not see any output

view this post on Zulip jco (Jun 19 2020 at 14:03):

that is to say, the QuickCheck command clearly is doing something (because it takes maybe half a second to a second to return), but I don't see output from the command

view this post on Zulip Li-yao (Jun 19 2020 at 14:08):

OK I see, that's indeed probably something with coqtail.

view this post on Zulip jco (Jun 19 2020 at 14:08):

I guess I have no choice but to use emacs. I guess proof general is the preferred optoin there?

view this post on Zulip Kenji Maillard (Jun 19 2020 at 14:10):

with emacs you can also use spacemacs and the coq layer to recover some vim bindings;
otherwise vscode is also an option these days

view this post on Zulip Wolf Honore (Jun 19 2020 at 14:11):

Would you mind opening an issue for coqtail or linking the relevant quickcheck issue? I'd like to take a look and fix it if possible

view this post on Zulip jco (Jun 19 2020 at 14:12):

Wolf Honore said:

Would you mind opening an issue for coqtail or linking the relevant quickcheck issue? I'd like to take a look and fix it if possible

But of course!

view this post on Zulip Li-yao (Jun 19 2020 at 14:12):

@Wolf Honore minimal example

Require Import QuickChick.QuickChick.
Require Import Arith.

QuickChick (fun n => Nat.eqb n n).

doesn't print anything when it should.

view this post on Zulip Wolf Honore (Jun 19 2020 at 14:14):

Thanks

view this post on Zulip jco (Jun 19 2020 at 14:15):

https://github.com/whonore/Coqtail/issues/99

view this post on Zulip jco (Jun 19 2020 at 14:21):

Btw want to compliment you on the plugin. It is simple and works nicely -- that's why I like vim :) emacs is more of a lifestyle...

view this post on Zulip Wolf Honore (Jun 19 2020 at 14:25):

jco said:

Btw want to compliment you on the plugin. It is simple and works nicely -- that's why I like vim :) emacs is more of a lifestyle...

Thank you for the kind words. I'm glad you find it useful.


Last updated: Jan 29 2023 at 05:03 UTC