fix(kernel/environment): compilation problem on Windows

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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

src/kernel/environment.cpp

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include <unordered_map>
 #include <mutex>
 #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) {

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)

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

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 <iostream>
+#include <cstdlib>
+#include "util/realpath.h"
+#ifdef LEAN_WINDOWS
+#include <windows.h>
+#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
+}
+}

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 <string>
+namespace lean {
+std::string realpath(char const * fname);
+}