Stream: jsCoq

Topic: Quickchick


view this post on Zulip Catherine Dubois (Feb 24 2022 at 18:38):

Hi!
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?

view this post on Zulip Li-yao (Feb 24 2022 at 18:47):

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.

view this post on Zulip Enrico Tassi (Feb 24 2022 at 20:45):

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)

view this post on Zulip Catherine Dubois (Feb 25 2022 at 07:30):

Thanks for this solution that however requires an installation.

view this post on Zulip Enrico Tassi (Feb 25 2022 at 09:45):

Did it work? Which OS did you use? (if it does not work I'll open an issue on the platform)

view this post on Zulip Michael Soegtrop (Feb 25 2022 at 13:47):

@Catherine Dubois : do you have technical problems with an installation or don't you like executable installers - say would you prefer ZIPs?

view this post on Zulip Shachar Itzhaky (Mar 06 2022 at 09:15):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 09:44):

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?

view this post on Zulip Shachar Itzhaky (Mar 07 2022 at 10:03):

I am not aware of one but probably we can just grep for Unix in their source? :) It's not too large

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 10:04):

Hopefully I can look into this soon, and also on the extension of the Require API we need

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 10:05):

@Ramkumar Ramachandra and I would like to have something similar to handle Require in a special way

view this post on Zulip Karl Palmskog (Mar 07 2022 at 10:05):

you may want to check with Michael Soegtrop, who I believe investigated QuickChick on Windows at some point

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 10:06):

That's a great point @Karl Palmskog , we are actually interested on doing this API to improve plugin portability

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 10:06):

cc @Michael Soegtrop

view this post on Zulip Michael Soegtrop (Mar 07 2022 at 11:29):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2022 at 11:48):

We do have access to ocamlc from jsCoq, at least in some way, this is how the try ocaml plaftforms works

view this post on Zulip Shachar Itzhaky (Mar 07 2022 at 17:22):

ocamlc runs as is on ocaml-wasm. I assume it can be compiled to JS as well?

view this post on Zulip Shachar Itzhaky (Mar 07 2022 at 17:26):

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

view this post on Zulip Bas Spitters (Aug 03 2022 at 08:34):

This thread seems hopeful. Are there any obstacles on building the QC book here: https://coq.vercel.app/ext/sf/ ?
@Shachar Itzhaky

view this post on Zulip Bas Spitters (Aug 03 2022 at 08:35):

Not important to me, but are there obstacles to building the VST book?

view this post on Zulip Shachar Itzhaky (Aug 03 2022 at 13:30):

It's pretty straightforward although I have not quite documented the process. I can explain to whoever is interested.

view this post on Zulip Bas Spitters (Aug 03 2022 at 13:33):

@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?

view this post on Zulip Shachar Itzhaky (Aug 03 2022 at 15:10):

Oh sorry I missed the fact that you mentioned QC there. I thought you were talking about building one's own copy of SF.

view this post on Zulip Shachar Itzhaky (Aug 03 2022 at 15:12):

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.

view this post on Zulip Shachar Itzhaky (Aug 03 2022 at 15:13):

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.

view this post on Zulip Bas Spitters (Aug 04 2022 at 09:22):

Thanks. I can just run the QC part on my local machine, if needed. It's just that things look/work nice with jscoq

view this post on Zulip Bas Spitters (Sep 05 2022 at 13:11):

@Leonidas Lampropoulos @Li-yao @Yishuai Li I see the QC book now depends on a beta release for 2.0
https://github.com/QuickChick/QuickChick/releases/tag/v.2.0%2Bbeta

This release is not in opam, platform or nix. Do you plan to make something more permanent available (in the somewhat near future) ?

view this post on Zulip Li-yao (Sep 05 2022 at 13:54):

Ah, maybe we should add it to the dev repository while we work out a proper release.

view this post on Zulip Karl Palmskog (Sep 05 2022 at 13:57):

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 extra-dev

view this post on Zulip Leonidas Lampropoulos (Sep 05 2022 at 16:05):

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)

view this post on Zulip Bas Spitters (Sep 23 2022 at 11:43):

@Leonidas Lampropoulos Did you happen to make any progress on this?

view this post on Zulip Bas Spitters (Oct 19 2022 at 14:37):

@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.

view this post on Zulip Bas Spitters (Nov 19 2022 at 16:51):

@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.

view this post on Zulip Bas Spitters (Apr 18 2023 at 06:52):

Congrats on the v2 release . @Shachar Itzhaky is this everything you need for inclusion in jscoq?

view this post on Zulip Shachar Itzhaky (Apr 18 2023 at 18:30):

