From e0c23e598480b9bb93261b8fcab2f569fb9cd7a2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 18 Nov 2013 09:52:47 -0800
Subject: [PATCH] fix(kernel/environment): compilation problem on Windows

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/CMakeLists.txt         |  4 ++++
 src/kernel/environment.cpp |  3 ++-
 src/util/CMakeLists.txt    |  2 +-
 src/util/name.h            |  1 +
 src/util/realpath.cpp      | 32 ++++++++++++++++++++++++++++++++
 src/util/realpath.h        | 11 +++++++++++
 6 files changed, 51 insertions(+), 2 deletions(-)
 create mode 100644 src/util/realpath.cpp
 create mode 100644 src/util/realpath.h

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