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

fix(build): fix Cygwin build

Browse Source
This commit is contained in:
Nuno Lopes
2018-01-22 16:54:33 +00:00
committed by Leonardo de Moura
parent eff960d498
commit 0d820fa23d
5 changed files with 8 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
.gitignore vendored
View File

@@ -10,6 +10,7 @@ GSYMS
GTAGS
.projectile
.lean_options
.vs
src/emacs/dependencies
compile_commands.json
*.idea

3
src/CMakeLists.txt
View File

@@ -1,4 +1,5 @@
cmake_minimum_required(VERSION 2.8.7)
cmake_policy(SET CMP0054 NEW)
project(LEAN CXX C)
set(LEAN_VERSION_MAJOR 3)
set(LEAN_VERSION_MINOR 3)
@@ -135,7 +136,7 @@ if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
endif()
if("${CYGWIN}" EQUAL "1")
set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_CYGWIN")
set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_CYGWIN -D _GNU_SOURCE")
endif()
if(JSON)

2
src/library/native_compiler/dynamic_library.cpp
View File

@@ -8,7 +8,7 @@ Author: Jared Roesch
#include <string>
// Interacting with dynamic linking is *not* cross-platform, this is my first
// attempt at supporting all platforms.
#if !defined (LEAN_WINDOWS)
#if !defined (LEAN_WINDOWS) || defined(LEAN_CYGWIN)
#include <dlfcn.h>
#endif
#include "util/exception.h"

2
src/tests/util/lp/lp.cpp
View File

@@ -1513,7 +1513,7 @@ void test_out_dir(string out_dir) {
DIR *out_dir_p = opendir(out_dir.c_str());
if (out_dir_p == nullptr) {
cout << "creating directory " << out_dir << std::endl;
#ifdef LEAN_WINDOWS
#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
int res = mkdir(out_dir.c_str());
#else
int res = mkdir(out_dir.c_str(), S_IRWXU | S_IRWXG | S_IROTH | S_IXOTH);

6
src/util/file_lock.cpp
View File

@@ -11,7 +11,7 @@ Author: Leonardo de Moura
#include "util/sstream.h"
#include "util/file_lock.h"
#ifdef LEAN_WINDOWS
#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
#include <windows.h>
#include <io.h>
#define LOCK_SH 1 /* shared lock */
@@ -96,13 +96,13 @@ file_lock::file_lock(char const * fname, bool exclusive):
file_lock::~file_lock() {
#if !defined(LEAN_EMSCRIPTEN)
if (m_fd != -1) {
#if !defined(LEAN_WINDOWS)
#if !defined(LEAN_WINDOWS) || defined(LEAN_CYGWIN)
/* On Windows, we cannot remove the file if it is locked. */
std::remove(m_fname.c_str());
#endif
flock(m_fd, LOCK_UN);
close(m_fd);
#if defined(LEAN_WINDOWS)
#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
/* On Windows, we (to) to remove the file after we released the lock. The operation will fail if another
process has a handle to it. However, this is better than always keeping all .lock files. */
std::remove(m_fname.c_str());