Michael Soegtrop (Apr 04 2022 at 05:55): Michael Soegtrop (Apr 04 2022 at 05:55):Over the weekend I fixed a few Windows issues, notably Ott and Quickchick - all just minor issues. But a big thing which remains - for all installers, macOS, Windows and snap, is that OCaml is not included. QuickChick requires it and one could also think about enabling native compute at least for snap.
Originally I did include OCaml in the Windows installers - it was removed for size reasons, but I guess meanwhile this doesn't matter much any more. But I guess adding it back to all installers - likely unifying the file selectors on the way - would likely take me one or two weeks to get through CI. Is it worth it?
Otherwise 2022.03 is ready (except that I think about adding Fiat Crypto, which got opam packages end of last week and some minor adjustments in the main readme).
Please use upvote for "include OCaml + delay" and downvote for "not include OCaml + no delay".
Michael Soegtrop (Apr 04 2022 at 06:02):@Benjamin Pierce @Leonidas Lampropoulos @Li-yao : what is your opinion on this? Is QuickChick used in courses (there is a SF course on it)? I am a bit astonished that I get zero feedback on the QuickChick issues in Coq Platform. But at least with the recent fixes by @Li-yao and me it now does work on all platforms in "compile from sources" mode. But it does work in non of the installers, since none of them installs OCaml.
Michael Soegtrop (Apr 04 2022 at 06:02):Btw.: did you think about using vm-compute and native-compute instead of compiling OCaml code? I would think for students vm-compute would be fast enough and for the professional users native compute should not be slower than compiled OCaml code.
Théo Zimmermann (Apr 04 2022 at 12:41):Why not including OCaml in the binary installers, but in a subsequent release IMHO.
Li-yao (Apr 04 2022 at 13:47):I also don't think it's worth delaying a release, especially when there is a working option (from sources).
It would indeed be nice to run QC using vm-compute, and I have some work-in-progress in that direction, but it may take a month or two to get it in a working state. But extraction will still be useful to do impure stuff (file system, networking...)
Karl Palmskog (Apr 04 2022 at 13:50):I'm strongly in favor of making OCaml itself a first-class citizen in future Platform releases (of binary installers). In my view, this needs to be done sooner or later, since we expect Dune to become the primary build system for Coq projects, and thus to Platform users [and Dune is unlikely to work without OCaml anytime soon]
Li-yao (Apr 04 2022 at 14:57):Do you really need OCaml to build a Coq-only project?
Karl Palmskog (Apr 04 2022 at 15:00):Dune doesn't work without OCaml. If we want to use Dune to build a Coq-only project, we currently thus need OCaml. coq_makefile will work fine without OCaml, but it's expected to become the legacy option to build Coq-only projects.
Michael Soegtrop (Apr 04 2022 at 15:37):I still wonder why dune would need OCaml ...
Théo Zimmermann (Apr 04 2022 at 15:57):I bet the requirement is artificial, but the check is there.
Michael Soegtrop (Apr 04 2022 at 17:08):@Emilio Jesús Gallego Arias : can you explain why dune requires OCaml to run - I darkly remember that we had this discussion before but I don't remember the answer, sorry.
Leonidas Lampropoulos (Apr 04 2022 at 17:50):I also agree with Li-yao. Not worth delaying a release over something that has a workaround, but I've always thought of OCaml as a de facto dependency.
On the topic of QuickChick in courses, we use SF volume 4 heavily at UMD, but all Windows students just use WSL as it's very easy to use and everything works just like in the Unix-based systems.
Finally, we don't only use OCaml for performance in QuickChick, but we currently rely on it for things like randomness/io. I'm not at all opposed to a vm_compute version of executing QuickChick properties, but it sounds like a significant engineering effort to work correctly.
Michael Soegtrop (Apr 04 2022 at 18:02):@Leonidas Lampropoulos : thanks for the confirmation!
Please note that the Linux Snap binary installation of Coq Platform doesn't work either - it also does not include OCaml. All binary installers (macOS, Windows, Snap) are identical in that. The "from sources" method works on all platforms (on Windows also without WSL2 - just run coq_platform_make_windows.bat, answer the questions and wait 2 hours).
As I said, I plan to fix this in the next release.
Emilio Jesús Gallego Arias (Apr 04 2022 at 18:08):@Michael Soegtrop that's just a dune bug, as it does some init too early; there was a PR trying to fix it, but I am not sure it has been merged yet
Emilio Jesús Gallego Arias (Apr 04 2022 at 18:09):Please someone check the dune bug tracker, I'm a bit busy today
Last updated: Apr 19 2024 at 12:02 UTC