Files are compiled twice when compiled

[gebner]

When compiling Lean files, we are not always generating C files. So if you have two targets, one which only requires oleans and the other compiles an executable, then the second will unexpectedly cause recompilation.

To reproduce:

git clone https://github.com/leanprover-community/mathlib4 5c951924850fb1fb3d8a656129d9637c401cc6b4
cd 5c951924850fb1fb3d8a656129d9637c401cc6b4
lake build
lake build runLinter

[gebner]

This also causes incorrect rebuilds:

git clone https://github.com/leanprover-community/mathlib4 5c951924850fb1fb3d8a656129d9637c401cc6b4
cd 5c951924850fb1fb3d8a656129d9637c401cc6b4
lake build runLinter
git checkout ea3eef0a270babfe47af87657981c2439325de14
lake build
lake build runLinter

The last command fails with a linking error:

/nix/store/cz52w8xf3i1d3xvzpzd9abf7rvpl9017-binutils-2.38/bin/ld: ./build/ir/Mathlib/Data/Array/Defs.o: in function `initialize_Mathlib_Data_Array_Defs':
Defs.c:(.text+0xd7d): undefined reference to `initialize_Mathlib_Init_Data_Nat_Basic'
collect2: error: ld returned 1 exit status
error: external command /home/gebner/.elan/toolchains/leanprover--lean4---nightly-2022-06-13/bin/leanc exited with status 1

[tydeu]

So if you have two targets, one which only requires oleans and the other compiles an executable, then the second will unexpectedly cause recompilation.

This is the intended behavior. I am confused why you would expect differently? As no .c file was produced originally, we need to recompile the module to produce one (since no .olean -> .c process currently exists).

[tydeu]

This also causes incorrect rebuilds

Ah, yeah, this a bug. Lake currently only produces a single trace for the module. The module is thus up to date because of the .olean rebuild but the .c file was not rebuilt. I had not considered the possibility of .c file existing when the default build is just .olean files. This is somewhat separate issue though from the title of this one.

[tydeu]

I went ahead and split the bug into a separate issue.

[Kha]

Didn't we talk about this in a prior meeting 😄 ? https://leanprover.zulipchat.com/#narrow/stream/147302-lean4-dev/topic/4.2E0.2E0-m3.20ETA.3F/near/270014591
In any case, as long as we can't produce .c files purely from .olean files, I maintain that always producing .c files is the sensible thing to do with virtually no downsides.

[tydeu]

@Kha Yeah, I do think we've talked about this before. 😆 I am still not a fan of producing C code when there is no intention to build any native code (e.g., for basic theorem proving). However, I did do the rename of the oleans facet to leanLib (allowing for the more general use case we discussed in #47) and do intend to merge the olean/olean&c pipelines into one flexible pipeline this week. I still intend to not produce C code on a leanLib build though (unless precompileModules is turned on). I believe makes sense in principle (and may end up being relevant when we have other backends like LLVM IR, MLIR, and WASM).

[tydeu]

Given all that, I am considering closing this as wontfix for now.

[gebner]

I am confused why you would expect differently? As no .c file was produced originally, we need to recompile the module to produce one (since no .olean -> .c process currently exists).

I would have expected the .c file to always be generated. The most expensive part is compiling .lean→.olean; duplicating an expensive step to avoid an extra file seems counterproductive to me.

Longer-term we might want to decouple the .c file generation from the main compilation step, also to support other backends like you've mentioned. But for now I think it would be best to simplify the code and just always generate .c files.