Having problems getting QuickChick to work with Emacs/ProofGeneral and VSCoq

[EliasC]

I downloaded the latest version of the QuickCheck chapter of Software Foundations and I'm having trouble getting it to work:

• When running in Emacs with ProofGeneral, the proof process hangs when running a QuickChick command (I interrupt it after a minute or so). A Sample command fails with the message

  Could not compile test program: /var/folders/zn/0d2q2m9916j_m0jvc95vw0t00000gn/T/QuickChick/203020_6c66b1/.QuickChick6b41ec.ml
  
  Build stdout:
  + ocamlfind ocamlopt -c -w -3 -package zarith -o QuickChick6b41ec.cmx QuickChick6b41ec.ml
  /var/folders/zn/0d2q2m9916j_m0jvc95vw0t00000gn/T/camlasm62caff.s:381:2: error: unknown use of instruction mnemonic without a size suffix
   mov x0, x1
   ^
  [~5000 similar lines omitted]
  
  File "QuickChick6b41ec.ml", line 1:
  Error: Assembler error, input left in file /var/folders/zn/0d2q2m9916j_m0jvc95vw0t00000gn/T/camlasm62caff.s
  Command exited with code 2.

  I have seen similar errors when compiling OCaml code from inside Emacs, so this might be related.

• In VSCode with VSCoq, commands seem to run but I am not able to see the output anywhere. The documentation mentions an "info" tab in the output pane, but I could not find this.

I am able to use QuickChick successfully in CoqIDE, but either of the two choices above would be preferrable. When compiling the source files in the chapter in a terminal with the Makefile, everything builds and prints correct output from the QuickCheck commands, but the file QuickChickInterface.v fails with the message:

File "./QuickChickInterface.v", line 190, characters 15-22:
Error: The reference OrdType was not found in the current environment.

When troubleshooting I cloned this GitHub repo. Running make also gives an error message related to QuickChickInterface.v:

coqc -R src QuickChick -I plugin QuickChickInterface.v
Error: Can't find file ./QuickChickInterface.v

As far as I can see that file is in the doc directory, which does not seem to be in the include path.

Finally, running the quickChick command line tool immediately fails with

Parse error when reading file: ./QuickChickInterface.v
Fatal error: exception Dune__exe__QuickChickToolParser.MenhirBasics.Error

I am guessing this has to do with the same errors from compiling the file.

I am running an M1 Mac with MacOS 14.2.1, Coq 8.19.1 and QuickChick 2.0.3 (both built from opam). I have also tried with Coq versions 8.18.0 and 8.17.0.

Any help is appreciated!

[liyishuai]

368 should fix the documentation check failure.

@lemonidas Some insights into the Emacs problem?

[lemonidas]

I'll try to see if I can replicate this tomorrow, hopefully it's not an M1 thing.

[EliasC]

@lemonidas FWIW, QuickChick started working for me in Proof General after updating Emacs to 23.9. I still can't see any output when using VSCoq, but that is not a show stopper for me personally.