Cannot render Coq files with QuickChick invocations

[anton-trunov]

Here is a minimal example:

From QuickChick Require Import QuickChick.
QuickChick (fun _ : bool => true).

This gets stuck with the following error message:

$ alectryon.py --frontend coq+rst --backend webpage quickchick.v -o quickchick.html
Unexpected response: b'QuickChick (fun _ : bool => true)\n'

[cpitclaudel]

Sounds like the output of Quickchick is printed to stdout directly instead of going through Coq's message-printing facilities, I'd raise a bug on the quickchick side. Or maybe quickchick is doing things right and SerAPI is missing that output.

[anton-trunov]

FWIW, the following sertop query

$ rlwrap sertop --printer=human
(Add () "From QuickChick Require Import QuickChick.")
(Add () "QuickChick (fun _ : bool => true).")

results in

(Answer 1 Ack)
(Answer 1
 (Added 3
  ((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1)
   (bol_pos_last 0) (bp 0) (ep 34))
  NewTip))
(Answer 1 Completed)

so it looks like SerAPI processing this just fine.

[anton-trunov]

@cpitclaudel Reported: https://github.com/QuickChick/QuickChick/issues/225. In the meantime: is there a workaround?

[cpitclaudel]

You need to Exec as well to see the issue:

("query0"("Add"()"From QuickChick Require Import QuickChick.\nQuickChick (fun _ : bool => true)."))
("query1"("Exec""2"))
("query2"("Query"(("sid""2"))"EGoals"))
("query3"("Exec""3"))

Then you see the following in the output:

(Answer query3 Ack)
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(ProcessingIn master))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents Processed)))
QuickChecking (fun _ : bool => true)
/home/clement/.opam/coq-8.12/bin/ocamldep.opt -modules QuickChickc98a65.ml > QuickChickc98a65.ml.depends
/home/clement/.opam/coq-8.12/bin/ocamldep.opt -modules QuickChickc98a65.mli > QuickChickc98a65.mli.depends
/home/clement/.opam/coq-8.12/bin/ocamlc.opt -c -w -3 -o QuickChickc98a65.cmi QuickChickc98a65.mli
/home/clement/.opam/coq-8.12/bin/ocamlopt.opt -c -w -3 -o QuickChickc98a65.cmx QuickChickc98a65.ml
/home/clement/.opam/coq-8.12/bin/ocamlopt.opt unix.cmxa QuickChickc98a65.cmx -o QuickChickc98a65.native
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(Message(level Info)(loc())(pp(Pp_string"+++ Passed 10000 tests (0 discards)"))(str"+++ Passed 10000 tests (0 discards)")))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents Processed)))
(Answer query3 Completed)
(Answer EOF Ack)
(Answer EOF Completed)

Notice how the "+++" part is properly handled as a message, while the rest is mixed with the output.

[cpitclaudel]

I added a workaround, but you're in scary territory. Try with --expect-unexpected.

[anton-trunov]

Awesome! Thanks a lot, that worked for my case.