diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9a2526ab8..9ba91c5d9 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -123,6 +123,11 @@ set(CPACK_PACKAGE_FILE_NAME "Lean-${LEAN_VERSION_MAJOR}.${LEAN_VERSION_MINOR}") set(CPACK_PACKAGE_ICON "${LEAN_SOURCE_DIR}/../images/lean.png") ################## +if (${CMAKE_SYSTEM_NAME} MATCHES "Linux") + # The following options is needed to generate a shared library + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fPIC") +endif() + include(CheckIncludeFileCXX) check_include_file_cxx("unistd.h" HAVE_UNISTD) @@ -311,46 +316,48 @@ configure_file("${LEAN_SOURCE_DIR}/../bin/linja.in" "${LEAN_SOURCE_DIR}/../bin/l include_directories("${LEAN_BINARY_DIR}") add_subdirectory(util) -set(LEAN_LIBS ${LEAN_LIBS} util) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(util/numerics) -set(LEAN_LIBS ${LEAN_LIBS} numerics) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(util/sexpr) -set(LEAN_LIBS ${LEAN_LIBS} sexpr) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(util/interval) -set(LEAN_LIBS ${LEAN_LIBS} interval) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(kernel) -set(LEAN_LIBS ${LEAN_LIBS} kernel) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(kernel/inductive) -set(LEAN_LIBS ${LEAN_LIBS} inductive) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(kernel/quotient) -set(LEAN_LIBS ${LEAN_LIBS} quotient) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(kernel/hits) -set(LEAN_LIBS ${LEAN_LIBS} hits) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library) -set(LEAN_LIBS ${LEAN_LIBS} library) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/simplifier) -set(LEAN_LIBS ${LEAN_LIBS} simplifier) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/tactic) -set(LEAN_LIBS ${LEAN_LIBS} tactic) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/definitional) -set(LEAN_LIBS ${LEAN_LIBS} definitional) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/error_handling) -set(LEAN_LIBS ${LEAN_LIBS} error_handling) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(frontends/lean) -set(LEAN_LIBS ${LEAN_LIBS} lean_frontend) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(frontends/lua) -set(LEAN_LIBS ${LEAN_LIBS} leanlua) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(init) -set(LEAN_LIBS ${LEAN_LIBS} init) +set(LEAN_OBJS ${LEAN_OBJS} $) set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS}") if(MULTI_THREAD AND (NOT ("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")) AND (NOT BOOST)) set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread") endif() set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage") -set(ALL_LIBS ${LEAN_LIBS} ${EXTRA_LIBS}) +add_library(leanstatic ${LEAN_OBJS}) +add_library(leanshared SHARED ${LEAN_OBJS}) + add_subdirectory(shell) -set(LEAN_LIBS ${LEAN_LIBS} shell) add_subdirectory(emacs) + add_subdirectory(tests/util) add_subdirectory(tests/util/numerics) add_subdirectory(tests/util/interval) diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 28b82f033..5704b4303 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -1,4 +1,4 @@ -add_library(lean_frontend tokens.cpp register_module.cpp +add_library(lean_frontend OBJECT tokens.cpp register_module.cpp token_table.cpp scanner.cpp parse_table.cpp parser_config.cpp parser.cpp parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp server.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp @@ -11,5 +11,3 @@ parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp type_util.cpp elaborator_exception.cpp migrate_cmd.cpp local_ref_info.cpp obtain_expr.cpp decl_attributes.cpp nested_declaration.cpp parse_with_options_tactic.cpp parse_simp_tactic.cpp opt_cmd.cpp) - -target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lua/CMakeLists.txt b/src/frontends/lua/CMakeLists.txt index c4dde5af2..94f82406e 100644 --- a/src/frontends/lua/CMakeLists.txt +++ b/src/frontends/lua/CMakeLists.txt @@ -1,3 +1 @@ -add_library(leanlua register_modules.cpp) - -target_link_libraries(leanlua ${LEAN_LIBS}) +add_library(leanlua OBJECT register_modules.cpp) diff --git a/src/init/CMakeLists.txt b/src/init/CMakeLists.txt index cfd1dd399..f8c1052a3 100644 --- a/src/init/CMakeLists.txt +++ b/src/init/CMakeLists.txt @@ -1,3 +1 @@ -add_library(init init.cpp) - -target_link_libraries(init ${LEAN_LIBS}) +add_library(init OBJECT init.cpp) diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index 70ba4ac8a..eb5d23c2b 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -1,9 +1,7 @@ -add_library(kernel level.cpp expr.cpp expr_eq_fn.cpp for_each_fn.cpp +add_library(kernel OBJECT level.cpp expr.cpp expr_eq_fn.cpp for_each_fn.cpp replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp formatter.cpp declaration.cpp environment.cpp justification.cpp pos_info_provider.cpp metavar.cpp converter.cpp constraint.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp normalizer_extension.cpp init_module.cpp extension_context.cpp expr_cache.cpp default_converter.cpp equiv_manager.cpp) - -target_link_libraries(kernel ${LEAN_LIBS}) diff --git a/src/kernel/hits/CMakeLists.txt b/src/kernel/hits/CMakeLists.txt index f3a124757..6e447bec0 100644 --- a/src/kernel/hits/CMakeLists.txt +++ b/src/kernel/hits/CMakeLists.txt @@ -1,2 +1 @@ -add_library(hits hits.cpp) -target_link_libraries(hits ${LEAN_LIBS}) +add_library(hits OBJECT hits.cpp) diff --git a/src/kernel/inductive/CMakeLists.txt b/src/kernel/inductive/CMakeLists.txt index b284e7a69..4dbca65d2 100644 --- a/src/kernel/inductive/CMakeLists.txt +++ b/src/kernel/inductive/CMakeLists.txt @@ -1,2 +1 @@ -add_library(inductive inductive.cpp) -target_link_libraries(inductive ${LEAN_LIBS}) +add_library(inductive OBJECT inductive.cpp) diff --git a/src/kernel/quotient/CMakeLists.txt b/src/kernel/quotient/CMakeLists.txt index 831b8a6ce..d8d4daf57 100644 --- a/src/kernel/quotient/CMakeLists.txt +++ b/src/kernel/quotient/CMakeLists.txt @@ -1,2 +1 @@ -add_library(quotient quotient.cpp) -target_link_libraries(quotient ${LEAN_LIBS}) +add_library(quotient OBJECT quotient.cpp) diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 2ba750f68..b3a698a06 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -1,4 +1,4 @@ -add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp +add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp kernel_bindings.cpp io_state_stream.cpp bin_app.cpp constants.cpp resolve_macro.cpp kernel_serializer.cpp max_sharing.cpp normalize.cpp shared_environment.cpp module.cpp coercion.cpp @@ -16,5 +16,3 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp relation_manager.cpp export.cpp user_recursors.cpp class_instance_synth.cpp idx_metavar.cpp composition_manager.cpp tc_multigraph.cpp noncomputable.cpp) - -target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/definitional/CMakeLists.txt b/src/library/definitional/CMakeLists.txt index 569c27c5c..ea6a79208 100644 --- a/src/library/definitional/CMakeLists.txt +++ b/src/library/definitional/CMakeLists.txt @@ -1,5 +1,3 @@ -add_library(definitional rec_on.cpp induction_on.cpp cases_on.cpp +add_library(definitional OBJECT rec_on.cpp induction_on.cpp cases_on.cpp no_confusion.cpp projection.cpp brec_on.cpp equations.cpp init_module.cpp) - -target_link_libraries(definitional ${LEAN_LIBS}) diff --git a/src/library/error_handling/CMakeLists.txt b/src/library/error_handling/CMakeLists.txt index 5d540bfe1..967083526 100644 --- a/src/library/error_handling/CMakeLists.txt +++ b/src/library/error_handling/CMakeLists.txt @@ -1,2 +1 @@ -add_library(error_handling error_handling.cpp) -target_link_libraries(error_handling ${LEAN_LIBS}) +add_library(error_handling OBJECT error_handling.cpp) diff --git a/src/library/simplifier/CMakeLists.txt b/src/library/simplifier/CMakeLists.txt index aeaa1df5f..c5f2336f6 100644 --- a/src/library/simplifier/CMakeLists.txt +++ b/src/library/simplifier/CMakeLists.txt @@ -1,2 +1 @@ -add_library(simplifier ceqv.cpp simp_rule_set.cpp init_module.cpp simp_tactic.cpp) -target_link_libraries(simplifier ${LEAN_LIBS}) +add_library(simplifier OBJECT ceqv.cpp simp_rule_set.cpp init_module.cpp simp_tactic.cpp) diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 207610415..ed9bcac47 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,4 +1,4 @@ -add_library(tactic goal.cpp proof_state.cpp tactic.cpp elaborate.cpp +add_library(tactic OBJECT goal.cpp proof_state.cpp tactic.cpp elaborate.cpp apply_tactic.cpp intros_tactic.cpp rename_tactic.cpp trace_tactic.cpp exact_tactic.cpp generalize_tactic.cpp inversion_tactic.cpp whnf_tactic.cpp revert_tactic.cpp assert_tactic.cpp clear_tactic.cpp @@ -7,5 +7,3 @@ init_module.cpp change_tactic.cpp check_expr_tactic.cpp let_tactic.cpp contradiction_tactic.cpp exfalso_tactic.cpp constructor_tactic.cpp injection_tactic.cpp congruence_tactic.cpp relation_tactics.cpp induction_tactic.cpp subst_tactic.cpp unfold_rec.cpp with_options_tactic.cpp) - -target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index c5464424d..ccef8ec13 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -1,9 +1,9 @@ if(${EMSCRIPTEN}) add_executable(lean.js lean.cpp emscripten.cpp) - target_link_libraries(lean.js ${ALL_LIBS} "--embed-file library --memory-init-file 0") + target_link_libraries(lean.js leanstatic ${EXTRA_LIBS} "--embed-file library --memory-init-file 0") else() add_executable(lean lean.cpp emscripten.cpp) - target_link_libraries(lean ${ALL_LIBS}) + target_link_libraries(lean leanstatic ${EXTRA_LIBS}) ADD_CUSTOM_COMMAND(TARGET lean POST_BUILD COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin" @@ -12,8 +12,7 @@ else() install(TARGETS lean DESTINATION bin) endif() -add_library(shell emscripten.cpp) -target_link_libraries(shell ${LEAN_LIBS}) +add_library(shell OBJECT emscripten.cpp) # add_test(example1_stdin1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../tests/lean/single.lean") # add_test(example1_stdin2 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_CURRENT_BINARY_DIR}/lean "-l" "${LEAN_SOURCE_DIR}/../tests/lean/single.lean") diff --git a/src/tests/frontends/lean/CMakeLists.txt b/src/tests/frontends/lean/CMakeLists.txt index 294a7609d..ec6d12742 100644 --- a/src/tests/frontends/lean/CMakeLists.txt +++ b/src/tests/frontends/lean/CMakeLists.txt @@ -1,5 +1,5 @@ -add_executable(lean_scanner scanner.cpp) -target_link_libraries(lean_scanner "init" "lean_frontend" "library" "kernel" "util" ${EXTRA_LIBS}) +add_executable(lean_scanner scanner.cpp ${LEAN_OBJS}) +target_link_libraries(lean_scanner ${EXTRA_LIBS}) add_test(lean_scanner "${CMAKE_CURRENT_BINARY_DIR}/lean_scanner") # add_executable(lean_parser parser.cpp) # target_link_libraries(lean_parser ${ALL_LIBS}) diff --git a/src/tests/kernel/CMakeLists.txt b/src/tests/kernel/CMakeLists.txt index f1d4c04aa..db16fbdfa 100644 --- a/src/tests/kernel/CMakeLists.txt +++ b/src/tests/kernel/CMakeLists.txt @@ -1,24 +1,25 @@ -add_executable(level level.cpp) -target_link_libraries(level "library" "kernel" "util" ${EXTRA_LIBS}) +set(kernel_tst_objs $ $ $ $ $ $ $ $) +add_executable(level level.cpp ${kernel_tst_objs}) +target_link_libraries(level ${EXTRA_LIBS}) add_test(level "${CMAKE_CURRENT_BINARY_DIR}/level") -add_executable(expr expr.cpp) -target_link_libraries(expr "library" "kernel" "util" ${EXTRA_LIBS}) +add_executable(expr expr.cpp ${kernel_tst_objs}) +target_link_libraries(expr ${EXTRA_LIBS}) add_test(expr "${CMAKE_CURRENT_BINARY_DIR}/expr") -add_executable(max_sharing max_sharing.cpp) -target_link_libraries(max_sharing "kernel" "library" "util" ${EXTRA_LIBS}) +add_executable(max_sharing max_sharing.cpp ${kernel_tst_objs}) +target_link_libraries(max_sharing ${EXTRA_LIBS}) add_test(max_sharing "${CMAKE_CURRENT_BINARY_DIR}/max_sharing") -add_executable(free_vars free_vars.cpp) -target_link_libraries(free_vars "kernel" "util" ${EXTRA_LIBS}) +add_executable(free_vars free_vars.cpp ${kernel_tst_objs}) +target_link_libraries(free_vars ${EXTRA_LIBS}) add_test(free_vars "${CMAKE_CURRENT_BINARY_DIR}/free_vars") -add_executable(replace replace.cpp) -target_link_libraries(replace "library" "kernel" "util" ${EXTRA_LIBS}) +add_executable(replace replace.cpp ${kernel_tst_objs}) +target_link_libraries(replace ${EXTRA_LIBS}) add_test(replace "${CMAKE_CURRENT_BINARY_DIR}/replace") -add_executable(environment environment.cpp) -target_link_libraries(environment "library" "kernel" "util" ${EXTRA_LIBS}) +add_executable(environment environment.cpp ${kernel_tst_objs}) +target_link_libraries(environment ${EXTRA_LIBS}) add_test(environment "${CMAKE_CURRENT_BINARY_DIR}/environment") -add_executable(metavar metavar.cpp) -target_link_libraries(metavar "library" "kernel" "util" ${EXTRA_LIBS}) +add_executable(metavar metavar.cpp ${kernel_tst_objs}) +target_link_libraries(metavar ${EXTRA_LIBS}) add_test(metavar "${CMAKE_CURRENT_BINARY_DIR}/metavar") -add_executable(instantiate instantiate.cpp) -target_link_libraries(instantiate "kernel" "util" ${EXTRA_LIBS}) +add_executable(instantiate instantiate.cpp ${kernel_tst_objs}) +target_link_libraries(instantiate ${EXTRA_LIBS}) add_test(instantiate "${CMAKE_CURRENT_BINARY_DIR}/instantiate") diff --git a/src/tests/library/CMakeLists.txt b/src/tests/library/CMakeLists.txt index 0ca485062..a333d0801 100644 --- a/src/tests/library/CMakeLists.txt +++ b/src/tests/library/CMakeLists.txt @@ -1,15 +1,16 @@ -add_executable(expr_lt expr_lt.cpp) -target_link_libraries(expr_lt "library" "kernel" "util" ${EXTRA_LIBS}) +set(library_tst_objs $ $ $ $ $ $ $ $) +add_executable(expr_lt expr_lt.cpp ${library_tst_objs}) +target_link_libraries(expr_lt ${EXTRA_LIBS}) add_test(expr_lt "${CMAKE_CURRENT_BINARY_DIR}/expr_lt") -add_executable(deep_copy deep_copy.cpp) -target_link_libraries(deep_copy "library" "kernel" "util" ${EXTRA_LIBS}) +add_executable(deep_copy deep_copy.cpp ${library_tst_objs}) +target_link_libraries(deep_copy ${EXTRA_LIBS}) add_test(deep_copy "${CMAKE_CURRENT_BINARY_DIR}/deep_copy") -add_executable(occurs occurs.cpp) -target_link_libraries(occurs "library" "kernel" "util" ${EXTRA_LIBS}) +add_executable(occurs occurs.cpp ${library_tst_objs}) +target_link_libraries(occurs ${EXTRA_LIBS}) add_test(occurs "${CMAKE_CURRENT_BINARY_DIR}/occurs") -add_executable(unifier unifier.cpp) -target_link_libraries(unifier "library" "kernel" "util" ${EXTRA_LIBS}) +add_executable(unifier unifier.cpp ${library_tst_objs}) +target_link_libraries(unifier ${EXTRA_LIBS}) add_test(unifier "${CMAKE_CURRENT_BINARY_DIR}/unifier") -add_executable(head_map head_map.cpp) -target_link_libraries(head_map "library" "kernel" "util" ${EXTRA_LIBS}) +add_executable(head_map head_map.cpp ${library_tst_objs}) +target_link_libraries(head_map ${EXTRA_LIBS}) add_test(head_map "${CMAKE_CURRENT_BINARY_DIR}/head_map") diff --git a/src/tests/library/blast/CMakeLists.txt b/src/tests/library/blast/CMakeLists.txt index 973c7d350..1a8ede115 100644 --- a/src/tests/library/blast/CMakeLists.txt +++ b/src/tests/library/blast/CMakeLists.txt @@ -1,3 +1,3 @@ -add_executable(union_find union_find.cpp) -target_link_libraries(union_find "util" ${EXTRA_LIBS}) +add_executable(union_find union_find.cpp $) +target_link_libraries(union_find ${EXTRA_LIBS}) add_test(union_find "${CMAKE_CURRENT_BINARY_DIR}/union_find") diff --git a/src/tests/shell/CMakeLists.txt b/src/tests/shell/CMakeLists.txt index 1312b9b41..ebff0b92f 100644 --- a/src/tests/shell/CMakeLists.txt +++ b/src/tests/shell/CMakeLists.txt @@ -1,5 +1,5 @@ -add_executable(shell_test shell.cpp) -target_link_libraries(shell_test "init" "lean_frontend" "library" "kernel" "util" "shell" ${EXTRA_LIBS}) +add_executable(shell_test shell.cpp ${LEAN_OBJS} $) +target_link_libraries(shell_test ${EXTRA_LIBS}) add_test(NAME "emscripten_test" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/tests/shell" diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt index dfc3456e7..cb2a0b4e0 100644 --- a/src/tests/util/CMakeLists.txt +++ b/src/tests/util/CMakeLists.txt @@ -1,93 +1,93 @@ -add_executable(name name.cpp) -target_link_libraries(name "util" ${EXTRA_LIBS}) +add_executable(name name.cpp $) +target_link_libraries(name ${EXTRA_LIBS}) add_test(name "${CMAKE_CURRENT_BINARY_DIR}/name") -add_executable(sequence sequence.cpp) -target_link_libraries(sequence "util" ${EXTRA_LIBS}) +add_executable(sequence sequence.cpp $) +target_link_libraries(sequence ${EXTRA_LIBS}) add_test(sequence "${CMAKE_CURRENT_BINARY_DIR}/sequence") -add_executable(sexpr_tst sexpr.cpp) -target_link_libraries(sexpr_tst "util" "numerics" "sexpr" ${EXTRA_LIBS}) +add_executable(sexpr_tst sexpr.cpp $ $ $) +target_link_libraries(sexpr_tst ${EXTRA_LIBS}) add_test(sexpr "${CMAKE_CURRENT_BINARY_DIR}/sexpr_tst") -add_executable(format format.cpp) -target_link_libraries(format "util" "numerics" "sexpr" ${EXTRA_LIBS}) +add_executable(format format.cpp $ $ $) +target_link_libraries(format ${EXTRA_LIBS}) add_test(format "${CMAKE_CURRENT_BINARY_DIR}/format") -add_executable(buffer buffer.cpp) -target_link_libraries(buffer "util" ${EXTRA_LIBS}) +add_executable(buffer buffer.cpp $) +target_link_libraries(buffer ${EXTRA_LIBS}) add_test(buffer "${CMAKE_CURRENT_BINARY_DIR}/buffer") -add_executable(list list.cpp) -target_link_libraries(list "util" ${EXTRA_LIBS}) +add_executable(list list.cpp $) +target_link_libraries(list ${EXTRA_LIBS}) add_test(list "${CMAKE_CURRENT_BINARY_DIR}/list") -add_executable(scoped_set scoped_set.cpp) -target_link_libraries(scoped_set "util" ${EXTRA_LIBS}) +add_executable(scoped_set scoped_set.cpp $) +target_link_libraries(scoped_set ${EXTRA_LIBS}) add_test(scoped_set "${CMAKE_CURRENT_BINARY_DIR}/scoped_set") -add_executable(options options.cpp) -target_link_libraries(options "util" "numerics" "sexpr" ${EXTRA_LIBS}) +add_executable(options options.cpp $ $ $) +target_link_libraries(options ${EXTRA_LIBS}) add_test(options "${CMAKE_CURRENT_BINARY_DIR}/options") -add_executable(scoped_map scoped_map.cpp) -target_link_libraries(scoped_map "util" ${EXTRA_LIBS}) +add_executable(scoped_map scoped_map.cpp $) +target_link_libraries(scoped_map ${EXTRA_LIBS}) add_test(scoped_map "${CMAKE_CURRENT_BINARY_DIR}/scoped_map") -add_executable(memory memory.cpp) -target_link_libraries(memory "util" ${EXTRA_LIBS}) +add_executable(memory memory.cpp $) +target_link_libraries(memory ${EXTRA_LIBS}) add_test(memory "${CMAKE_CURRENT_BINARY_DIR}/memory") -add_executable(rb_tree rb_tree.cpp) -target_link_libraries(rb_tree "util" ${EXTRA_LIBS}) +add_executable(rb_tree rb_tree.cpp $) +target_link_libraries(rb_tree ${EXTRA_LIBS}) add_test(rb_tree "${CMAKE_CURRENT_BINARY_DIR}/rb_tree") -add_executable(rb_map rb_map.cpp) -target_link_libraries(rb_map "util" ${EXTRA_LIBS}) +add_executable(rb_map rb_map.cpp $) +target_link_libraries(rb_map ${EXTRA_LIBS}) add_test(rb_map "${CMAKE_CURRENT_BINARY_DIR}/rb_map") -add_executable(splay_tree splay_tree.cpp) -target_link_libraries(splay_tree "util" ${EXTRA_LIBS}) +add_executable(splay_tree splay_tree.cpp $) +target_link_libraries(splay_tree ${EXTRA_LIBS}) add_test(splay_tree "${CMAKE_CURRENT_BINARY_DIR}/splay_tree") -add_executable(splay_map splay_map.cpp) -target_link_libraries(splay_map "util" ${EXTRA_LIBS}) +add_executable(splay_map splay_map.cpp $) +target_link_libraries(splay_map ${EXTRA_LIBS}) add_test(splay_map "${CMAKE_CURRENT_BINARY_DIR}/splay_map") -add_executable(trace trace.cpp) -target_link_libraries(trace "util" ${EXTRA_LIBS}) +add_executable(trace trace.cpp $) +target_link_libraries(trace ${EXTRA_LIBS}) add_test(trace "${CMAKE_CURRENT_BINARY_DIR}/trace") -add_executable(exception exception.cpp) -target_link_libraries(exception "util" ${EXTRA_LIBS}) +add_executable(exception exception.cpp $) +target_link_libraries(exception ${EXTRA_LIBS}) add_test(exception "${CMAKE_CURRENT_BINARY_DIR}/exception") -add_executable(bit_tricks bit_tricks.cpp) -target_link_libraries(bit_tricks "util" ${EXTRA_LIBS}) +add_executable(bit_tricks bit_tricks.cpp $) +target_link_libraries(bit_tricks ${EXTRA_LIBS}) add_test(bit_tricks "${CMAKE_CURRENT_BINARY_DIR}/bit_tricks") -add_executable(lazy_list lazy_list.cpp) -target_link_libraries(lazy_list "util" "numerics" ${EXTRA_LIBS}) +add_executable(lazy_list lazy_list.cpp $ $) +target_link_libraries(lazy_list ${EXTRA_LIBS}) add_test(lazy_list "${CMAKE_CURRENT_BINARY_DIR}/lazy_list") -add_executable(hash hash.cpp) -target_link_libraries(hash "util" ${EXTRA_LIBS}) +add_executable(hash hash.cpp $) +target_link_libraries(hash ${EXTRA_LIBS}) add_test(hash "${CMAKE_CURRENT_BINARY_DIR}/hash") -add_executable(safe_arith safe_arith.cpp) -target_link_libraries(safe_arith "util" ${EXTRA_LIBS}) +add_executable(safe_arith safe_arith.cpp $) +target_link_libraries(safe_arith ${EXTRA_LIBS}) add_test(safe_arith "${CMAKE_CURRENT_BINARY_DIR}/safe_arith") -add_executable(set set.cpp) -target_link_libraries(set "util" ${EXTRA_LIBS}) +add_executable(set set.cpp $) +target_link_libraries(set ${EXTRA_LIBS}) add_test(set "${CMAKE_CURRENT_BINARY_DIR}/set") -add_executable(optional optional.cpp) -target_link_libraries(optional "util" ${EXTRA_LIBS}) +add_executable(optional optional.cpp $) +target_link_libraries(optional ${EXTRA_LIBS}) add_test(optional "${CMAKE_CURRENT_BINARY_DIR}/optional") -add_executable(stackinfo stackinfo.cpp) -target_link_libraries(stackinfo "util" ${EXTRA_LIBS}) +add_executable(stackinfo stackinfo.cpp $) +target_link_libraries(stackinfo ${EXTRA_LIBS}) add_test(stackinfo "${CMAKE_CURRENT_BINARY_DIR}/stackinfo") -add_executable(serializer serializer.cpp) -target_link_libraries(serializer "util" ${EXTRA_LIBS}) +add_executable(serializer serializer.cpp $) +target_link_libraries(serializer ${EXTRA_LIBS}) add_test(serializer "${CMAKE_CURRENT_BINARY_DIR}/serializer") -add_executable(trie trie.cpp) -target_link_libraries(trie "util" ${EXTRA_LIBS}) +add_executable(trie trie.cpp $) +target_link_libraries(trie ${EXTRA_LIBS}) add_test(trie "${CMAKE_CURRENT_BINARY_DIR}/trie") -add_executable(lru_cache lru_cache.cpp) -target_link_libraries(lru_cache "util" ${EXTRA_LIBS}) +add_executable(lru_cache lru_cache.cpp $) +target_link_libraries(lru_cache ${EXTRA_LIBS}) add_test(lru_cache "${CMAKE_CURRENT_BINARY_DIR}/lru_cache") -add_executable(worker_queue worker_queue.cpp) -target_link_libraries(worker_queue "util" ${EXTRA_LIBS}) +add_executable(worker_queue worker_queue.cpp $) +target_link_libraries(worker_queue ${EXTRA_LIBS}) add_test(worker_queue "${CMAKE_CURRENT_BINARY_DIR}/worker_queue") # thread.cpp used import_test.lua add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/import_test.lua" COMMAND "${CMAKE_COMMAND}" -E copy "${CMAKE_CURRENT_SOURCE_DIR}/import_test.lua" "${CMAKE_CURRENT_BINARY_DIR}/import_test.lua" DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/import_test.lua") add_custom_target("import_test" DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/import_test.lua") -add_executable(thread thread.cpp) -target_link_libraries(thread "util" ${EXTRA_LIBS}) +add_executable(thread thread.cpp $) +target_link_libraries(thread ${EXTRA_LIBS}) add_test(thread "${CMAKE_CURRENT_BINARY_DIR}/thread") add_dependencies(thread import_test) -add_executable(bitap_fuzzy_search bitap_fuzzy_search.cpp) -target_link_libraries(bitap_fuzzy_search "util" ${EXTRA_LIBS}) +add_executable(bitap_fuzzy_search bitap_fuzzy_search.cpp $) +target_link_libraries(bitap_fuzzy_search ${EXTRA_LIBS}) add_test(bitap_fuzzy_search "${CMAKE_CURRENT_BINARY_DIR}/bitap_fuzzy_search") diff --git a/src/tests/util/interval/CMakeLists.txt b/src/tests/util/interval/CMakeLists.txt index 66ecf6017..3037973b1 100644 --- a/src/tests/util/interval/CMakeLists.txt +++ b/src/tests/util/interval/CMakeLists.txt @@ -1,15 +1,15 @@ -add_executable(interval_tst interval.cpp) -target_link_libraries(interval_tst "interval" "numerics" "util" ${EXTRA_LIBS}) +add_executable(interval_tst interval.cpp $ $ $) +target_link_libraries(interval_tst ${EXTRA_LIBS}) add_test(basic_interval "${CMAKE_CURRENT_BINARY_DIR}/interval_tst") -add_executable(float_interval_tst float_interval.cpp) -target_link_libraries(float_interval_tst "interval" "numerics" "util" ${EXTRA_LIBS}) +add_executable(float_interval_tst float_interval.cpp $ $ $) +target_link_libraries(float_interval_tst ${EXTRA_LIBS}) add_test(float_interval "${CMAKE_CURRENT_BINARY_DIR}/float_interval_tst") -add_executable(double_interval_tst double_interval.cpp) -target_link_libraries(double_interval_tst "interval" "numerics" "util" ${EXTRA_LIBS}) +add_executable(double_interval_tst double_interval.cpp $ $ $) +target_link_libraries(double_interval_tst ${EXTRA_LIBS}) add_test(double_interval "${CMAKE_CURRENT_BINARY_DIR}/double_interval_tst") -add_executable(mpfp_interval_tst mpfp_interval.cpp) -target_link_libraries(mpfp_interval_tst "interval" "numerics" "util" ${EXTRA_LIBS}) +add_executable(mpfp_interval_tst mpfp_interval.cpp $ $ $) +target_link_libraries(mpfp_interval_tst ${EXTRA_LIBS}) add_test(mpfp_interval "${CMAKE_CURRENT_BINARY_DIR}/mpfp_interval_tst") diff --git a/src/tests/util/memory.cpp b/src/tests/util/memory.cpp index ec47a6858..efef8db78 100644 --- a/src/tests/util/memory.cpp +++ b/src/tests/util/memory.cpp @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #include #include "util/test.h" -#include "util/memory.cpp" +#include "util/memory.h" static void tst1() { std::cout << "Initial: " << lean::get_allocated_memory() << "\n"; diff --git a/src/tests/util/numerics/CMakeLists.txt b/src/tests/util/numerics/CMakeLists.txt index 905bdef9e..c5c1e0bd3 100644 --- a/src/tests/util/numerics/CMakeLists.txt +++ b/src/tests/util/numerics/CMakeLists.txt @@ -1,33 +1,33 @@ -add_executable(mpq mpq.cpp) -target_link_libraries(mpq "numerics" "util" ${EXTRA_LIBS}) +add_executable(mpq mpq.cpp $ $ $) +target_link_libraries(mpq ${EXTRA_LIBS}) add_test(mpq "${CMAKE_CURRENT_BINARY_DIR}/mpq") -add_executable(mpbq mpbq.cpp) -target_link_libraries(mpbq "numerics" "util" ${EXTRA_LIBS}) +add_executable(mpbq mpbq.cpp $ $ $) +target_link_libraries(mpbq ${EXTRA_LIBS}) add_test(mpbq "${CMAKE_CURRENT_BINARY_DIR}/mpbq") -add_executable(mpfp mpfp.cpp) -target_link_libraries(mpfp "numerics" "util" ${EXTRA_LIBS}) +add_executable(mpfp mpfp.cpp $ $ $) +target_link_libraries(mpfp ${EXTRA_LIBS}) add_test(mpfp "${CMAKE_CURRENT_BINARY_DIR}/mpfp") -add_executable(mpz mpz.cpp) -target_link_libraries(mpz "numerics" "util" ${EXTRA_LIBS}) +add_executable(mpz mpz.cpp $ $ $) +target_link_libraries(mpz ${EXTRA_LIBS}) add_test(mpz "${CMAKE_CURRENT_BINARY_DIR}/mpz") -add_executable(double double.cpp) -target_link_libraries(double "numerics" "util" ${EXTRA_LIBS}) +add_executable(double double.cpp $ $ $) +target_link_libraries(double ${EXTRA_LIBS}) add_test(double "${CMAKE_CURRENT_BINARY_DIR}/double") -add_executable(float float.cpp) -target_link_libraries(float "numerics" "util" ${EXTRA_LIBS}) +add_executable(float float.cpp $ $ $) +target_link_libraries(float ${EXTRA_LIBS}) add_test(float "${CMAKE_CURRENT_BINARY_DIR}/float") -add_executable(xnumeral xnumeral.cpp) -target_link_libraries(xnumeral "numerics" "util" ${EXTRA_LIBS}) +add_executable(xnumeral xnumeral.cpp $ $ $) +target_link_libraries(xnumeral ${EXTRA_LIBS}) add_test(xnumeral "${CMAKE_CURRENT_BINARY_DIR}/xnumeral") -add_executable(primes primes.cpp) -target_link_libraries(primes "numerics" "util" ${EXTRA_LIBS}) +add_executable(primes primes.cpp $ $ $) +target_link_libraries(primes ${EXTRA_LIBS}) add_test(primes "${CMAKE_CURRENT_BINARY_DIR}/primes") -add_executable(numeric_traits numeric_traits.cpp) -target_link_libraries(numeric_traits "numerics" "util" ${EXTRA_LIBS}) +add_executable(numeric_traits numeric_traits.cpp $ $ $) +target_link_libraries(numeric_traits ${EXTRA_LIBS}) add_test(numeric_traits "${CMAKE_CURRENT_BINARY_DIR}/numeric_traits") -add_executable(gcd gcd.cpp) -target_link_libraries(gcd "numerics" "util" ${EXTRA_LIBS}) +add_executable(gcd gcd.cpp $ $ $) +target_link_libraries(gcd ${EXTRA_LIBS}) add_test(gcd "${CMAKE_CURRENT_BINARY_DIR}/gcd") -add_executable(zpz zpz.cpp) -target_link_libraries(zpz "numerics" "util" ${EXTRA_LIBS}) +add_executable(zpz zpz.cpp $ $ $) +target_link_libraries(zpz ${EXTRA_LIBS}) add_test(zpz "${CMAKE_CURRENT_BINARY_DIR}/zpz") diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 2982f2112..57f8f3e22 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -1,9 +1,7 @@ -add_library(util trace.cpp debug.cpp name.cpp name_set.cpp +add_library(util OBJECT trace.cpp debug.cpp name.cpp name_set.cpp name_generator.cpp exception.cpp interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp safe_arith.cpp ascii.cpp memory.cpp shared_mutex.cpp realpath.cpp script_state.cpp script_exception.cpp rb_map.cpp lua.cpp luaref.cpp lua_named_param.cpp stackinfo.cpp lean_path.cpp serializer.cpp lbool.cpp thread_script_state.cpp bitap_fuzzy_search.cpp init_module.cpp thread.cpp memory_pool.cpp utf8.cpp name_map.cpp list_fn.cpp) - -target_link_libraries(util ${LEAN_LIBS}) diff --git a/src/util/interval/CMakeLists.txt b/src/util/interval/CMakeLists.txt index cf4e38049..bba3ca26c 100644 --- a/src/util/interval/CMakeLists.txt +++ b/src/util/interval/CMakeLists.txt @@ -1,2 +1 @@ -add_library(interval interval_instances.cpp) -target_link_libraries(interval ${LEAN_LIBS}) +add_library(interval OBJECT interval_instances.cpp) diff --git a/src/util/numerics/CMakeLists.txt b/src/util/numerics/CMakeLists.txt index da4fe1e09..2006ed0ee 100644 --- a/src/util/numerics/CMakeLists.txt +++ b/src/util/numerics/CMakeLists.txt @@ -1,4 +1,2 @@ -add_library(numerics init_module.cpp mpz.cpp mpq.cpp mpbq.cpp mpfp.cpp +add_library(numerics OBJECT init_module.cpp mpz.cpp mpq.cpp mpbq.cpp mpfp.cpp float.cpp double.cpp numeric_traits.cpp primes.cpp zpz.cpp) - -target_link_libraries(numerics ${LEAN_LIBS} ${EXTRA_LIBS}) diff --git a/src/util/sexpr/CMakeLists.txt b/src/util/sexpr/CMakeLists.txt index a323bb190..c2a1fa07e 100644 --- a/src/util/sexpr/CMakeLists.txt +++ b/src/util/sexpr/CMakeLists.txt @@ -1,4 +1,2 @@ -add_library(sexpr sexpr.cpp sexpr_fn.cpp format.cpp options.cpp +add_library(sexpr OBJECT sexpr.cpp sexpr_fn.cpp format.cpp options.cpp option_declarations.cpp init_module.cpp) - -target_link_libraries(sexpr ${LEAN_LIBS})