stage0 builds twice on windows

Stream: lean4 dev

[Robin Arnez]

When building stage0 I now noticed multiple times that everything under stage0/stdlib/Lean seems to be built twice (without caching for the second pass!), specifically:

[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Std/Time/Zoned/ZoneRules.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/AddDecl.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Attributes.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/BuiltinDocAttr.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Class.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Compiler/ClosedTermCache.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Compiler/CSimpAttr.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Compiler/ExternAttr.c
...
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Widget/InteractiveCode.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Widget/InteractiveDiagnostic.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Widget/InteractiveGoal.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Widget/TaggedText.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Widget/Types.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Widget/UserWidget.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/AddDecl.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Attributes.c
...
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Widget/Diff.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Widget/InteractiveCode.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Widget/InteractiveDiagnostic.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Widget/InteractiveGoal.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Widget/TaggedText.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Widget/Types.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Widget/UserWidget.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lake/Build/Actions.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lake/Build/Common.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lake/Build/Executable.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lake/Build/ExternLib.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lake/Build/Facets.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lake/Build/Index.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lake/Build/InputFile.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lake/Build/Job/Basic.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lake/Build/Key.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lake/Build/Library.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/BuiltinDocAttr.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Class.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Compiler/ClosedTermCache.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Compiler/CSimpAttr.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean/Compiler/ExternAttr.c

I'm not sure why exactly this might happen but I attached the full build log here:
build log.txt

[Henrik Böving]

This has always been the case on windows I think? At least I can remember seeing it months ago on our Windows debugging setup.

[Robin Arnez]

Is there a reason for this?

[Henrik Böving]

Iirc it was because we are forced to build two DLLs on Windows because Microsoft is in denial about developers needing more than 2^16 symbols per DLL but I don't remember the precise details why it has to be built twice for that.

[Robin Arnez]

We're building three DLLs though and only building twice... idk

[Henrik Böving]

Oh the third DLL is new yeah

[Robin Arnez]

I don't quite understand why you'd need to build the same thing multiple times then though; wouldn't you just need to select the right .o files to build the DLLs?

[Henrik Böving]

I don't remember, I try to not think too much about my interactions with Windows as it is a completely unnecessary pain every time :sweat_smile:. You can probably trace out what the different invocations to the C compiler are by asking make with make VERBOSE=1

[Robin Arnez]

Well I don't really want to invalidate stage0 since I'd need to rebuild basically everything then... I'll maybe try that next time I need it

[Henrik Böving]

But it should be in cache now right?

[Robin Arnez]

Yeah right I mean right now it won't run the C compiler at all for stage0, I would need to change stuff in stage0 to get compiler calls

[Robin Arnez]

Right this is what it looks like now

Rebuild with cache

[  4%] Performing update step for 'mimalloc'
-- Already at requested tag: v2.2.3
[  8%] No patch step for 'mimalloc'
[ 12%] No configure step for 'mimalloc'
[ 16%] No build step for 'mimalloc'
[ 20%] No install step for 'mimalloc'
[ 25%] Completed 'mimalloc'
[ 33%] Built target mimalloc
[ 37%] Performing configure step for 'stage0'
-- No build type selected, default to Release
-- 64-bit machine detected
-- Windows detected
-- LIBUV_LDFLAGS: -LC:/msys64/clang64/lib-luv-lpsapi-luser32-ladvapi32-liphlpapi-luserenv-lws2_32-ldbghelp-lole32-lshell32
-- LIBUV_INCLUDE_DIRS: C:/msys64/clang64/include
-- stage0 sha1: 068d969076cdd71d9c3f2e26dcf8373d764cc1a2
-- Configuring done (0.3s)
-- Generating done (0.3s)
-- Build files have been written to: C:/Users/robin/lean4dev/lean4/build/release/stage0
[ 41%] Performing build step for 'stage0'
[  2%] Built target leanmain
[  4%] Built target leanmanifest
[  5%] Built target initialize
[  7%] Built target constructions
[  9%] Built target leanshell
[ 35%] Built target kernel
[ 35%] Built target util
[ 36%] Built target leaninitialize
[ 52%] Built target library
[ 97%] Built target leanrt_initial-exec
[ 99%] Built target leanrt
[ 99%] Built target leancpp_1
[100%] Built target leancpp
[100%] Built target make_stdlib
[100%] Built target Init_shared
[100%] Built target leanshared
[100%] Built target lean
[100%] Built target lake_shared
[100%] Built target lake
[ 45%] No install step for 'stage0'
[ 50%] Completed 'stage0'
[ 66%] Built target stage0
[ 70%] Performing configure step for 'stage1'
-- No build type selected, default to Release
-- 64-bit machine detected
-- Windows detected
-- LIBUV_LDFLAGS: -LC:/msys64/clang64/lib-luv-lpsapi-luser32-ladvapi32-liphlpapi-luserenv-lws2_32-ldbghelp-lole32-lshell32
-- LIBUV_INCLUDE_DIRS: C:/msys64/clang64/include
-- git commit sha1: ce1e63fe3d1ae3b102100293ce08c6c1c53898e8
-- Configuring done (0.3s)
-- Generating done (0.3s)
-- Build files have been written to: C:/Users/robin/lean4dev/lean4/build/release/stage1
[ 75%] Performing build step for 'stage1'
[  0%] Built target copy-cadical
[  2%] Built target leanmanifest
[  4%] Built target leanmain
[  5%] Built target initialize
[  7%] Built target leanshell
[  9%] Built target constructions
[ 22%] Built target kernel
[ 35%] Built target util
[ 36%] Built target leaninitialize
[ 52%] Built target library
[ 75%] Built target leanrt_initial-exec
[ 99%] Built target leanrt
[100%] Built target leancpp
[100%] Built target leancpp_1
ℹ [3997/5155] Replayed Lean.Meta.WHNF:c.o
info: stderr:
C:\Users\robin\lean4dev\lean4\build\release\stage1\lib\temp\Lean\Meta\WHNF.c:92:26: warning: redeclaration of 'lean_whnf' should not add 'dllexport' attribute [-Wdll-attribute-on-redeclaration]
   92 | LEAN_EXPORT lean_object* lean_whnf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
      |                          ^
C:\Users\robin\lean4dev\lean4\build\release\stage1\lib\temp\Lean\Meta\WHNF.c:75:14: note: previous declaration is here
   75 | lean_object* lean_whnf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
      |              ^
1 warning generated.
ℹ [4525/5155] Replayed Lean.Meta.LevelDefEq:c.o
info: stderr:
C:\Users\robin\lean4dev\lean4\build\release\stage1\lib\temp\Lean\Meta\LevelDefEq.c:114:26: warning: redeclaration of 'lean_is_level_def_eq' should not add 'dllexport' attribute [-Wdll-attribute-on-redeclaration]
  114 | LEAN_EXPORT lean_object* lean_is_level_def_eq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
      |                          ^
C:\Users\robin\lean4dev\lean4\build\release\stage1\lib\temp\Lean\Meta\LevelDefEq.c:29:14: note: previous declaration is here
   29 | lean_object* lean_is_level_def_eq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
      |              ^
1 warning generated.
ℹ [4527/5155] Replayed Lean.Meta.ExprDefEq:c.o
info: stderr:
C:\Users\robin\lean4dev\lean4\build\release\stage1\lib\temp\Lean\Meta\ExprDefEq.c:953:26: warning: redeclaration of 'lean_is_expr_def_eq' should not add 'dllexport' attribute [-Wdll-attribute-on-redeclaration]
  953 | LEAN_EXPORT lean_object* lean_is_expr_def_eq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
      |                          ^
C:\Users\robin\lean4dev\lean4\build\release\stage1\lib\temp\Lean\Meta\ExprDefEq.c:447:14: note: previous declaration is here
  447 | lean_object* lean_is_expr_def_eq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
      |              ^
1 warning generated.
ℹ [5068/5619] Replayed Lean.Elab.Tactic.Try:c.o
info: stderr:
C:\Users\robin\lean4dev\lean4\build\release\stage1\lib\temp\Lean\Elab\Tactic\Try.c:819:26: warning: redeclaration of 'lean_eval_suggest_tactic' should not add 'dllexport' attribute [-Wdll-attribute-on-redeclaration]
  819 | LEAN_EXPORT lean_object* lean_eval_suggest_tactic(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
      |                          ^
C:\Users\robin\lean4dev\lean4\build\release\stage1\lib\temp\Lean\Elab\Tactic\Try.c:338:14: note: previous declaration is here
  338 | lean_object* lean_eval_suggest_tactic(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
      |              ^
1 warning generated.
ℹ [5094/5619] Replayed Lean.Meta.Tactic.Grind.Arith.Cutsat.Var:c.o
info: stderr:
C:\Users\robin\lean4dev\lean4\build\release\stage1\lib\temp\Lean\Meta\Tactic\Grind\Arith\Cutsat\Var.c:121:26: warning: redeclaration of 'lean_grind_cutsat_mk_var' should not add 'dllexport' attribute [-Wdll-attribute-on-redeclaration]
  121 | LEAN_EXPORT lean_object* lean_grind_cutsat_mk_var(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
      |                          ^
C:\Users\robin\lean4dev\lean4\build\release\stage1\lib\temp\Lean\Meta\Tactic\Grind\Arith\Cutsat\Var.c:50:14: note: previous declaration is here
   50 | lean_object* lean_grind_cutsat_mk_var(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
      |              ^
1 warning generated.
ℹ [5099/5619] Replayed Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr:c.o
info: stderr:
C:\Users\robin\lean4dev\lean4\build\release\stage1\lib\temp\Lean\Meta\Tactic\Grind\Arith\Cutsat\LeCnstr.c:296:26: warning: redeclaration of 'lean_grind_cutsat_assert_le' should not add 'dllexport' attribute [-Wdll-attribute-on-redeclaration]
  296 | LEAN_EXPORT lean_object* lean_grind_cutsat_assert_le(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
      |                          ^
C:\Users\robin\lean4dev\lean4\build\release\stage1\lib\temp\Lean\Meta\Tactic\Grind\Arith\Cutsat\LeCnstr.c:273:14: note: previous declaration is here
  273 | lean_object* lean_grind_cutsat_assert_le(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
      |              ^
1 warning generated.
ℹ [5101/5619] Replayed Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr:c.o
info: stderr:
C:\Users\robin\lean4dev\lean4\build\release\stage1\lib\temp\Lean\Meta\Tactic\Grind\Arith\Cutsat\EqCnstr.c:476:26: warning: redeclaration of 'lean_grind_cutsat_assert_eq' should not add 'dllexport' attribute [-Wdll-attribute-on-redeclaration]
  476 | LEAN_EXPORT lean_object* lean_grind_cutsat_assert_eq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
      |                          ^
C:\Users\robin\lean4dev\lean4\build\release\stage1\lib\temp\Lean\Meta\Tactic\Grind\Arith\Cutsat\EqCnstr.c:382:14: note: previous declaration is here
  382 | lean_object* lean_grind_cutsat_assert_eq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
      |              ^
1 warning generated.
Build completed successfully (5619 jobs).
[100%] Built target make_stdlib
[100%] Built target Init_shared
[100%] Built target leanshared
[100%] Built target leanc
[100%] Built target lake_shared
[100%] Built target lean
[100%] Built target lake
[ 79%] No install step for 'stage1'
[ 83%] Completed 'stage1'
[100%] Built target stage1

[Henrik Böving]

I don't know how it works on Windows but on Linux we use a ccache wrapper so if you remove build/release, recreate it and run make it should do those ccache calls so you can see the compiler invocation but the ccache will instantly return the object file from its object file cache. Though of course if Windows doesn't have a ccache this isn't going to help you.

[Robin Arnez]

I mean I have a ccache on msys

[Robin Arnez]

I hope it actually gets used...

[Robin Arnez]

Okay I deleted everything that's directly in build/release/stage0/lib/temp and ran make -j12 VERBOSE=1:
verbose.txt

[Robin Arnez]

I suppose this is the interesting part:

[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Init.c
[100%] Built target leancpp_1
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Init.c
C:/Users/robin/lean4dev/lean4/build/release/stage0/leanc.sh -c -o ../../build/release/stage0/lib/temp/Init.o C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Init.c -IC:/Users/robin/lean4dev/lean4/build/release/stage0/include -O3 -DNDEBUG
C:/Users/robin/lean4dev/lean4/build/release/stage0/leanc.sh -c -o ../../build/release/stage0/lib/temp/Init.o.export C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Init.c -IC:/Users/robin/lean4dev/lean4/build/release/stage0/include -O3 -DNDEBUG -DLEAN_EXPORTING
# "T"hin archive seems necessary to preserve paths so that we can distinguish
# between object files with the same file name when manipulating the archive for
# `libleanshared_*`
make[7]: Leaving directory '/c/Users/robin/lean4dev/lean4/stage0/src'
"/C/Users/robin/lean4dev/lean4/build/release/stage0/bin/leanmake" lib lib.export PKG=Std LEAN="/bin/lean" LEANC="C:/Users/robin/lean4dev/lean4/build/release/stage0/leanc.sh" OUT="../../build/release/stage0/lib" LIB_OUT="../../build/release/stage0/lib/lean" OLEAN_OUT="../../build/release/stage0/lib/lean" BIN_OUT="C:/Users/robin/lean4dev/lean4/build/release/stage0/bin" LEAN_OPTS+=" -DElab.async=true" LEANC_OPTS+=" -IC:/Users/robin/lean4dev/lean4/build/release/stage0/include -O3 -DNDEBUG" LEAN_AR="C:/msys64/clang64/bin/llvm-ar.exe" MORE_DEPS+="/bin/lean" CMAKE_LIKE_OUTPUT=1 C_ONLY=1 C_OUT=C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib/
make[7]: Entering directory '/c/Users/robin/lean4dev/lean4/stage0/src'
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Std.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Std.c
C:/Users/robin/lean4dev/lean4/build/release/stage0/leanc.sh -c -o ../../build/release/stage0/lib/temp/Std.o C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Std.c -IC:/Users/robin/lean4dev/lean4/build/release/stage0/include -O3 -DNDEBUG
C:/Users/robin/lean4dev/lean4/build/release/stage0/leanc.sh -c -o ../../build/release/stage0/lib/temp/Std.o.export C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Std.c -IC:/Users/robin/lean4dev/lean4/build/release/stage0/include -O3 -DNDEBUG -DLEAN_EXPORTING
# "T"hin archive seems necessary to preserve paths so that we can distinguish
# between object files with the same file name when manipulating the archive for
# `libleanshared_*`
make[7]: Leaving directory '/c/Users/robin/lean4dev/lean4/stage0/src'
"/C/Users/robin/lean4dev/lean4/build/release/stage0/bin/leanmake" lib lib.export PKG=Lean LEAN="/bin/lean" LEANC="C:/Users/robin/lean4dev/lean4/build/release/stage0/leanc.sh" OUT="../../build/release/stage0/lib" LIB_OUT="../../build/release/stage0/lib/lean" OLEAN_OUT="../../build/release/stage0/lib/lean" BIN_OUT="C:/Users/robin/lean4dev/lean4/build/release/stage0/bin" LEAN_OPTS+=" -DElab.async=true" LEANC_OPTS+=" -IC:/Users/robin/lean4dev/lean4/build/release/stage0/include -O3 -DNDEBUG" LEAN_AR="C:/msys64/clang64/bin/llvm-ar.exe" MORE_DEPS+="/bin/lean" CMAKE_LIKE_OUTPUT=1 C_ONLY=1 C_OUT=C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib/
make[7]: Entering directory '/c/Users/robin/lean4dev/lean4/stage0/src'
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean.c
C:/Users/robin/lean4dev/lean4/build/release/stage0/leanc.sh -c -o ../../build/release/stage0/lib/temp/Lean.o C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean.c -IC:/Users/robin/lean4dev/lean4/build/release/stage0/include -O3 -DNDEBUG
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean.c
C:/Users/robin/lean4dev/lean4/build/release/stage0/leanc.sh -c -o ../../build/release/stage0/lib/temp/Lean.o.export C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lean.c -IC:/Users/robin/lean4dev/lean4/build/release/stage0/include -O3 -DNDEBUG -DLEAN_EXPORTING
# "T"hin archive seems necessary to preserve paths so that we can distinguish
# between object files with the same file name when manipulating the archive for
# `libleanshared_*`
make[7]: Leaving directory '/c/Users/robin/lean4dev/lean4/stage0/src'
make[6]: Nothing to be done for 'Leanc'.
"/C/Users/robin/lean4dev/lean4/build/release/stage0/bin/leanmake" -C lake lib lib.export ../../../build/release/stage0/lib/temp/LakeMain.o.export  PKG=Lake LEAN="/bin/lean" LEANC="C:/Users/robin/lean4dev/lean4/build/release/stage0/leanc.sh" OUT="../../build/release/stage0/lib" LIB_OUT="../../build/release/stage0/lib/lean" OLEAN_OUT="../../build/release/stage0/lib/lean" BIN_OUT="C:/Users/robin/lean4dev/lean4/build/release/stage0/bin" LEAN_OPTS+=" -DElab.async=true" LEANC_OPTS+=" -IC:/Users/robin/lean4dev/lean4/build/release/stage0/include -O3 -DNDEBUG" LEAN_AR="C:/msys64/clang64/bin/llvm-ar.exe" MORE_DEPS+="/bin/lean" CMAKE_LIKE_OUTPUT=1 C_ONLY=1 C_OUT=C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib/ OUT="../../../build/release/stage0/lib" LIB_OUT="../../../build/release/stage0/lib/lean" TEMP_OUT="../../../build/release/stage0/lib/temp" OLEAN_OUT="../../../build/release/stage0/lib/lean" EXTRA_SRC_ROOTS=LakeMain.lean
make[7]: Entering directory '/c/Users/robin/lean4dev/lean4/stage0/src/lake'
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lake.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lake.c
[    ] Building C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//LakeMain.c
C:/Users/robin/lean4dev/lean4/build/release/stage0/leanc.sh -c -o ../../../build/release/stage0/lib/temp/Lake.o C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lake.c -IC:/Users/robin/lean4dev/lean4/build/release/stage0/include -O3 -DNDEBUG
C:/Users/robin/lean4dev/lean4/build/release/stage0/leanc.sh -c -o ../../../build/release/stage0/lib/temp/Lake.o.export C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Lake.c -IC:/Users/robin/lean4dev/lean4/build/release/stage0/include -O3 -DNDEBUG -DLEAN_EXPORTING
C:/Users/robin/lean4dev/lean4/build/release/stage0/leanc.sh -c -o ../../../build/release/stage0/lib/temp/LakeMain.o.export C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//LakeMain.c -IC:/Users/robin/lean4dev/lean4/build/release/stage0/include -O3 -DNDEBUG -DLEAN_EXPORTING
# "T"hin archive seems necessary to preserve paths so that we can distinguish
# between object files with the same file name when manipulating the archive for
# `libleanshared_*`
make[7]: Leaving directory '/c/Users/robin/lean4dev/lean4/stage0/src/lake'
make[6]: Leaving directory '/c/Users/robin/lean4dev/lean4/stage0/src'
make[5]: Leaving directory '/c/Users/robin/lean4dev/lean4/build/release/stage0'
[100%] Built target make_stdlib

[Robin Arnez]

Hmm I don't see any mention of ccache

[Henrik Böving]

ccache disguises itself as a normal c compiler binary so its completely plug and play, it's hidden behind the leanc invocation, but the key is:

C:/Users/robin/lean4dev/lean4/build/release/stage0/leanc.sh -c -o ../../build/release/stage0/lib/temp/Init.o C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Init.c -IC:/Users/robin/lean4dev/lean4/build/release/stage0/include -O3 -DNDEBUG
C:/Users/robin/lean4dev/lean4/build/release/stage0/leanc.sh -c -o ../../build/release/stage0/lib/temp/Init.o.export C:/Users/robin/lean4dev/lean4/stage0/src/../stdlib//Init.c -IC:/Users/robin/lean4dev/lean4/build/release/stage0/include -O3 -DNDEBUG -DLEAN_EXPORTING
# "T"hin archive seems necessary to preserve paths so that we can distinguish
# between object files with the same file name when manipulating the archive for
# `libleanshared_*`

I personally don't want to know what a Thin archive is but that is the reason we have to build twice

[Henrik Böving]

In particular one file is built with -DLEAN_EXPORTING while the other is built without it to provide object files for linking in the same and in different DLLs and that's the reason two C compiler invocations occur

[Henrik Böving]

Note that it would be quite great in general if we didn't have to do this because not only stage0 but also stage1 has to be double built in this fashion and that's one of the factors that make our Windows CI times quite horrible compared to the other platforms.

That said I'm not willing to loose my sanity over Windows linking details again :sweat_smile:

[Robin Arnez]

Hmm I feel like since I started using -DUSE_LAKE stage1 build times have gone down significantly; I guess maybe it still does this double compilation but it uses better caching? Not sure

[Henrik Böving]

Lake can be a lot smarter about caching yes. The CMake/Makefile system merely acts on files being touched at a later date than the files that depend on them have been so if you do any modification the entire transitive import closure has to be recompiled. Lake has a more semantic notion of rebuilding.

[Henrik Böving]

(and of course the module system comes in handy here as well)

[Mac Malone]

Lake doesn't build stage0, so while it may (hopefully) improve the build time overall, it is not helping here for stage0.

[Mac Malone]

(oops, accidentally necroposted)

[Robin Arnez]

Okay, coming back to this, it seems like the only difference between o.export / o.noexport is that o.export additionally contains a .drectve section. So it feels like all we need to do here is to simply write (or use) a utility that deletes the .drectve section from an .o file and then use that instead of a rebuild.

[Robin Arnez]

Seems like llvm-objcopy --remove-section .drectve abc.c.o.export abc.c.o.noexport should do the trick

[Yuri]

So, always build with LEAN_EXPORTING and then strip the section? If this works, it would simplify the build a bit including Lake.