search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.49k stars 393 forks source link

Finish GMP removal #827

Open Kha opened 2 years ago

leodemoura commented 2 years ago

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

leodemoura commented 2 years ago

We are looking for volunteers to stress test this feature.

rujialiu commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

Thank you @Kha !