feat: patches for compiling on FreeBSD

- excised some code in `util/memory`; to be reimplemented
jlpaca · May 24, 2020 · d679a73 · d679a73
1 parent 0947586
commit d679a73
Show file tree

Hide file tree

Showing 4 changed files with 33 additions and 9 deletions.
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -185,7 +185,7 @@ endif()
 
 if(STATIC)
   message(STATUS "Creating a static executable")
-  if (MULTI_THREAD AND ${CMAKE_SYSTEM_NAME} MATCHES "Linux")
+  if (MULTI_THREAD AND ${CMAKE_SYSTEM_NAME} MATCHES "Linux|FreeBSD")
     set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -Wl,--whole-archive -lpthread -lrt -Wl,--no-whole-archive")
   endif()
   set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -static")
@@ -216,7 +216,7 @@ if (NOT DEFINED CMAKE_MACOSX_RPATH)
   set(CMAKE_MACOSX_RPATH 0)
 endif()
 
-if (${CMAKE_SYSTEM_NAME} MATCHES "Linux")
+if (${CMAKE_SYSTEM_NAME} MATCHES "Linux|FreeBSD")
   # The following options is needed to generate a shared library
   set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fPIC")
 endif()
@@ -598,7 +598,7 @@ if(NOT (${GIT_SHA1} MATCHES "GITDIR-NOTFOUND"))
   set(CPACK_PACKAGE_VERSION "${CPACK_PACKAGE_VERSION}.git${GIT_SHA1}")
 endif()
 set(CPACK_PACKAGE_FILE_NAME "lean-${LEAN_VERSION_STRING}-${LOWER_SYSTEM_NAME}")
-if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
+if(${CMAKE_SYSTEM_NAME} MATCHES "Linux|FreeBSD")
   SET(CPACK_GENERATOR TGZ)
 else()
   SET(CPACK_GENERATOR ZIP)

diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp
@@ -27,7 +27,7 @@ Author: Leonardo de Moura
 #else
     #include <unistd.h>
 #endif
-#if defined(__linux__) || defined(__APPLE__) || defined(LEAN_EMSCRIPTEN)
+#if defined(__linux__) || defined(__APPLE__) || defined(__FreeBSD__) || defined(LEAN_EMSCRIPTEN)
     #include <sys/socket.h>
     #include <sys/un.h>
     #define SOCKET int
@@ -483,7 +483,7 @@ static vm_obj fs_rename(vm_obj const & p1, vm_obj const & p2, vm_obj const &) {
 }
 
 int mkdir_single(const char *path) {
-#if defined(__linux__) || defined(__APPLE__) || defined(LEAN_EMSCRIPTEN)
+#if defined(__linux__) || defined(__APPLE__) || defined(__FreeBSD__) || defined(LEAN_EMSCRIPTEN)
     return mkdir(path, 0777);
 #else
     return !CreateDirectoryA(path, NULL);
@@ -539,7 +539,7 @@ static vm_obj fs_mkdir(vm_obj const & _path, vm_obj const & rec, vm_obj const &)
 
 static vm_obj fs_rmdir(vm_obj const & path, vm_obj const &) {
     bool res;
-#if defined(__linux__) || defined(__APPLE__) || defined(LEAN_EMSCRIPTEN)
+#if defined(__linux__) || defined(__APPLE__) || defined(__FreeBSD__) || defined(LEAN_EMSCRIPTEN)
     res = !rmdir(to_string(path).c_str());
 #else
     res = RemoveDirectoryA(to_string(path).c_str());
@@ -918,7 +918,7 @@ vm_obj monad_io_random_impl() {
 }
 
 void initialize_vm_io() {
-#if !(defined(__linux__) || defined(__APPLE__) || defined(LEAN_EMSCRIPTEN))
+#if !(defined(__linux__) || defined(__APPLE__) || defined(__FreeBSD__) || defined(LEAN_EMSCRIPTEN))
     WSADATA wsaData;
     int err = WSAStartup(MAKEWORD(2, 2), &wsaData);
     if (err != 0) {

diff --git a/src/util/memory.cpp b/src/util/memory.cpp
@@ -91,6 +91,8 @@ size_t get_current_rss() {
     if (task_info(mach_task_self(), MACH_TASK_BASIC_INFO, reinterpret_cast<task_info_t>(&info), &infoCount) != KERN_SUCCESS)
         return static_cast<size_t>(0);
     return static_cast<size_t>(info.resident_size);
+#elif defined(__FreeBSD__)
+    return 0; // TODO: implement this.
 #else
     long rss  = 0;
     FILE * fp = nullptr;

diff --git a/src/util/path.cpp b/src/util/path.cpp
@@ -72,15 +72,37 @@ std::string get_exe_location() {
     return std::string(buf2);
 }
 bool is_path_sep(char c) { return c == g_path_sep; }
-#else
-// Linux version
+#elif defined(__FreeBSD__)
+// FreeBSD version
 #include <unistd.h>
+#include <sys/types.h>
+#include <sys/sysctl.h>
 #include <string.h>
 #include <limits.h> // NOLINT
 #include <stdio.h>
 static char g_path_sep     = ':';
 static constexpr char g_sep          = '/';
 static char g_bad_sep      = '\\';
+std::string get_exe_location() {
+  char dest[PATH_MAX];
+  memset(dest, 0, PATH_MAX);
+  size_t cb = sizeof(dest);
+  int mib[4] = { CTL_KERN, KERN_PROC, KERN_PROC_PATHNAME, -1 };
+  if (sysctl(mib, 4, dest, &cb, NULL, 0) == -1) {
+        throw exception("failed to locate Lean executable location");
+  }
+  return std::string(dest);
+}
+bool is_path_sep(char c) { return c == g_path_sep; }
+#else
+// Linux version
+#include <unistd.h> // NOLINT
+#include <string.h> // NOLINT
+#include <limits.h> // NOLINT
+#include <stdio.h>  // NOLINT
+static char g_path_sep     = ':';
+static constexpr char g_sep          = '/';
+static char g_bad_sep      = '\\';
 std::string get_exe_location() {
     char path[PATH_MAX];
     char dest[PATH_MAX];