Hi! I think what mostly blocked me and still is that I don't have a grasp of the use cases of QuickChick since I myself have never used it and did not study the QC volume of SF. I see that examples/Tutorial.v is no longer present.
I can try walking through the QC volume myself. The problem remains that for some tasks, ocamlc is required. Is there any significant part of it that can be made to work without it?

view this post on Zulip Karl Palmskog (Apr 18 2023 at 18:32):

I think the inductive type instance generator is something nontrivial that works in pure Coq? We may want to summon @Michael Soegtrop for advice. (I think he has some smoke test in the Platform?)

view this post on Zulip Michael Soegtrop (Apr 20 2023 at 12:17):

I can't say much on the technicalities of QuickChick. What I can say is that since a while it is enabled also on Windows (where we don't have ocamlc) and the Smoke test kit runs through. So it does "something". What parts depend on ocamlc I can't tell, but I could test my typical use cases.

view this post on Zulip Shachar Itzhaky (Apr 20 2023 at 14:09):

ok thanks for this point of view @Michael Soegtrop . Can we run the smoke tests on our jsCoq version? How do we do that?

view this post on Zulip Michael Soegtrop (Apr 21 2023 at 08:55):

@Shachar Itzhaky : you mean run the smoke test for QuickChick or the whole smoke test kit? You can download the smoke test kits for various versions here : https://github.com/coq/platform/releases (don't forget to click on "show all assets").

But please mind that the purpose of the smoke test kit is mostly to check if something has been properly installed - it is not that much of a functional test, but this depends.

view this post on Zulip Shachar Itzhaky (Apr 21 2023 at 12:48):

ok, it is something at least. can you suggest something more comprehensive, perhaps from the examples directory, that would not require ocamlc?

view this post on Zulip Michael Soegtrop (Apr 24 2023 at 07:26):

Let me do some tests ...

view this post on Zulip Michael Soegtrop (Apr 26 2023 at 12:23):

Sorry busy - scheduled for tomorrow.

view this post on Zulip Michael Soegtrop (Apr 28 2023 at 11:38):

@Shachar Itzhaky I did some tests. Indeed Quickchick requires for all functionality ocamlc - the smoke test for QuickChick is actually disabled. Sorry for the confusion. There was once an issue on Windows that it did not even work when ocamlc was available (in "compile from sources mode") and this has been fixed - I just remembered this as "QuickChick has been fixed on Windows".

view this post on Zulip Michael Soegtrop (Apr 28 2023 at 11:39):

It might make sense to ask the team if they don't think about moving to Coq VM code - it should not be that much slower. A while back they said they consider to switch.

view this post on Zulip Shachar Itzhaky (Apr 28 2023 at 11:39):

that is one option

view this post on Zulip Shachar Itzhaky (Apr 28 2023 at 11:39):

another would be to make ocamlc available in wasm. This has been done before.

view this post on Zulip Shachar Itzhaky (Apr 28 2023 at 11:40):

need to see that I can reassemble the pieces.

view this post on Zulip Michael Soegtrop (Apr 28 2023 at 11:41):

It would be interesting to see how native compute to WASM compares speed wise to Coq byte code VM.

view this post on Zulip Bas Spitters (Jun 19 2023 at 15:38):

@Shachar Itzhaky Any progress on this. It's an interesting topic.

view this post on Zulip Shachar Itzhaky (Jun 21 2023 at 14:03):

Hopefully I will have time this summer to peek into the ocamlc issue. The previous venture revealed that there is not much to do with QuickChick if you don't have ocamlc. So we need to revisit this.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2023 at 14:11):

@Shachar Itzhaky , @Gabriel Scherer was working on having the OCaml compiler more usable as a JIT, I actually looked into that myself, but found the code too tied to the FS to dare to go ahead and change. I'm unsure what the status of that is as of today.

WASM envs may be a too heavy to maintain for a complete distribution, unless they start to become more POSIX, but it seems that will take time right

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2023 at 14:11):

?

view this post on Zulip Shachar Itzhaky (Jun 21 2023 at 14:12):

I have a version that does work on WASM, I just need to see that it did not rot

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2023 at 14:14):

My worry is more about the process primitives (wait / excevp) etc... working properly / being easy to access

view this post on Zulip Shachar Itzhaky (Jun 21 2023 at 14:16):

I have support for those in wasi-kernel. Also WASIX is an emerging POSIX env for WASM that we can try. It relies on asyncify for blocking syscalls which is a bit clunky but we should check it out

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2023 at 14:19):

I saw some trouble about WASIX so I was indeed fearing that.

JIT is used now by Ltac2 Compiler, QuickChick, and Native, I think we should introduce a proper API in Coq cc @Gaëtan Gilbert


Last updated: Jun 25 2024 at 15:02 UTC