michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add support for cygwin

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-10 14:15:13 -07:00
parent 03461df55e
commit f79c0d3546
11 changed files with 62 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/CMakeLists.txt
View file

@ -6,6 +6,14 @@ set(LEAN_VERSION_MINOR 1)
set(CMAKE_COLOR_MAKEFILE ON)
enable_testing()
set(LEAN_EXTRA_LINKER_FLAGS "")
# Cygwin: Windows does not support ulimit -s unlimited. So, we reserve a lot of stack space: 100Mb
if(${CYGWIN})
message("-- CYGWIN detected")
set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -Wl,--stack,104857600")
endif()
# Set Module Path
set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules/")
@ -59,20 +67,21 @@ include_directories(${LEAN_SOURCE_DIR}/parsers)
include_directories(${LEAN_SOURCE_DIR}/frontend)
add_subdirectory(util)
set(EXTRA_LIBS ${EXTRA_LIBS} util)
set(LEAN_LIBS ${LEAN_LIBS} util)
add_subdirectory(util/numerics)
set(EXTRA_LIBS ${EXTRA_LIBS} numerics)
set(LEAN_LIBS ${LEAN_LIBS} numerics)
add_subdirectory(interval)
set(EXTRA_LIBS ${EXTRA_LIBS} interval)
set(LEAN_LIBS ${LEAN_LIBS} interval)
add_subdirectory(kernel)
set(EXTRA_LIBS ${EXTRA_LIBS} kernel)
set(LEAN_LIBS ${LEAN_LIBS} kernel)
add_subdirectory(kernel/arith)
set(EXTRA_LIBS ${EXTRA_LIBS} kernel_arith)
set(LEAN_LIBS ${LEAN_LIBS} kernel_arith)
add_subdirectory(frontend)
set(EXTRA_LIBS ${EXTRA_LIBS} frontend)
set(LEAN_LIBS ${LEAN_LIBS} frontend)
add_subdirectory(parsers)
set(EXTRA_LIBS ${EXTRA_LIBS} parser_common)
set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread")
set(LEAN_LIBS ${LEAN_LIBS} parser_common)
set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINKER_FLAGS}")
set(EXTRA_LIBS ${LEAN_LIBS} ${EXTRA_LIBS})
add_subdirectory(shell)
add_subdirectory(tests/util)
add_subdirectory(tests/util/numerics)

2
src/frontend/CMakeLists.txt
View file

@ -1,2 +1,2 @@
add_library(frontend frontend.cpp)
target_link_libraries(frontend ${EXTRA_LIBS})
target_link_libraries(frontend ${LEAN_LIBS})

3
src/interval/CMakeLists.txt
View file

@ -1,2 +1,3 @@
add_library(interval interval.cpp)
target_link_libraries(interval ${EXTRA_LIBS})
target_link_libraries(interval ${LEAN_LIBS})

2
src/kernel/CMakeLists.txt
View file

@ -2,4 +2,4 @@ add_library(kernel expr.cpp max_sharing.cpp free_vars.cpp abstract.cpp
instantiate.cpp deep_copy.cpp normalize.cpp level.cpp environment.cpp
type_check.cpp context.cpp builtin.cpp basic_thms.cpp toplevel.cpp
pp.cpp)
target_link_libraries(kernel ${EXTRA_LIBS})
target_link_libraries(kernel ${LEAN_LIBS})

2
src/kernel/arith/CMakeLists.txt
View file

@ -1,2 +1,2 @@
add_library(kernel_arith arith.cpp)
target_link_libraries(kernel_arith ${EXTRA_LIBS})
target_link_libraries(kernel_arith ${LEAN_LIBS})

2
src/parsers/CMakeLists.txt
View file

@ -1,2 +1,2 @@
add_library(parser_common scanner.cpp)
target_link_libraries(parser_common ${EXTRA_LIBS})
target_link_libraries(parser_common ${LEAN_LIBS})

1
src/parsers/scanner.cpp
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <cstdio>
#include "scanner.h"
#include "debug.h"

2
src/tests/interval/interval.cpp
View file

