Zulip Chat Archive

Stream: general

Topic: What is leanc and how to use it

kana (Sep 28 2021 at 12:40):

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 (Sep 28 2021 at 16:11):

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 (Sep 28 2021 at 16:25):

Does this belong in #lean4?

Christian Pehle (Sep 28 2021 at 17:19):

Eric Wieser said:

Does this belong in #lean4?


Notification Bot (Sep 29 2021 at 00:14):

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

Last updated: Aug 03 2023 at 10:10 UTC