diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix index 1cdeabd80f..1b8b916b10 100644 --- a/nix/bootstrap.nix +++ b/nix/bootstrap.nix @@ -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 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e160af14f1..898fe08751 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -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") diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index e75d9fb35e..71e63e9505 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -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) diff --git a/src/shell/lean.cpp b/src/util/shell.cpp similarity index 99% rename from src/shell/lean.cpp rename to src/util/shell.cpp index 034a465294..31aa39e03c 100644 --- a/src/shell/lean.cpp +++ b/src/util/shell.cpp @@ -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.