FS#64460 - Do not force -DUSE_LIB_GMP=1 for configuring Z3.

Attached to Project: Community Packages
Opened by Daniel Kirchner (ekpyron) - Monday, 11 November 2019, 17:50 GMT
Last edited by Felix Yan (felixonmars) - Monday, 07 September 2020, 20:57 GMT
Task Type Feature Request
Category Packages
Status Closed
Assigned To Felix Yan (felixonmars)
Levente Polyak (anthraxx)
Architecture All
Severity Low
Priority Normal
Reported Version
Due in Version Undecided
Due Date Undecided
Percent Complete 100%
Votes 1
Private No

Details

The Z3 PKGBUILD explicitly sets "-DUSE_LIB_GMP=1". The default is *not* to link against GMP.
Why is that? I'm asking because we recently stumbled upon cases, in which Z3 could solve a problem, if *not* linked against GMP, while it failed to solve it, when linked against GMP.
There might, of course, be cases with the opposite behavior, but my question is: what's the reason for not keeping it at the upstream default?
This task depends upon

Closed by  Felix Yan (felixonmars)
Monday, 07 September 2020, 20:57 GMT
Reason for closing:  Implemented
Additional comments about closing:  4.8.8-2
Comment by Felix Yan (felixonmars) - Wednesday, 20 November 2019, 19:09 GMT
Looks like Z3 used to depend on GMP but dropped the need later. Comments in the code suggest that an internal implementation (which is limited in some way) would be used when GMP is not present.

I'll wait for an answer from upstream on the issue you mentioned: https://github.com/Z3Prover/z3/issues/2551#issuecomment-552536486
Comment by Kamil Śliwak (cameel) - Monday, 07 September 2020, 10:56 GMT
The issue listed above has been resolved (not reproducible now) but there's another one that's triggered only when using Z3 with GMP: https://github.com/Z3Prover/z3/issues/4407#issuecomment-663650494
Comment by Leo Alt (leonardoalt) - Monday, 07 September 2020, 11:56 GMT
Well, using or not using GMP is not an issue. z3 might give different answers depending on whether GMP is linked, but that doesn't ultimately make one or the other bad.
I don't think z3 has any open bugs because of the non GMP implementation. I also think it would make sense to not use GMP in this package (same as upstream).

Loading...