jco (Jun 19 2020 at 13:24): 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
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)
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
jco (Jun 19 2020 at 13:46):Ah, hmm, it looks like QuickChick may require Coq 8.8?
jco (Jun 19 2020 at 13:46):hmm though there is a 8.11 branch
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
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!
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
Li-yao (Jun 19 2020 at 13:59):that looks like a warning message you can just ignore
Li-yao (Jun 19 2020 at 14:01):If you've installed it via opam you got the right version
jco (Jun 19 2020 at 14:02):but I do not see any output
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
Li-yao (Jun 19 2020 at 14:08):OK I see, that's indeed probably something with coqtail.
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?
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
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
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!
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.
Wolf Honore (Jun 19 2020 at 14:14):Thanks
jco (Jun 19 2020 at 14:15):https://github.com/whonore/Coqtail/issues/99
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...
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: Oct 13 2024 at 01:02 UTC