GMP in Lean 4

Stream: lean4

[Matej Penciak]

I've looked around the lean4 codebase and Zulip and I've been seeing a bunch of mixed messages, so I just wanted to clarify.

If I get my Lean toolchain from elan (not building from source with any compiler flags or anything), and I try to extract the mpz from a Nat in some externally linked C code, will I be getting a GMP mpz or the home-brewed Lean mpz?

[Gabriel Ebner]

This depends on your platform. On macOS/aarch64 and Windows, you're going to get the homegrown one. And otherwise, gmp.