sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

feat(build): add preliminary MSVC support

Browse Source 
Still doesn't build fully, but at least Intellisense sort of works now
This commit is contained in:
Nuno Lopes
2018-01-23 14:06:54 +00:00
committed by Leonardo de Moura
parent fe2e95def3
commit 59b5a4a07a
8 changed files with 114 additions and 46 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
.gitignore vendored
View File

@@ -20,3 +20,4 @@ settings.json
.vscode
/*.nix
/library/init/version.lean
CMakeSettings.json

1
doc/make/index.md
View File

@@ -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

34
doc/make/msvc.md Normal file
View File

@@ -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.

27
src/CMakeLists.txt
View File

@@ -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)

2
src/cmake/Modules/FindGMP.cmake
View File

@@ -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} )

88
src/util/debug.h
View File

@@ -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)

1
src/util/name.cpp
View File

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <cctype>
#include <cstring>
#include <vector>
#include <algorithm>

6
src/util/name.h
View File

@@ -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) {