extract to c

Stream: general

[Quinn]

How hard would it be to extract to c from lean4, these days? I didn't find anything on google and the discussions in the zulip search were all very old.

[Quinn]

https://lean-lang.org/lean4/doc/dev/ffi.html hmm i'm having trouble reading the examples given here to determine if c source is generated

[Adam Topaz]

Lean4 compiles to c

[Adam Topaz]

If you build your project, then look inside the .lake folder, you should see the output

[Tomas Skrivan]

In case you are interested in running Lean code inside of another program have a look at the reverse-ffi example https://github.com/leanprover/lean4/tree/4508692c7177145382e3acf2a785a80ce8a27e6a/src/lake/examples/reverse-ffi