`leanc` does not use internal flags when `LEAN_CC` is set even if it is set to the bundled compiler

[tydeu]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

If LEAN_CC is set, leanc will not apply its internal flags, even LEAN_CC is set to the bundled compiler.

https://github.com/leanprover/lean4/blob/2061c9bbea847afd6cd301381c5fb239fb21062f/src/Leanc.lean#L43-L47

Steps to Reproduce

From leanprover/lake#93, setting precompileModules to true produces the following LSP error:

`/home/xubaiw/.elan/toolchains/leanprover--lean4---nightly-2022-07-03/bin/lake print-paths Init Lean Foo` failed:

stderr:
info: > LEAN_PATH=./build/lib LD_LIBRARY_PATH=/home/xubaiw/.elan/toolchains/leanprover--lean4---nightly-2022-07-03/lib:./build/lib /home/xubaiw/.elan/toolchains/leanprover--lean4---nightly-2022-07-03/bin/lean ./././Foo.lean -R ././. -o ./build/lib/Foo.olean -i ./build/lib/Foo.ilean -c ./build/ir/Foo.c
info: > /home/xubaiw/.elan/toolchains/leanprover--lean4---nightly-2022-07-03/bin/leanc -c -o ./build/ir/Foo.o ./build/ir/Foo.c -O3 -DNDEBUG
error: stderr:
In file included from ./build/ir/Foo.c:4:
/home/xubaiw/.elan/toolchains/leanprover--lean4---nightly-2022-07-03/include/lean/lean.h:8:10: fatal error: 'stddef.h' file not found
#include <stddef.h>
         ^~~~~~~~~~
1 error generated.
error: external command /home/xubaiw/.elan/toolchains/leanprover--lean4---nightly-2022-07-03/bin/leanc exited with status 1
error: build failed

