Quickchick perl script hack failed

[4ever2]

Quickchick installed with Coq Platform 2021.02.0 64 bit windows installer fails executing sample on any generator e.g. Sample (choose (0,10)) with the following error

perl script hack failed. Report: perl -i -p0e 's/type int =\s*int/type tmptmptmp = int\ntype int = tmptmptmp/sg' C:\Users\E\AppData\Local\Temp\QuickChick\140434\QuickChick01bca8.ml

After manually installing perl it still doesn't work but instead fails with the error Could not compile test program

[MSoegtropIMC]

Thanks for reporting and sorry for the long delay.

Can you tell if it makes a difference if Coq Platform is installed with the Windows installer or compiled from sources using the scripts? I am pretty sure the installer does not install perl and I was not aware that QuickChick requires perl.

[MSoegtropIMC]

Please tell precisely what you try to run (input files, command line, ...).

There are smoke tests files for QuickChick and these do run fine, so I don't know what to test.

[spitters]

The students mention it shows up in this line. I am not sure entirely about their setup, but removing perl should solve the issues. https://github.com/DeepSpec/sfdev/blob/master/qc/QC.v#L324

[FrederikVigen]

@MSoegtropIMC If it is any help we get exactly the same error on JsCoq which should be a standardized system

[MSoegtropIMC]

@spitters : I don't have access to the sfdev repo. Can you point me to an equivalent line on the SF public repo?

[spitters]

https://github.com/DeepSpec/sf/blob/master/qc-current/QC.v#L278

On Thu, Dec 9, 2021 at 5:25 PM MSoegtropIMC @.***> wrote:

@spitters https://github.com/spitters : I don't have access to the sfdev repo. Can you point me to an equivalent line on the SF public repo?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/coq/platform/issues/95#issuecomment-990009025, or unsubscribe https://github.com/notifications/unsubscribe-auth/AABTNTTWURNULNCWPISQDXLUQDJ55ANCNFSM4ZXIFAXA . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

[MSoegtropIMC]

Thanks, I will have a look.

[MSoegtropIMC]

I would say this is more of a long term project. As it looks QuickChick requires an OCaml compiler, which is not available with the installed Coq Platform. It will take a while until OCaml on Windows is sufficiently cleaned up to make this possible (maybe end of this year).

What looks more feasible would be to run it with a compiled from sources Coq Platform on Windows. I will work with the QuickChick team on this.

[MSoegtropIMC]

See https://github.com/QuickChick/QuickChick/issues/269

[MSoegtropIMC]

This has been fixed upstream.

Please note that in the 2022.04 release QuickChick only works with "compile from sources" because it requires OCaml.