conf-gmp: use pkg-config where available

[mseri]

See #18129 and #22954

I need to test the dependencies in opam list --depends-on conf-gmp before un-drafting

[mseri]

Checked packages:

• bap-std
• class_group_vdf
• comby
• conf-gmp-powm-sec
• conf-mpfr
• gappa
• gmp-ecm
• goblint
• guile
• libsail
• lutin
• mlgmp
• mlgmpidl
• numerix
• polka
• sail
• secp256k1-internal
• yices2
• z3
• zarith

Upper bound needed for

mlgmp, numerix

although they were already broken in systems with non-standard include paths

[artempyanykh]

Hi @mseri ! Just wanted to double-check if I could help somehow here. For the context, I'm interested in getting zarith fixes in as otherwise my team can't simply build our stuff (infer) on M1 MacBooks.

[nberth]

Hi @mseri
I've had similar issues locating weird installation paths for system libraries with mlgmpidl, so I've tried in #23613 an approach where packages like conf-gmp and conf-mpfr define some opam variables that other packages like zarith or mlgmpidl can use to locate the libraries (see https://github.com/ocaml/opam-repository/pull/23613/files#diff-2aa76d47e681a91666af166e62200ce54a0650971fbb9133bf778cf0cf1aeb27R12 for an example usage). For now this attempt makes use of a (slightly hackish) support package ez-conf-lib and does not involve pkg-config, as I've seen some systems where the directories it returns seemed incorrect; I think that feature could still be added with little effort.

[artempyanykh]

Hi @mseri! I see there's an alternative PR for GMP #23613 . Even if it gets merged, we'll still need a patch to zarith to use pkg-config for flag lookup. Is there something I can help with to help push this PR forward?

[mseri]

I need to check all the packages in the comment above, ensure that they link properly and that their reverse dependencies all still work. Once they all have a checkmark, we can undraft this

[mseri]

There is a PR in zarith to use pkg-config for gmp, which will also align it to this PR

[jvillard]

Any chance this could be revived? gmp and zarith cannot be installed on osx with custom Homebrew paths at the moment.

[nberth]

Any chance this could be revived? gmp and zarith cannot be installed on osx with custom Homebrew paths at the moment.

There's been progress on the mlgmpidl side recently. It now uses a distinct "conf" package, named conf-gmp-paths. Customization via user input is not complete yet, but if that does not install properly you may be able to try the hack I suggested here.
I don't know if there is any plan to adapt zarith accordingly yet.

[mseri]

I will try to take some time to continue, but this is completely manual work and takes a lot of time for each package. I am not sure when I can unblock it.

[mseri]

the change to make zarith use pkg-config has been merged in the meantime (ocaml/Zarith#132) and published in zarith 1.13 (release-1.13)

[mseri]

I think I can refresh this PR with the suggestion from @avsm in #24133