Skip to content

Commit c2761dc

Browse files
KhaKha
authored
feat: Lake shared library (#5143)
Fixes #2436 #5050 Next step: when libLake_shared is in stage 0, --load-dynlib it when building stage 1 Lake
1 parent ec7ae59 commit c2761dc

File tree

6 files changed

+52
-12
lines changed

6 files changed

+52
-12
lines changed

‎nix/bootstrap.nix

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -95,12 +95,13 @@ lib.warn "The Nix-based build is deprecated" rec {
9595
Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Std ]; };
9696
Lake = build {
9797
name = "Lake";
98+
sharedLibName = "Lake_shared";
9899
src = src + "/src/lake";
99100
deps = [ Init Lean ];
100101
};
101102
Lake-Main = build {
102-
name = "Lake.Main";
103-
roots = [ "Lake.Main" ];
103+
name = "LakeMain";
104+
roots = [{ glob = "one"; mod = "LakeMain"; }];
104105
executableName = "lake";
105106
deps = [ Lake ];
106107
linkFlags = lib.optional stdenv.isLinux "-rdynamic";
@@ -133,7 +134,7 @@ lib.warn "The Nix-based build is deprecated" rec {
133134
mods = foldl' (mods: pkg: mods // pkg.mods) {} stdlib;
134135
print-paths = Lean.makePrintPathsFor [] mods;
135136
leanc = writeShellScriptBin "leanc" ''
136-
LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${libInit_shared} -L${leanshared_1} -L${leanshared} "$@"
137+
LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${libInit_shared} -L${leanshared_1} -L${leanshared} -L${Lake.sharedLib} "$@"
137138
'';
138139
lean = runCommand "lean" { buildInputs = lib.optional stdenv.isDarwin darwin.cctools; } ''
139140
mkdir -p $out/bin
@@ -144,7 +145,7 @@ lib.warn "The Nix-based build is deprecated" rec {
144145
name = "lean-${desc}";
145146
buildCommand = ''
146147
mkdir -p $out/bin $out/lib/lean
147-
ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList stdlib)} ${libInit_shared}/* ${leanshared_1}/* ${leanshared}/* $out/lib/lean/
148+
ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList stdlib)} ${libInit_shared}/* ${leanshared_1}/* ${leanshared}/* ${Lake.sharedLib}/* $out/lib/lean/
148149
# put everything in a single final derivation so `IO.appDir` references work
149150
cp ${lean}/bin/lean ${leanc}/bin/leanc ${Lake-Main.executable}/bin/lake $out/bin
150151
# NOTE: `lndir` will not override existing `bin/leanc`

‎nix/buildLeanPackage.nix

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ lib.makeOverridable (
3030
pluginDeps ? [],
3131
# `overrideAttrs` for `buildMod`
3232
overrideBuildModAttrs ? null,
33-
debug ? false, leanFlags ? [], leancFlags ? [], linkFlags ? [], executableName ? lib.toLower name, libName ? name,
33+
debug ? false, leanFlags ? [], leancFlags ? [], linkFlags ? [], executableName ? lib.toLower name, libName ? name, sharedLibName ? libName,
3434
srcTarget ? "..#stage0", srcArgs ? "(\${args[*]})", lean-final ? lean-final' }@args:
3535
with builtins; let
3636
# "Init.Core" ~> "Init/Core"
@@ -233,7 +233,7 @@ in rec {
233233
cTree = symlinkJoin { name = "${name}-cTree"; paths = map (mod: mod.c) (attrValues mods); };
234234
oTree = symlinkJoin { name = "${name}-oTree"; paths = (attrValues objects); };
235235
iTree = symlinkJoin { name = "${name}-iTree"; paths = map (mod: mod.ilean) (attrValues mods); };
236-
sharedLib = mkSharedLib "lib${libName}" ''
236+
sharedLib = mkSharedLib "lib${sharedLibName}" ''
237237
${if stdenv.isDarwin then "-Wl,-force_load,${staticLib}/lib${libName}.a" else "-Wl,--whole-archive ${staticLib}/lib${libName}.a -Wl,--no-whole-archive"} \
238238
${lib.concatStringsSep " " (map (d: "${d.sharedLib}/*") deps)}'';
239239
executable = lib.makeOverridable ({ withSharedStdlib ? true }: let

‎script/lib/update-stage0

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ done
1818

1919
# special handling for Lake files due to its nested directory
2020
# copy the README to ensure the `stage0/src/lake` directory is comitted
21-
for f in $(git ls-files 'src/lake/Lake/*' src/lake/Lake.lean src/lake/README.md ':!:src/lakefile.toml'); do
21+
for f in $(git ls-files 'src/lake/Lake/*' src/lake/Lake.lean src/lake/LakeMain.lean src/lake/README.md ':!:src/lakefile.toml'); do
2222
if [[ $f == *.lean ]]; then
2323
f=${f#src/lake}
2424
f=${f%.lean}.c

‎src/CMakeLists.txt

Lines changed: 26 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -333,7 +333,12 @@ if(NOT LEAN_STANDALONE)
333333
endif()
334334

335335
# flags for user binaries = flags for toolchain binaries + Lake
336-
string(APPEND LEANC_STATIC_LINKER_FLAGS " ${TOOLCHAIN_STATIC_LINKER_FLAGS} -lLake")
336+
set(LEANC_STATIC_LINKER_FLAGS " ${TOOLCHAIN_STATIC_LINKER_FLAGS} -lLake")
337+
if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
338+
set(LEANC_SHARED_LINKER_FLAGS " ${TOOLCHAIN_SHARED_LINKER_FLAGS} -Wl,--as-needed -lLake_shared -Wl,--no-as-needed")
339+
else()
340+
set(LEANC_SHARED_LINKER_FLAGS " ${TOOLCHAIN_SHARED_LINKER_FLAGS} -lLake_shared")
341+
endif()
337342

338343
if (LLVM)
339344
string(APPEND LEANSHARED_LINKER_FLAGS " -L${LLVM_CONFIG_LIBDIR} ${LLVM_CONFIG_LDFLAGS} ${LLVM_CONFIG_LIBS} ${LLVM_CONFIG_SYSTEM_LIBS}")
@@ -378,16 +383,20 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
378383
string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec")
379384
string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
380385
string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
386+
string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libLake.a.export -Wl,--no-whole-archive")
381387
string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
382388
elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
383389
string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec")
384390
string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib")
385391
string(APPEND LEANSHARED_1_LINKER_FLAGS " -install_name @rpath/libleanshared_1.dylib")
386392
string(APPEND LEANSHARED_LINKER_FLAGS " -install_name @rpath/libleanshared.dylib")
393+
string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/temp/libLake.a.export -install_name @rpath/libLake_shared.dylib")
387394
string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean")
388395
elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
389396
string(APPEND CMAKE_CXX_FLAGS " -fPIC")
390397
string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
398+
elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
399+
string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libLake_shared.dll.a -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libLake.a.export -Wl,--no-whole-archive")
391400
endif()
392401

393402
if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
@@ -587,8 +596,13 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
587596
)
588597
add_custom_target(leanshared ALL
589598
DEPENDS Init_shared leancpp
599+
COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX}
590600
COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}
591601
)
602+
add_custom_target(lake_shared ALL
603+
DEPENDS leanshared
604+
COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
605+
)
592606
else()
593607
add_custom_target(Init_shared ALL
594608
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
@@ -606,11 +620,21 @@ else()
606620
endif()
607621

608622
if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
609-
add_custom_target(lake ALL
623+
add_custom_target(lake_lib ALL
610624
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
611625
DEPENDS leanshared
612626
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Lake
613627
VERBATIM)
628+
add_custom_target(lake_shared ALL
629+
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
630+
DEPENDS lake_lib
631+
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make libLake_shared
632+
VERBATIM)
633+
add_custom_target(lake ALL
634+
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
635+
DEPENDS lake_shared
636+
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make lake
637+
VERBATIM)
614638
endif()
615639

616640
if(PREV_STAGE)

‎src/lake/Lake/Main.lean renamed to ‎src/lake/LakeMain.lean

File renamed without changes.

‎src/stdlib.make.in

Lines changed: 18 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ ifeq "${STAGE}" "0"
2929
LEANMAKE_OPTS+=C_ONLY=1 C_OUT=${LEAN_SOURCE_DIR}/../stdlib/
3030
endif
3131

32-
.PHONY: Init Std Lean leanshared Lake lean
32+
.PHONY: Init Std Lean leanshared Lake Lake_shared lake lean
3333

3434
# These can be phony since the inner Makefile will have the correct dependencies and avoid rebuilds
3535
Init:
@@ -100,9 +100,24 @@ leanshared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRAR
100100

101101
Lake:
102102
# lake is in its own subdirectory, so must adjust relative paths...
103-
+"${LEAN_BIN}/leanmake" -C lake bin lib PKG=Lake BIN_NAME=lake${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}' OUT="../${LIB}" LIB_OUT="../${LIB}/lean" OLEAN_OUT="../${LIB}/lean"
103+
+"${LEAN_BIN}/leanmake" -C lake lib lib.export ../${LIB}/temp/LakeMain.o.export PKG=Lake $(LEANMAKE_OPTS) OUT="../${LIB}" LIB_OUT="../${LIB}/lean" TEMP_OUT="../${LIB}/temp" OLEAN_OUT="../${LIB}/lean" EXTRA_SRC_ROOTS=LakeMain.lean
104104

105-
${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/libleanmain.a
105+
${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/libLean.a.export ${LIB}/temp/libLake.a.export
106+
@echo "[ ] Building $@"
107+
"${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ \
108+
${LAKESHARED_LINKER_FLAGS} -lleanshared -lleanshared_1 -lInit_shared ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
109+
110+
libLake_shared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
111+
112+
${CMAKE_BINARY_DIR}/bin/lake${CMAKE_EXECUTABLE_SUFFIX}: ${LIB}/temp/LakeMain.o.export ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
113+
@echo "[ ] Building $@"
114+
# on Windows, must remove file before writing a new one (since the old one may be in use)
115+
@rm -f $@
116+
"${CMAKE_BINARY_DIR}/leanc.sh" $^ ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEANC_OPTS} -o $@
117+
118+
lake: ${CMAKE_BINARY_DIR}/bin/lake${CMAKE_EXECUTABLE_SUFFIX}
119+
120+
${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/libleanmain.a
106121
@echo "[ ] Building $@"
107122
# on Windows, must remove file before writing a new one (since the old one may be in use)
108123
@rm -f $@

0 commit comments

Comments
 (0)