This is due to Lake setting LEAN_CC to the compiler it discovers (which, generally, is the bundled clang compiler) when it invokes the Lean server via lean --server (see Lake's serve method for details).

Expected behavior:

leanc to apply its internal flags if LEAN_CC points to the bundled compiler.

Actual behavior:

leanc breaks if LEAN_CC is pointed to the bundled compiler because it does not apply the necessary flags.

Reproduces how often:

Always.

Versions

Windows 20H2 Lean (version 4.0.0-nightly-2022-07-03, commit 7326c817d22e, Release) Lake version 3.2.0

Additional Information

As noted above, this is one of the issues behind leanprover/lake#93.

[Kha]

This is due to Lake setting LEAN_CC to the compiler it discovers

But why would it do that? LEAN_CC is intended to be "the C compiler used for compiling Lean-produced C files". Any other C files should be compiled with the standard CC (which Lake may set instead) in my opinion.

[Kha]

It bears repeating that leanc is an implementation detail that is explicitly not intended as a general-purpose C compiler (in particular as it lacks even the basic suite of C standard headers). But I also understand that it's currently the easiest solution for interfacing with C signatures that our FFI cannot handle yet, so I'm not fundamentally opposed to its use in that way until FFI is dramatically improved.

[gebner]

LEAN_CC is intended to be "the C compiler used for compiling Lean-produced C files".

How is LEAN_CC actually intended to be used? I've never been able to make it work. (Except in nixpkgs, but that only works because you added a wrapper around leanc.) This is what it prints on Ubuntu:

LEAN_CC=gcc lake build
> /root/.elan/toolchains/leanprover--lean4---nightly-2022-07-05/bin/leanc -o ./build/bin/a ./build/ir/Main.o ./build/ir/A.o
error: stderr:
/usr/bin/ld: cannot find -lc++abi: No such file or directory
collect2: error: ld returned 1 exit status
error: external command /root/.elan/toolchains/leanprover--lean4---nightly-2022-07-05/bin/leanc exited with status 1
error: build failed

[Kha]

@gebner Ah, I can't say that customizing LEAN_CC is really supported either! You probably need at least -L <lean-sysroot>/lib as in the Nixpkgs leanc wrapper, which we could do by default, but at this point LEAN_CC mostly just exists for the benefit of bootstrapping and Nixpkgs.

[Kha]

In short, it is very unclear to me if and how the our custom libc, headers, runtime, ... should be fed to different compilers across different systems, and I'm just glad that it works at all when using the bundled compiler.

[tydeu]

@Kha

This is due to Lake setting LEAN_CC to the compiler it discovers

But why would it do that? LEAN_CC is intended to be "the C compiler used for compiling Lean-produced C files". Any other C files should be compiled with the standard CC (which Lake may set instead) in my opinion.

The logic here is that Lake should forward its configured environment to the instances it spawns. So, if Lake is configured with a given LEAN_CC (either by default, by am environment variable, or manually by CLI options or code), it should pass that to the processes it spawns as their LEAN_CC (to prevent toolchain clashes)- -- the same way it does with LEAN_SYSROOT, LEAN_AR, LEAN_PATH, LAKE, etc.

However, the "by default" case breaks this because, while Lean can correctly find the bundled compiler, passing the bundled compiler via LEAN_CC does not produce the same result as if it was unset. Currently, to make the setup work, LEAN_CC would require special casing to note that, if the configured compiler is the bundled one, then LEAN_CC should be unset rather than set to that compiler. This feels rather unprincipled to me, but I guess I can make it work as stop-gap solution.

Honestly, I really think Lake should just bypass leanc altogether and invoke the compiler directly. Otherwise, as it stands, there are essentially two build tools to configure -- Lake with its user facing settings and leanc with its hidden internal settings. This makes it difficult both to figure out and to control how Lean C files are actually built and thus how to make them play nice with other external C code one wishes to link to.

[Kha]

This feels rather unprincipled to me, but I guess I can make it work as stop-gap solution.

It feels more principled to me than worrying about whether we have to compare LEAN_CC against the default with or without normalization and/or realPath conversion, whether we need to catch exceptions during that, ...

Honestly, I really think Lake should just bypass leanc altogether and invoke the compiler directly

I'm still open to that as I said before

[tydeu]

@Kha

This feels rather unprincipled to me, but I guess I can make it work as stop-gap solution.

It feels more principled to me than worrying about whether we have to compare LEAN_CC against the default with or without normalization and/or realPath conversion, whether we need to catch exceptions during that, ...

Fair enough. Either way, though, there is special casing needed somewhere (either in leanc or in Lake). Alternatively, leanc could always apply its internal flags regardless of LEAN_CC being set to avoid any special casing (and maybe add an option --no-internal instead to turn it off if necessary)?

Honestly, I really think Lake should just bypass leanc altogether and invoke the compiler directly

I'm still open to that as I said before

Oh, sorry, I had not gotten that feeling from your previous responses. You seemed to me rather resistant to the idea, wanting a more convincing case before heading in that direction. My apologies for the misunderstand. 😞

[gebner]

Honestly, I really think Lake should just bypass leanc altogether and invoke the compiler directly

I'm still open to that as I said before

The bundled compiler doesn't work on nixpkgs, so there needs to be a way to override the override the bundled compiler and the override needs to be integrated in the nixpkgs elan package. (Currently, we set LEAN_CC to the system compiler and add a bespoke wrapper around leanc.)

[Kha]

Yeah, there's no need to outright remove leanc. It's nice to have for the test suite as well.

[Kha]

Fair enough. Either way, though, there is special casing needed somewhere (either in leanc or in Lake). Alternatively, leanc could always apply its internal flags regardless of LEAN_CC being set to avoid any special casing (and maybe add an option --no-internal instead to turn it off if necessary)?

Honestly at this point I'm okay with anything that works for Lake and doesn't break Nixpkgs elan. If you think it should be in leanc, I'm happy to merge a PR.

Oh, sorry, I had not gotten that feeling from your previous responses.

Hah, I may have been more hesitant in the past. But here I was referring to https://github.com/leanprover/lake/pull/89#issuecomment-1170932460. Performance is a convincing use case, this issue is a convincing-enough use case.

[tydeu]

@gebner

The bundled compiler doesn't work on nixpkgs, so there needs to be a way to override the override the bundled compiler and the override needs to be integrated in the nixpkgs elan package. (Currently, we set LEAN_CC to the system compiler and add a bespoke wrapper around leanc.)

Yeah, I was just talking about skipping leanc in Lake, which isn't in the nixpkgs setup, correct? Even if it is,, the plan would be to still have Lake respect LEAN_CC, so everything should (fingers crossed) still work.

[gebner]

I was just talking about skipping leanc in Lake, which isn't in the nixpkgs setup, correct?

Whether that works depends on what you call instead of leanc. If you call the bundled compiler, then it will break.

[Kha]

Right, my bad. Lake would have to correctly respect LEAN_CC in that case, yes.