lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

Finish GMP removal

Open Kha opened this issue 4 years ago • 2 comments

Kha avatar Nov 26 '21 17:11 Kha

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

leodemoura avatar Jan 20 '22 17:01 leodemoura

We are looking for volunteers to stress test this feature.

leodemoura avatar Jun 01 '22 23:06 leodemoura

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)

rujialiu avatar Aug 19 '23 02:08 rujialiu

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!

Kha avatar Aug 19 '23 12:08 Kha

Thank you @Kha !

rujialiu avatar Aug 20 '23 11:08 rujialiu