@ -17,7 +17,7 @@ typedef interval<double> di;
typedef interval<mpfp> fi;
typedef std::vector<qi> qiv;
qiv mk_some_intervals(int low, int hi) {
static qiv mk_some_intervals(int low, int hi) {
qiv r;
for (unsigned lo = 0; lo < 2; lo++)
for (unsigned uo = 0; uo < 2; uo++)

1
src/util/numerics/CMakeLists.txt
View file

@ -1 +1,2 @@
add_library(numerics gmp_init.cpp mpz.cpp mpq.cpp mpbq.cpp mpfp.cpp float.cpp double.cpp numeric_traits.cpp)
target_link_libraries(numerics ${LEAN_LIBS} ${EXTRA_LIBS})

11
src/util/numerics/double.cpp
View file

@ -10,7 +10,16 @@ Author: Soonho Kong
namespace lean {
thread_local mpfr_rnd_t numeric_traits<double>::rnd = MPFR_RNDN;
static thread_local mpfr_rnd_t g_rnd;
void set_double_rnd(bool plus_inf) {
g_rnd = plus_inf ? MPFR_RNDU : MPFR_RNDD;
}
mpfr_rnd_t get_double_rnd() {
return g_rnd;
}
void double_power(double & v, unsigned k) {
v = std::pow(v, k);

49
src/util/numerics/double.h
View file

@ -23,15 +23,18 @@ void double_power(double & v, unsigned k);
t.f(rnd); \
v = t.get_double(rnd);
void set_double_rnd(bool plus_inf);
mpfr_rnd_t get_double_rnd();
template<>
class numeric_traits<double> {
public:
static thread_local mpfr_rnd_t rnd;
static bool precise() { return false; }
static bool is_zero(double v) { return v == 0.0; }
static bool is_pos(double v) { return v > 0.0; }
static bool is_neg(double v) { return v < 0.0; }
static void set_rounding(bool plus_inf) { rnd = plus_inf ? MPFR_RNDU : MPFR_RNDD; }
static mpfr_rnd_t rnd() { return get_double_rnd(); }
static void set_rounding(bool plus_inf) { set_double_rnd(plus_inf); }
static void neg(double & v) { v = -v; }
static void inv(double & v) { v = 1.0/v; }
static void reset(double & v) { v = 0.0; }
@ -53,26 +56,26 @@ public:
static inline double pi_twice_upper() { return pi_u * 2; }
// Transcendental functions using MPFR
static void exp(double & v) { LEAN_TRANS_DOUBLE_FUNC(exp, v, rnd); }
static void exp2(double & v) { LEAN_TRANS_DOUBLE_FUNC(exp2, v, rnd); }
static void exp10(double & v) { LEAN_TRANS_DOUBLE_FUNC(exp10, v, rnd); }
static void log(double & v) { LEAN_TRANS_DOUBLE_FUNC(log, v, rnd); }
static void log2(double & v) { LEAN_TRANS_DOUBLE_FUNC(log2, v, rnd); }
static void log10(double & v) { LEAN_TRANS_DOUBLE_FUNC(log10, v, rnd); }
static void sin(double & v) { LEAN_TRANS_DOUBLE_FUNC(sin, v, rnd); }
static void cos(double & v) { LEAN_TRANS_DOUBLE_FUNC(cos, v, rnd); }
static void tan(double & v) { LEAN_TRANS_DOUBLE_FUNC(tan, v, rnd); }
static void sec(double & v) { LEAN_TRANS_DOUBLE_FUNC(sec, v, rnd); }
static void csc(double & v) { LEAN_TRANS_DOUBLE_FUNC(csc, v, rnd); }
static void cot(double & v) { LEAN_TRANS_DOUBLE_FUNC(cot, v, rnd); }
static void asin(double & v) { LEAN_TRANS_DOUBLE_FUNC(asin, v, rnd); }
static void acos(double & v) { LEAN_TRANS_DOUBLE_FUNC(acos, v, rnd); }
static void atan(double & v) { LEAN_TRANS_DOUBLE_FUNC(atan, v, rnd); }
static void sinh(double & v) { LEAN_TRANS_DOUBLE_FUNC(sinh, v, rnd); }
static void cosh(double & v) { LEAN_TRANS_DOUBLE_FUNC(cosh, v, rnd); }
static void tanh(double & v) { LEAN_TRANS_DOUBLE_FUNC(tanh, v, rnd); }
static void asinh(double & v) { LEAN_TRANS_DOUBLE_FUNC(asinh, v, rnd); }
static void acosh(double & v) { LEAN_TRANS_DOUBLE_FUNC(acosh, v, rnd); }
static void atanh(double & v) { LEAN_TRANS_DOUBLE_FUNC(atanh, v, rnd); }
static void exp(double & v) { LEAN_TRANS_DOUBLE_FUNC(exp, v, rnd()); }
static void exp2(double & v) { LEAN_TRANS_DOUBLE_FUNC(exp2, v, rnd()); }
static void exp10(double & v) { LEAN_TRANS_DOUBLE_FUNC(exp10, v, rnd()); }
static void log(double & v) { LEAN_TRANS_DOUBLE_FUNC(log, v, rnd()); }
static void log2(double & v) { LEAN_TRANS_DOUBLE_FUNC(log2, v, rnd()); }
static void log10(double & v) { LEAN_TRANS_DOUBLE_FUNC(log10, v, rnd()); }
static void sin(double & v) { LEAN_TRANS_DOUBLE_FUNC(sin, v, rnd()); }
static void cos(double & v) { LEAN_TRANS_DOUBLE_FUNC(cos, v, rnd()); }
static void tan(double & v) { LEAN_TRANS_DOUBLE_FUNC(tan, v, rnd()); }
static void sec(double & v) { LEAN_TRANS_DOUBLE_FUNC(sec, v, rnd()); }
static void csc(double & v) { LEAN_TRANS_DOUBLE_FUNC(csc, v, rnd()); }
static void cot(double & v) { LEAN_TRANS_DOUBLE_FUNC(cot, v, rnd()); }
static void asin(double & v) { LEAN_TRANS_DOUBLE_FUNC(asin, v, rnd()); }
static void acos(double & v) { LEAN_TRANS_DOUBLE_FUNC(acos, v, rnd()); }
static void atan(double & v) { LEAN_TRANS_DOUBLE_FUNC(atan, v, rnd()); }
static void sinh(double & v) { LEAN_TRANS_DOUBLE_FUNC(sinh, v, rnd()); }
static void cosh(double & v) { LEAN_TRANS_DOUBLE_FUNC(cosh, v, rnd()); }
static void tanh(double & v) { LEAN_TRANS_DOUBLE_FUNC(tanh, v, rnd()); }
static void asinh(double & v) { LEAN_TRANS_DOUBLE_FUNC(asinh, v, rnd()); }
static void acosh(double & v) { LEAN_TRANS_DOUBLE_FUNC(acosh, v, rnd()); }
static void atanh(double & v) { LEAN_TRANS_DOUBLE_FUNC(atanh, v, rnd()); }
};
}