Finish GMP removal

[Kha]

No description provided.

[leodemoura]

Update: we have an option for building Lean without GMP. We want to fuzzy it before making it the default.

[leodemoura]

We are looking for volunteers to stress test this feature.

[rujialiu]

May I ask what's the current state? Is it the defult now or do you still need stress testing? I'm planning to evaluate lean4 to do some general-purpose programming. Big integers are not need for many programming tasks, and even it's required, libbf is a very attractive alternative which is fast enough in most cases, lightweight and commercial friendly (BTW: I've successfully replaced GMP with libbf in my own fork of Idris2)

[Kha]

We have already disabled GMP in the macOS ARM and Windows releases for technical reasons and no issues were reported about them so far, but further testing would be appreciated!

[rujialiu]

Thank you @Kha !