max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: Nix: do not compile shell/lean.cpp into leancpp

Browse source
This commit is contained in:
Sebastian Ullrich 2021-01-10 18:52:23 +01:00
parent 02a4383afb
commit 332ca33947
1 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
nix/bootstrap.nix
View file

@ -34,10 +34,14 @@ rec {
leancpp = buildCMake {
name = "leancpp";
src = ../src;
# `lean.cpp` is usually linked directly into the executable, but we want to do that step outside of CMake
preConfigure = ''
echo "target_sources(leancpp PRIVATE shell/lean.cpp)" >> CMakeLists.txt
echo 'add_library(leancppmain shell/lean.cpp)
set_target_properties(leancppmain PROPERTIES
ARCHIVE_OUTPUT_DIRECTORY ''${CMAKE_BINARY_DIR}/lib/lean
OUTPUT_NAME leancppmain)' >> CMakeLists.txt
'';
buildFlags = [ "leancpp" ];
buildFlags = [ "leancpp" "leancppmain" ];
installPhase = ''
mkdir -p $out
mv lib/ $out/
@ -87,8 +91,8 @@ rec {
name = "lean-${desc}";
buildCommand = ''
mkdir -p $out/bin $out/lib/lean
ln -sf ${leancpp}/lib/lean/* ${Leanpkg.modRoot}/* ${Lean.staticLib}/* ${Lean.modRoot}/* ${Std.staticLib}/* ${Std.modRoot}/* ${Init.staticLib}/* ${Init.modRoot}/* $out/lib/lean/
${leanc}/bin/leanc -x none -rdynamic -o $out/bin/lean
ln -sf ${leancpp}/lib/lean/libleancpp.* ${Leanpkg.modRoot}/* ${Lean.staticLib}/* ${Lean.modRoot}/* ${Std.staticLib}/* ${Std.modRoot}/* ${Init.staticLib}/* ${Init.modRoot}/* $out/lib/lean/
${leanc}/bin/leanc -x none -rdynamic ${leancpp}/lib/lean/libleancppmain.* -o $out/bin/lean
${leanc}/bin/leanc -x none -rdynamic ${Leanpkg.staticLib}/* -o $out/bin/leanpkg
'';
});