You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The error is easily resolved by installing libgmp-dev, as indicated in the list of dependencies.
apt update && apt install -y libgmp-dev
Describe the solution you'd like
An error that clearly points to the possibility of a missing library, since that's likely the problem, and links to the other required dependencies, just in case those are missing too.
Describe alternatives you've considered
The current error is not that terrible, because it does mention libgmp.so, and a quick internet search will probably find out that the problem is a missing package. However, that search also returns results about having the wrong version of libgmp, which could be confusing.
Is your feature request related to a problem? Please describe.
When missing the
libgmp-dev
package, the error is not that clear.Reproduce with:
The error is easily resolved by installing
libgmp-dev
, as indicated in the list of dependencies.Describe the solution you'd like
An error that clearly points to the possibility of a missing library, since that's likely the problem, and links to the other required dependencies, just in case those are missing too.
Describe alternatives you've considered
The current error is not that terrible, because it does mention
libgmp.so
, and a quick internet search will probably find out that the problem is a missing package. However, that search also returns results about having the wrong version oflibgmp
, which could be confusing.Additional context
Inspired by: #1416 #1419 #1535
The text was updated successfully, but these errors were encountered: