2 ms·
> native code compilation (via C code extraction), allowing you to compile all the constructions you can formalize in Lean directly to native code Is that real
by tom_mellior 9y ago
> native code compilation (via C code extraction), allowing you to compile all the constructions you can formalize in Lean directly to native code
Is that really true? What do they do for garbage collection, do they provide their own or use something like the Boehm collector?
As far as I understood, F* also allows C extraction, but only for a subset not including dynamic allocation (or maybe with explicit memory management via effects?).
- cmrx64 9y agoNo, it's not true, it "extracts" (compiles) to C++. <https://github.com/leanprover/lean/pull/1241> https://github.com/leanprover/lean/pull/1241> It's written in Lean itself, as a metaprogram. The code it generates calls into the Lean library ("runtime") for some objects, otherwise uses native types when it can. vm_obj's in Lean are reference counted. There's also in-progress work on an LLVM backend.