I'm trying to use Quickchick with JsCoq through https://coq.vercel.app/scratchpad.html.
(jsCoq (0.14.2), Coq 8.14.1/81400
OCaml 4.12.0, Js_of_ocaml 3.11.0)
I got the following error when executing sampling in the simple example below:
perl script hack failed. Report: perl -i -p0e 's/type int =\s*int/type tmptmptmp = int\ntype int = tmptmptmp/sg' /tmp/QuickChick/192814/QuickChicke5d463.ml
Inductive mt : Set :=
| v : mt
| l : mt -> mt.
From QuickChick Require Import QuickChick.
Derive (Arbitrary, Show) for mt.
Definition g_mt n : G mt := @arbitrarySized _ GenSizedmt n.
Sample (g_mt 3).
Could you help me?
I guess the problem is that perl doesn't exist in jscoq, so that QuickChick just won't work at the moment. jscoq needs to upgrade QuickChick, and even after that there might be further issues.
If you want an easy way to evaluate quickchick you can use one of the coq plqtform installers here: https://github.com/coq/platform/releases/tag/2022.01.0 (they do include it)
Thanks for this solution that however requires an installation.
Did it work? Which OS did you use? (if it does not work I'll open an issue on the platform)
@Catherine Dubois : do you have technical problems with an installation or don't you like executable installers - say would you prefer ZIPs?
Yes, sorry; we have a problem with QuickChick; we can compile it with jsCoq but it relies on having a Unix environment and these requirements are currently missing so it is unusable atm.
We can extend Coq's plugin API so we can properly handle that, does the quickchick people have a spec of what their unix access needs are?
I am not aware of one but probably we can just grep for Unix in their source? :) It's not too large
Hopefully I can look into this soon, and also on the extension of the Require API we need
@Ramkumar Ramachandra and I would like to have something similar to handle Require in a special way
you may want to check with Michael Soegtrop, who I believe investigated QuickChick on Windows at some point
That's a great point @Karl Palmskog , we are actually interested on doing this API to improve plugin portability
cc @Michael Soegtrop
Things might have improved meanwhile (see https://github.com/QuickChick/QuickChick/issues/269), but afaik (might be wrong) QuickChick still requires ocamlc at run time. I would suggest you create an issue at QuickChick to discuss the jsCoq issues.
We do have access to ocamlc from jsCoq, at least in some way, this is how the try ocaml plaftforms works
ocamlc runs as is on ocaml-wasm. I assume it can be compiled to JS as well?
the bottleneck is having the ocaml stdlib as well. I have a package here that used to work: https://www.npmjs.com/package/@ocaml-wasm/4.12--base
This thread seems hopeful. Are there any obstacles on building the QC book here: https://coq.vercel.app/ext/sf/ ?
Not important to me, but are there obstacles to building the VST book?
It's pretty straightforward although I have not quite documented the process. I can explain to whoever is interested.
@Shachar Itzhaky would it be possible for you to do it and to host the QC book at the same place as the other books?
https://coq.vercel.app/ext/sf/ I think that's the most logical location, isn't it?
Oh sorry I missed the fact that you mentioned QC there. I thought you were talking about building one's own copy of SF.
Unfortunately QuickChick does not quite work in jsCoq at the moment; the main problem is that the QuickChick plugin runs extraction and then invokes
ocamlc. So we will have to set up an environment that is capable of running
ocamlc in the browser. This is doable (in fact it has been done already as a proof-of-concept), but requires some careful integration.
As for VST, I am personally interested in having VST as one of our affiliated libraries. Once we have it there would not be a problem to compile the VST book as well. That's (probably?) easier than QC but still requires some time investment as any library that we wish to support.
Thanks. I can just run the QC part on my local machine, if needed. It's just that things look/work nice with jscoq
@Leonidas Lampropoulos @Li-yao @Yishuai Li I see the QC book now depends on a beta release for 2.0
This release is not in opam, platform or nix. Do you plan to make something more permanent available (in the somewhat near future) ?
Ah, maybe we should add it to the dev repository while we work out a proper release.
does it only work with Coq 8.16? Or 8.15? If the latter, feel free to add to regular
released repository. Not many people know about or know how to use dev repos like
I'm cleaning up a few more things this week, and then we should be in shape to make a push for opam (will just need to fix the CI mess, as it will not be backwards compatible with Coq < 8.15 I think)
@Leonidas Lampropoulos Did you happen to make any progress on this?
@Li-yao @Leonidas Lampropoulos Is there any progress on this, I'd like to use the QC book in my teaching in a couple of weeks.
If possible it would be nice to be able to use jscoq.
@Li-yao @Leonidas Lampropoulos I'll start teaching QC on Monday. I'm sorry this is stalled. Hope we can get something to work for next year.
Last updated: Jan 31 2023 at 10:01 UTC