From 59b5a4a07ac53412f8352f94b3f29b2578c13ad2 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 23 Jan 2018 14:06:54 +0000 Subject: [PATCH] feat(build): add preliminary MSVC support Still doesn't build fully, but at least Intellisense sort of works now --- .gitignore | 1 + doc/make/index.md | 1 + doc/make/msvc.md | 34 +++++++++++++ src/CMakeLists.txt | 27 ++++++++-- src/cmake/Modules/FindGMP.cmake | 2 +- src/util/debug.h | 88 ++++++++++++++++++--------------- src/util/name.cpp | 1 + src/util/name.h | 6 +++ 8 files changed, 114 insertions(+), 46 deletions(-) create mode 100644 doc/make/msvc.md diff --git a/.gitignore b/.gitignore index 9a754b5138..3297b4537f 100644 --- a/.gitignore +++ b/.gitignore @@ -20,3 +20,4 @@ settings.json .vscode /*.nix /library/init/version.lean +CMakeSettings.json diff --git a/doc/make/index.md b/doc/make/index.md index 7aa0ef26e6..7add68a687 100644 --- a/doc/make/index.md +++ b/doc/make/index.md @@ -10,6 +10,7 @@ Platform-Specific Setup - [Linux (Ubuntu)](ubuntu-16.04.md) - [Windows (msys2)](msys2.md) +- [Windows (Visual Studio)](doc/make/msvc.md) - [macOS](osx-10.9.md) Generic Build Instructions diff --git a/doc/make/msvc.md b/doc/make/msvc.md new file mode 100644 index 0000000000..756e2adfc3 --- /dev/null +++ b/doc/make/msvc.md @@ -0,0 +1,34 @@ +Compiling Lean with Visual Studio +--------------------------------- + +WARNING: Compiling Lean with Visual Studio doesn't currently work. +There's an ongoing effort to port Lean to Visual Studio. +The instructions below are for VS 2017. + + +## Installing dependencies + +First, install `vcpkg` from https://github.com/Microsoft/vcpkg if you haven't +done so already. +Then, open a console in the directory you cloned `vcpkg` to, and type: +`vcpkg install mpir` for the 32-bit library or +`vcpkg install mpir:x64-windows` for the x64 one. + +In Visual Studio, use the "open folder" feature and open the Lean directory. +Go to the `CMake->Change CMake Settings` menu. File `CMakeSettings.json` opens. +In each of the targets, add the following snippet (i.e., after every +`ctestCommandArgs`): + +```json + "variables": [ + { + "name": "CMAKE_TOOLCHAIN_FILE", + "value": "C:\\path\\to\\vcpkg\\scripts\\buildsystems\\vcpkg.cmake" + } + ] +``` + + +## Build Lean + +Press F7. diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c43dc0e657..b16ee7c61a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -186,11 +186,11 @@ endif() set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules") # Initialize CXXFLAGS. -set(CMAKE_CXX_FLAGS "-Wall -Wextra -std=c++11 ${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\"") -set(CMAKE_CXX_FLAGS_DEBUG "-g3 -DLEAN_DEBUG -DLEAN_TRACE") -set(CMAKE_CXX_FLAGS_MINSIZEREL "-Os -DNDEBUG") -set(CMAKE_CXX_FLAGS_RELEASE "-O3 -DNDEBUG") -set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g3 -DLEAN_DEBUG") +set(CMAKE_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\"") +set(CMAKE_CXX_FLAGS_DEBUG "-DLEAN_DEBUG -DLEAN_TRACE") +set(CMAKE_CXX_FLAGS_MINSIZEREL "-DNDEBUG") +set(CMAKE_CXX_FLAGS_RELEASE "-DNDEBUG") +set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-DLEAN_DEBUG") set(CMAKE_CXX_FLAGS_GPROF "-O2 -g -pg") # OSX .dmg generation (this is working in progress) @@ -241,12 +241,29 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -stdlib=libc++") set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -stdlib=libc++") endif () +elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "MSVC") + # All good. Maybe enforce a recent version? + set(IS_MSVC 1) + set(CMAKE_CXX_FLAGS "/GL /EHsc /W1 ${CMAKE_CXX_FLAGS}") + set(CMAKE_CXX_FLAGS_DEBUG "/Od ${CMAKE_CXX_FLAGS_DEBUG}") + set(CMAKE_CXX_FLAGS_MINSIZEREL "/Os ${CMAKE_CXX_FLAGS_MINSIZEREL}") + set(CMAKE_CXX_FLAGS_RELEASE "/O2 /Oi /Oy ${CMAKE_CXX_FLAGS_RELEASE}") + set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "/O2 /Oi ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}") + set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} /LCTG") elseif (EMSCRIPTEN) message(STATUS "Emscripten is detected: Make sure the wraped compiler supports C++11") else() message(FATAL_ERROR "Unsupported compiler: ${CMAKE_CXX_COMPILER_ID}") endif () +if (NOT DEFINED IS_MSVC) + set(CMAKE_CXX_FLAGS "-Wall -Wextra -std=c++11 ${CMAKE_CXX_FLAGS}") + set(CMAKE_CXX_FLAGS_DEBUG "-g3 ${CMAKE_CXX_FLAGS_DEBUG}") + set(CMAKE_CXX_FLAGS_MINSIZEREL "-Os ${CMAKE_CXX_FLAGS_MINSIZEREL}") + set(CMAKE_CXX_FLAGS_RELEASE "-O3 ${CMAKE_CXX_FLAGS_RELEASE}") + set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g3 ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}") +endif () + if (EMSCRIPTEN) include(ExternalProject) set(gmp_install_prefix ${CMAKE_CURRENT_BINARY_DIR}/gmp-root) diff --git a/src/cmake/Modules/FindGMP.cmake b/src/cmake/Modules/FindGMP.cmake index 795c2cdcde..9300547eff 100644 --- a/src/cmake/Modules/FindGMP.cmake +++ b/src/cmake/Modules/FindGMP.cmake @@ -4,7 +4,7 @@ if (GMP_INCLUDE_DIR AND GMP_LIBRARIES) endif (GMP_INCLUDE_DIR AND GMP_LIBRARIES) find_path(GMP_INCLUDE_DIR NAMES gmp.h ) -find_library(GMP_LIBRARIES NAMES gmp libgmp REQUIRED) +find_library(GMP_LIBRARIES NAMES gmp libgmp mpir REQUIRED) #find_library(GMPXX_LIBRARIES NAMES gmpxx libgmpxx ) #MESSAGE(STATUS "GMP: " ${GMP_LIBRARIES}) # " " ${GMPXX_LIBRARIES} ) diff --git a/src/util/debug.h b/src/util/debug.h index 6ab6b9f939..204c28aa2c 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -34,58 +34,66 @@ Author: Leonardo de Moura #define LEAN_COMMASEQ_N() 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0 #define LEAN_RSEQ_N() 17, 16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0 #define LEAN_ARG_N(_1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, N, ...) N -#define LEAN_NARG_(ARGS...) LEAN_ARG_N(ARGS) -#define LEAN_HASCOMMA(ARGS...) LEAN_NARG_(ARGS, LEAN_COMMASEQ_N()) +#define LEAN_EXPAND(x) x +#ifdef _MSC_VER +#define LEAN_AUGMENT(...) dummy, __VA_ARGS__ +#define LEAN_NARG_1(...) LEAN_EXPAND(LEAN_ARG_N(__VA_ARGS__, 16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0)) +#define LEAN_NARG(...) LEAN_NARG_1(LEAN_AUGMENT(__VA_ARGS__)) +#else +#define LEAN_NARG_(...) LEAN_ARG_N(__VA_ARGS__) +#define LEAN_HASCOMMA(...) LEAN_NARG_(__VA_ARGS__, LEAN_COMMASEQ_N()) #define LEAN_COMMA() , #define LEAN_NARG_HELPER3_01(N) 0 #define LEAN_NARG_HELPER3_00(N) 1 #define LEAN_NARG_HELPER3_11(N) N #define LEAN_NARG_HELPER2(a, b, N) LEAN_NARG_HELPER3_ ## a ## b(N) #define LEAN_NARG_HELPER1(a, b, N) LEAN_NARG_HELPER2(a, b, N) -#define LEAN_NARG(ARGS...) LEAN_NARG_HELPER1(LEAN_HASCOMMA(ARGS), LEAN_HASCOMMA(LEAN_COMMA ARGS ()), LEAN_NARG_(ARGS, LEAN_RSEQ_N())) +#define LEAN_NARG(...) LEAN_NARG_HELPER1(LEAN_HASCOMMA(ARGS), LEAN_HASCOMMA(LEAN_COMMA __VA_ARGS__ ()), LEAN_NARG_(__VA_ARGS__, LEAN_RSEQ_N())) +#endif // Hack for LEAN_DISPLAY(ARGS...) // It works for at most 16 arguments. -#define LEAN_DISPLAY1_CORE(V) lean::debug::display_var(#V, V); -#define LEAN_DISPLAY2_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY1_CORE(REST); -#define LEAN_DISPLAY3_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY2_CORE(REST); -#define LEAN_DISPLAY4_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY3_CORE(REST); -#define LEAN_DISPLAY5_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY4_CORE(REST); -#define LEAN_DISPLAY6_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY5_CORE(REST); -#define LEAN_DISPLAY7_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY6_CORE(REST); -#define LEAN_DISPLAY8_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY7_CORE(REST); -#define LEAN_DISPLAY9_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY8_CORE(REST); -#define LEAN_DISPLAY10_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY9_CORE(REST); -#define LEAN_DISPLAY11_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY10_CORE(REST); -#define LEAN_DISPLAY12_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY11_CORE(REST); -#define LEAN_DISPLAY13_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY12_CORE(REST); -#define LEAN_DISPLAY14_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY13_CORE(REST); -#define LEAN_DISPLAY15_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY14_CORE(REST); -#define LEAN_DISPLAY16_CORE(V, REST...) lean::debug::display_var(#V, V); LEAN_DISPLAY15_CORE(REST); -#define LEAN_DISPLAY0() -#define LEAN_DISPLAY1(ARG) std::cerr << "Argument\n"; LEAN_DISPLAY1_CORE(ARG); -#define LEAN_DISPLAY2(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY2_CORE(ARGS); -#define LEAN_DISPLAY3(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY3_CORE(ARGS); -#define LEAN_DISPLAY4(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY4_CORE(ARGS); -#define LEAN_DISPLAY5(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY5_CORE(ARGS); -#define LEAN_DISPLAY6(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY6_CORE(ARGS); -#define LEAN_DISPLAY7(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY7_CORE(ARGS); -#define LEAN_DISPLAY8(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY8_CORE(ARGS); -#define LEAN_DISPLAY9(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY9_CORE(ARGS); -#define LEAN_DISPLAY10(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY10_CORE(ARGS); -#define LEAN_DISPLAY11(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY11_CORE(ARGS); -#define LEAN_DISPLAY12(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY12_CORE(ARGS); -#define LEAN_DISPLAY13(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY13_CORE(ARGS); -#define LEAN_DISPLAY14(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY14_CORE(ARGS); -#define LEAN_DISPLAY15(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY15_CORE(ARGS); -#define LEAN_DISPLAY16(ARGS...) std::cerr << "Arguments\n"; LEAN_DISPLAY16_CORE(ARGS); +#define EX(...) __VA_ARGS__ +#define LEAN_DISPLAY1_CORE(V) lean::debug::display_var(#V, V); +#define LEAN_DISPLAY2_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_DISPLAY1_CORE(__VA_ARGS__); +#define LEAN_DISPLAY3_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_DISPLAY2_CORE(__VA_ARGS__); +#define LEAN_DISPLAY4_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_DISPLAY3_CORE(__VA_ARGS__); +#define LEAN_DISPLAY5_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_DISPLAY4_CORE(__VA_ARGS__); +#define LEAN_DISPLAY6_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_DISPLAY5_CORE(__VA_ARGS__); +#define LEAN_DISPLAY7_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_DISPLAY6_CORE(__VA_ARGS__); +#define LEAN_DISPLAY8_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_DISPLAY7_CORE(__VA_ARGS__); +#define LEAN_DISPLAY9_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_DISPLAY8_CORE(__VA_ARGS__); +#define LEAN_DISPLAY10_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_DISPLAY9_CORE(__VA_ARGS__); +#define LEAN_DISPLAY11_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_DISPLAY10_CORE(__VA_ARGS__); +#define LEAN_DISPLAY12_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_DISPLAY11_CORE(__VA_ARGS__); +#define LEAN_DISPLAY13_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_DISPLAY12_CORE(__VA_ARGS__); +#define LEAN_DISPLAY14_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_DISPLAY13_CORE(__VA_ARGS__); +#define LEAN_DISPLAY15_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_DISPLAY14_CORE(__VA_ARGS__); +#define LEAN_DISPLAY16_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_DISPLAY15_CORE(__VA_ARGS__); +#define LEAN_DISPLAY0(...) +#define LEAN_DISPLAY1(ARG) std::cerr << "Argument\n"; LEAN_DISPLAY1_CORE(ARG); +#define LEAN_DISPLAY2(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY2_CORE(__VA_ARGS__)); +#define LEAN_DISPLAY3(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY3_CORE(__VA_ARGS__)); +#define LEAN_DISPLAY4(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY4_CORE(__VA_ARGS__)); +#define LEAN_DISPLAY5(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY5_CORE(__VA_ARGS__)); +#define LEAN_DISPLAY6(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY6_CORE(__VA_ARGS__)); +#define LEAN_DISPLAY7(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY7_CORE(__VA_ARGS__)); +#define LEAN_DISPLAY8(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY8_CORE(__VA_ARGS__)); +#define LEAN_DISPLAY9(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY9_CORE(__VA_ARGS__)); +#define LEAN_DISPLAY10(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY10_CORE(__VA_ARGS__)); +#define LEAN_DISPLAY11(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY11_CORE(__VA_ARGS__)); +#define LEAN_DISPLAY12(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY12_CORE(__VA_ARGS__)); +#define LEAN_DISPLAY13(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY13_CORE(__VA_ARGS__)); +#define LEAN_DISPLAY14(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY14_CORE(__VA_ARGS__)); +#define LEAN_DISPLAY15(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY15_CORE(__VA_ARGS__)); +#define LEAN_DISPLAY16(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY16_CORE(__VA_ARGS__)); #define LEAN_JOIN0(A, B) A ## B #define LEAN_JOIN(A, B) LEAN_JOIN0(A, B) -#define LEAN_DISPLAY(ARGS...) { LEAN_JOIN(LEAN_DISPLAY, LEAN_NARG(ARGS))(ARGS) } +#define LEAN_DISPLAY(...) { LEAN_JOIN(LEAN_DISPLAY, LEAN_NARG(__VA_ARGS__))(__VA_ARGS__) } -#define lean_assert(COND, ARGS...) DEBUG_CODE({if (LEAN_UNLIKELY(!(COND))) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(ARGS); lean::invoke_debugger(); }}) -#define lean_cond_assert(TAG, COND, ARGS...) DEBUG_CODE({if (lean::is_debug_enabled(TAG) && LEAN_UNLIKELY(!(COND))) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(ARGS); lean::invoke_debugger(); }}) -#define lean_always_assert(COND, ARGS...) { if (LEAN_UNLIKELY(!(COND))) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(ARGS); lean_unreachable(); } } +#define lean_assert(COND, ...) DEBUG_CODE({if (LEAN_UNLIKELY(!(COND))) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(__VA_ARGS__); lean::invoke_debugger(); }}) +#define lean_cond_assert(TAG, COND, ...) DEBUG_CODE({if (lean::is_debug_enabled(TAG) && LEAN_UNLIKELY(!(COND))) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(__VA_ARGS__); lean::invoke_debugger(); }}) +#define lean_always_assert(COND, ...) { if (LEAN_UNLIKELY(!(COND))) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(__VA_ARGS__); lean_unreachable(); } } #define lean_assert_eq(A, B) lean_assert(A == B, A, B) #define lean_assert_ne(A, B) lean_assert(A != B, A, B) diff --git a/src/util/name.cpp b/src/util/name.cpp index 32789097cf..0c84e9d5e6 100644 --- a/src/util/name.cpp +++ b/src/util/name.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include #include #include diff --git a/src/util/name.h b/src/util/name.h index 7ca7730e10..6bd5eec971 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -18,8 +18,14 @@ Author: Leonardo de Moura namespace lean { constexpr char const * lean_name_separator = "."; +#ifdef _MSC_VER +constexpr char16_t id_begin_escape = L'«'; +constexpr char16_t id_end_escape = L'»'; + +#else constexpr char16_t id_begin_escape = u'«'; constexpr char16_t id_end_escape = u'»'; +#endif bool is_id_first(char const * begin, char const * end); inline bool is_id_first(unsigned char const * begin, unsigned char const * end) {