max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove cygwin support

Browse source
This commit is contained in:
Sebastian Ullrich 2019-11-12 15:26:51 +01:00 • committed by Leonardo de Moura
parent 60620360fc
commit ae3b3bb825
10 changed files with 22 additions and 39 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
lean4-mode/lean4-settings.el
View file

@ -21,7 +21,6 @@
(defvar-local lean4-default-executable-name
(cl-case system-type
('windows-nt "lean.exe")
('cygwin "lean.exe")
(t "lean_wrapped"))
"Default executable name of Lean")

17
src/CMakeLists.txt
View file

@ -194,7 +194,7 @@ configure_file("${LEAN_SOURCE_DIR}/CTestCustom.cmake.in"
"${LEAN_BINARY_DIR}/CTestCustom.cmake" @ONLY)
# Windows does not support ulimit -s unlimited. So, we reserve a lot of stack space: 100Mb
if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
message(STATUS "Windows detected")
set(LEAN_WIN_STACK_SIZE "104857600")
if (MSVC)
@ -210,10 +210,6 @@ else()
set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -pthread -fPIC")
endif()
if("${CYGWIN}" EQUAL "1")
set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_CYGWIN -D _GNU_SOURCE")
endif()
if(JSON)
set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_JSON")
else()
@ -370,15 +366,8 @@ else()
find_package(GMP 5.0.5 REQUIRED)
include_directories(${GMP_INCLUDE_DIR})
set(COPY_LIBS ${COPY_LIBS} ${GMP_LIBRARIES})
endif()
# DL
if (EMSCRIPTEN)
# no dlopen
elseif((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
# TODO(Jared): config dlopen windows support
else()
set(EXTRA_LIBS ${EXTRA_LIBS} ${CMAKE_DL_LIBS})
# dlopen
set(EXTRA_LIBS ${EXTRA_LIBS} ${CMAKE_DL_LIBS})
endif()
# TRACK_MEMORY_USAGE

2
src/library/handle.cpp
View file

@ -11,7 +11,7 @@ Author: Leonardo de Moura & Jared Roesch
#include <utility>
#include <stdio.h>
#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
#if defined(LEAN_WINDOWS)
#include <windows.h>
#include <tchar.h>
#include <strsafe.h>

6
src/library/pipe.cpp
View file

@ -7,16 +7,14 @@ Author: Jared Roesch
#include "runtime/exception.h"
#include "library/pipe.h"
#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
#else
#if !defined(LEAN_WINDOWS)
#include <unistd.h>
#endif
namespace lean {
pipe::pipe() {
#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
#else
#if !defined(LEAN_WINDOWS)
int fds[2];
if (::pipe(fds) == -1) {
throw exception("unable to create pipe");

7
src/library/pipe.h
View file

@ -9,15 +9,13 @@ Author: Jared Roesch
#include <iostream>
#include <string>
#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
#if defined(LEAN_WINDOWS)
typedef void* HANDLE;
#else
#endif
namespace lean {
#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
#if defined(LEAN_WINDOWS)
struct pipe {
HANDLE m_read_fd;
HANDLE m_write_fd;
@ -37,7 +35,6 @@ struct pipe {
pipe(pipe const & p) :
m_read_fd(p.m_read_fd), m_write_fd(p.m_write_fd) {}
};
#endif
}

4
src/library/process.cpp
View file

@ -10,7 +10,7 @@ Author: Jared Roesch
#include <iomanip>
#include <utility>
#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
#if defined(LEAN_WINDOWS)
#include <windows.h>
#include <Fcntl.h>
#include <io.h>
@ -48,7 +48,7 @@ process & process::set_env(std::string const & var, optional<std::string> const
return *this;
}
#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
#if defined(LEAN_WINDOWS)
struct windows_child : public child {
handle_ref m_stdin;

6
src/runtime/debug.cpp
View file

@ -13,7 +13,7 @@ Author: Leonardo de Moura
#if defined(LEAN_EMSCRIPTEN)
#include <emscripten.h>
#endif
#if !defined(LEAN_WINDOWS) || defined(LEAN_CYGWIN)
#if !defined(LEAN_WINDOWS)
// Support for pid
#include<unistd.h>
#endif
@ -90,7 +90,7 @@ void invoke_debugger() {
for (;;) {
if (std::cin.eof())
debuggable_exit();
#if !defined(LEAN_WINDOWS) || defined(LEAN_CYGWIN)
#if !defined(LEAN_WINDOWS)
std::cerr << "(C)ontinue, (A)bort/exit, (S)top/trap\n";
#else
std::cerr << "(C)ontinue, (A)bort/exit, (S)top/trap, Invoke (G)DB\n";
@ -110,7 +110,7 @@ void invoke_debugger() {
case 's':
// force seg fault...
debuggable_exit();
#if !defined(LEAN_WINDOWS) || defined(LEAN_CYGWIN)
#if !defined(LEAN_WINDOWS)
case 'G':
case 'g': {
std::cerr << "INVOKING GDB...\n";

6
src/runtime/io.cpp
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
#if defined(LEAN_WINDOWS)
#include <windows.h>
#elif defined(__APPLE__)
#include <mach-o/dyld.h>
@ -167,7 +167,7 @@ extern "C" obj_res lean_io_getenv(b_obj_arg env_var, obj_arg) {
extern "C" obj_res lean_io_realpath(obj_arg fname, obj_arg) {
#if defined(LEAN_EMSCRIPTEN)
return set_io_result(fname);
#elif defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
#elif defined(LEAN_WINDOWS)
constexpr unsigned BufferSize = 8192;
char buffer[BufferSize];
DWORD retval = GetFullPathName(string_cstr(fname), BufferSize, buffer, nullptr);
@ -214,7 +214,7 @@ extern "C" obj_res lean_io_file_exists(b_obj_arg fname, obj_arg) {
}
extern "C" obj_res lean_io_app_dir(obj_arg) {
#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
#if defined(LEAN_WINDOWS)
HMODULE hModule = GetModuleHandleW(NULL);
WCHAR path[MAX_PATH];
GetModuleFileNameW(hModule, path, MAX_PATH);

6
src/util/file_lock.cpp
View file

@ -11,7 +11,7 @@ Author: Leonardo de Moura
#include "runtime/sstream.h"
#include "util/file_lock.h"
#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
#if defined(LEAN_WINDOWS)
#include <windows.h>
#include <io.h>
#define LOCK_SH 1 /* shared lock */
@ -97,13 +97,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) || defined(LEAN_CYGWIN)
#if !defined(LEAN_WINDOWS)
/* 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) && !defined(LEAN_CYGWIN)
#if defined(LEAN_WINDOWS)
/* 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());

6
src/util/path.cpp
View file

@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura, Gabriel Ebner
*/
#include "util/path.h"
#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
#if defined(LEAN_WINDOWS)
#include <windows.h>
#endif
#include <string>
@ -36,7 +36,7 @@ static char g_path_sep = ':';
static constexpr char g_sep = '/';
static char g_bad_sep = '\\';
bool is_path_sep(char c) { return c == g_path_sep; }
#elif defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
#elif defined(LEAN_WINDOWS)
// Windows version
static char g_path_sep = ';';
static constexpr char g_sep = '\\';
@ -223,7 +223,7 @@ std::vector<std::string> read_dir(std::string const &dirname) {
std::string lrealpath(std::string const & fname) {
#if defined(LEAN_EMSCRIPTEN)
return fname;
#elif defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
#elif defined(LEAN_WINDOWS)
constexpr unsigned BufferSize = 8192;
char buffer[BufferSize];
DWORD retval = GetFullPathName(fname.c_str(), BufferSize, buffer, nullptr);