-
Notifications
You must be signed in to change notification settings - Fork 349
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
leanc
does not use internal flags when LEAN_CC
is set even if it is set to the bundled compiler
#1281
Comments
But why would it do that? |
It bears repeating that |
How is
|
@gebner Ah, I can't say that customizing |
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. |
The logic here is that Lake should forward its configured environment to the instances it spawns. So, if Lake is configured with a given However, the "by default" case breaks this because, while Lean can correctly find the bundled compiler, passing the bundled compiler via Honestly, I really think Lake should just bypass |
It feels more principled to me than worrying about whether we have to compare
I'm still open to that as I said before |
Fair enough. Either way, though, there is special casing needed somewhere (either in
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. 😞 |
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, there's no need to outright remove |
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
Hah, I may have been more hesitant in the past. But here I was referring to leanprover/lake#89 (comment). Performance is a convincing use case, this issue is a convincing-enough use case. |
Yeah, I was just talking about skipping |
Whether that works depends on what you call instead of |
Right, my bad. Lake would have to correctly respect |
Prerequisites
Description
If
LEAN_CC
is set,leanc
will not apply its internal flags, evenLEAN_CC
is set to the bundled compiler.lean4/src/Leanc.lean
Lines 43 to 47 in 2061c9b
Steps to Reproduce
From leanprover/lake#93, setting
precompileModules
to true produces the following LSP error: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 vialean --server
(see Lake'sserve
method for details).Expected behavior:
leanc
to apply its internal flags ifLEAN_CC
points to the bundled compiler.Actual behavior:
leanc
breaks ifLEAN_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.
The text was updated successfully, but these errors were encountered: