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

chore: move all C++ code into libleanshared, use C stub for main

Browse source 
Avoids any issues with cross-lib C++
This commit is contained in:
Sebastian Ullrich 2021-09-16 11:12:04 +02:00 • committed by Leonardo de Moura
parent 08c2c31fcd
commit b3bb2bac97
4 changed files with 3 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
nix/bootstrap.nix
View file

@ -102,7 +102,7 @@ rec {
'';
lean = runCommand "lean" {} ''
mkdir -p $out/bin
${leanc}/bin/leanc ${leancpp}/lib/lean.cpp.o ${leanshared}/* -o $out/bin/lean ${if stdenv.isDarwin then "-lc++" else "-lstdc++"}
${leanc}/bin/leanc ${leancpp}/lib/lean.cpp.o ${leanshared}/* -o $out/bin/lean
'';
leanpkg = Leanpkg.executable.withSharedStdlib;
# derivation following the directory layout of the "basic" setup, mostly useful for running tests

2
src/CMakeLists.txt
View file

@ -284,11 +284,9 @@ endif()
if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lc++")
set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -lc++")
set(LEAN_EXE_LINKER_FLAGS "${LEAN_EXE_LINKER_FLAGS} -lc++")
else()
set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lstdc++")
set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -lstdc++")
set(LEAN_EXE_LINKER_FLAGS "${LEAN_EXE_LINKER_FLAGS} -lstdc++")
endif()
set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lm")

2
src/util/CMakeLists.txt
View file

@ -3,4 +3,4 @@ add_library(util OBJECT name.cpp name_set.cpp
path.cpp lbool.cpp init_module.cpp list_fn.cpp
timeit.cpp timer.cpp
name_generator.cpp kvmap.cpp map_foreach.cpp
options.cpp format.cpp option_declarations.cpp)
options.cpp format.cpp option_declarations.cpp shell.cpp)

2
src/shell/lean.cpp → src/util/shell.cpp
View file

@ -381,7 +381,7 @@ void check_optarg(char const * option_name) {
extern "C" object * lean_enable_initializer_execution(object * w);
int main(int argc, char ** argv) {
extern "C" int lean_main(int argc, char ** argv) {
#ifdef LEAN_EMSCRIPTEN
// When running in command-line mode under Node.js, we make system directories available in the virtual filesystem.
// This mode is used to compile 32-bit oleans.