Stream: Coq Platform devs & users

Topic: GMP and Perl now dependencies of Coq


view this post on Zulip Karl Palmskog (Aug 29 2020 at 12:08):

The GMP library is as per merging of PR 11742 now a dependency of Coq. This will likely introduce issues for the next platform, in particular on Windows.

view this post on Zulip Karl Palmskog (Aug 29 2020 at 12:12):

in particular, any compilation of Coq without use of depext for conf-gmp up front will fail.

view this post on Zulip Karl Palmskog (Aug 29 2020 at 12:19):

also, we depend on Perl of all languages now, sigh

view this post on Zulip Karl Palmskog (Aug 29 2020 at 12:33):

... but apparently only in the build phase, even more sigh

view this post on Zulip Enrico Tassi (Aug 29 2020 at 15:01):

What is the issue on windows? The PR did fix the windows build script, AFAIK

view this post on Zulip Enrico Tassi (Aug 29 2020 at 15:05):

About perl... we may not like the language, but to me perl is much much much more safe as a dependency than, say, ocaml.

view this post on Zulip Michael Soegtrop (Aug 29 2020 at 15:10):

The Coq platform anyway depends on GMP (for Gappa).

view this post on Zulip Karl Palmskog (Aug 29 2020 at 15:18):

Enrico Tassi said:

About perl... we may not like the language, but to me perl is much much much more safe as a dependency than, say, ocaml.

There are apparently two different flavors of Perl for Windows, likely incompatible. I guess the Windows installer will have to bundle its own version, or how will it work?

view this post on Zulip Michael Soegtrop (Aug 29 2020 at 15:39):

 I guess the Windows installer will have to bundle its own version, or how will it work?

I hope this dependency is build only. If so, it will use the cygwin supplied perl.

My personal opinion on Perl is that one should replace any use of perl with either python or awk/sed/grep/..., depending on the complexity. What I don't like about perl is that installing even simple text processing packages with cpan can take an hour, since it is difficult to tell it that it shouldn't run a complete test suite for each installation. Furthermore the system dependency management of perl packages is - well non existent. I had much much less issues with pip. Finally I think Perl makes it too easy to write very hard to maintain code. In any long term maintained project in which I used perl, it generated long term much more work than it saved in the first place.

view this post on Zulip Karl Palmskog (Aug 29 2020 at 15:41):

I hope this dependency is build only. If so, it will use the cygwin supplied perl.

Per OPAM, it is indeed build only for zarith:

depends:      "ocaml" "ocamlfind" {build} "conf-gmp" "conf-perl" {build}

Last updated: Jan 30 2023 at 11:03 UTC