What is leanc and how to use it

Stream: general

[kana]

Lean comes with leanc binary (when installed via elan), but I can't find any documentation about this leanc and I can't understand what is it and how to use it. I tried to use leanc on lean files, but it seems that it is not acceptable.

Is it just an alias to clang?

[Christian Pehle]

It is a wrapper around (currently C++) compiler, which passes in the correct linker flags and libraries so that one can compile c output of the lean executable without additional flags (provided one only depends on the default libraries Lean, Std and Init.

[Eric Wieser]

Does this belong in #lean4?

[Christian Pehle]

Eric Wieser said:

Does this belong in #lean4?

probably

[Notification Bot]

This topic was moved by Scott Morrison to #lean4 > What is leanc and how to use it