diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 98603c1e1..0051662b3 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -24,6 +24,10 @@ if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows")) set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_DEFAULT_PP_UNICODE=false") endif() +if(${CMAKE_SYSTEM_NAME} MATCHES "Windows") + set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_WINDOWS") +endif() + if("${THREAD_SAFE}" MATCHES "OFF") message(STATUS "Disabled thread-safety, it will not be safe to run multiple threads in parallel") set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_THREAD_UNSAFE") diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 62e0c74e6..ea700bfdd 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include #include #include "util/safe_arith.h" +#include "util/realpath.h" #include "kernel/for_each.h" #include "kernel/kernel_exception.h" #include "kernel/environment.h" @@ -426,7 +427,7 @@ struct environment::imp { } bool mark_imported(char const * fname, environment const & env) { - return mark_imported_core(name(realpath(fname, nullptr)), env); + return mark_imported_core(name(realpath(fname)), env); } bool mark_builtin_imported(char const * id, environment const & env) { diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 6f6fcb2c1..54e5c3319 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -1,3 +1,3 @@ add_library(util trace.cpp debug.cpp name.cpp exception.cpp interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp safe_arith.cpp - ascii.cpp memory.cpp shared_mutex.cpp) + ascii.cpp memory.cpp shared_mutex.cpp realpath.cpp) diff --git a/src/util/name.h b/src/util/name.h index e50d4af5d..c551478d8 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -26,6 +26,7 @@ class name { public: name(); name(char const * name); + name(std::string const & s):name(s.c_str()) {} name(name const & prefix, char const * name); name(name const & prefix, unsigned k); name(name const & other); diff --git a/src/util/realpath.cpp b/src/util/realpath.cpp new file mode 100644 index 000000000..aa7463980 --- /dev/null +++ b/src/util/realpath.cpp @@ -0,0 +1,32 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include +#include "util/realpath.h" +#ifdef LEAN_WINDOWS +#include +#endif + +namespace lean { +std::string realpath(char const * fname) { +#ifdef LEAN_WINDOWS + constexpr unsigned buffer_size = 8192; + char buffer[buffer_size]; + DWORD retval = GetFullPathName(fname, buffer_size, buffer, nullptr); + if (retval == 0 || retval > buffer_size) { + return std::string(fname); + } else { + return std::string(buffer); + } +#else + char * tmp = ::realpath(fname, nullptr); + std::string r(tmp); + free(tmp); + return r; +#endif +} +} diff --git a/src/util/realpath.h b/src/util/realpath.h new file mode 100644 index 000000000..c7c8735eb --- /dev/null +++ b/src/util/realpath.h @@ -0,0 +1,11 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +namespace lean { +std::string realpath(char const * fname); +}