-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Showing
8 changed files
with
192 additions
and
22 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,24 @@ | ||
| diff --git a/CMakeLists.txt b/CMakeLists.txt | ||
| index e4d4aaeda..c604ba989 100644 | ||
| --- a/CMakeLists.txt | ||
| +++ b/CMakeLists.txt | ||
| @@ -238,19 +238,6 @@ if (WIN32) | ||
| set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,--stack,100000000") | ||
| endif () | ||
|
|
||
| -#-----------------------------------------------------------------------------# | ||
| -# Use ld.gold if available | ||
| - | ||
| -execute_process(COMMAND ${CMAKE_C_COMPILER} | ||
| - -fuse-ld=gold | ||
| - -Wl,--version ERROR_QUIET OUTPUT_VARIABLE LD_VERSION) | ||
| -if ("${LD_VERSION}" MATCHES "GNU gold") | ||
| - string(APPEND CMAKE_EXE_LINKER_FLAGS " -fuse-ld=gold") | ||
| - string(APPEND CMAKE_SHARED_LINKER_FLAGS " -fuse-ld=gold") | ||
| - string(APPEND CMAKE_MODULE_LINKER_FLAGS " -fuse-ld=gold") | ||
| - message(STATUS "Using GNU gold linker.") | ||
| -endif () | ||
| - | ||
| #-----------------------------------------------------------------------------# | ||
| # Option defaults (three-valued options (cvc4_option(...))) | ||
| # |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,82 @@ | ||
| diff --git a/configure.sh b/configure.sh | ||
| index 21a444082..8b30c8b14 100755 | ||
| --- a/configure.sh | ||
| +++ b/configure.sh | ||
| @@ -23,6 +23,7 @@ General options; | ||
| --best turn on dependencies known to give best performance | ||
| --gpl permit GPL dependencies, if available | ||
| --win64 cross-compile for Windows 64 bit | ||
| + --win64-native natively compile for Windows 64 bit | ||
| --ninja use Ninja build system | ||
|
|
||
|
|
||
| @@ -146,6 +147,7 @@ ubsan=default | ||
| unit_testing=default | ||
| valgrind=default | ||
| win64=default | ||
| +win64_native=default | ||
|
|
||
| language_bindings_java=default | ||
| language_bindings_python=default | ||
| @@ -238,6 +240,9 @@ do | ||
| --win64) win64=ON;; | ||
| --no-win64) win64=OFF;; | ||
|
|
||
| + --win64-native) win64_native=ON;; | ||
| + --no-win64-native) win64_native=OFF;; | ||
| + | ||
| --ninja) ninja=ON;; | ||
|
|
||
| --glpk) glpk=ON;; | ||
| @@ -387,6 +392,9 @@ cmake_opts="" | ||
| && cmake_opts="$cmake_opts -DENABLE_GPL=$gpl" | ||
| [ $win64 != default ] \ | ||
| && cmake_opts="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-mingw64.cmake" | ||
| +# Because 'MSYS Makefiles' has a space in it, we set the variable vs. adding to 'cmake_opts' | ||
| +[ $win64_native != default ] \ | ||
| + && [ $ninja == default ] && export CMAKE_GENERATOR="MSYS Makefiles" | ||
| [ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja" | ||
| [ $muzzle != default ] \ | ||
| && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle" | ||
| diff --git a/src/expr/mkexpr b/src/expr/mkexpr | ||
| index c5f12f487..b47c66753 100755 | ||
| --- a/src/expr/mkexpr | ||
| +++ b/src/expr/mkexpr | ||
| @@ -14,6 +14,9 @@ | ||
| # | ||
| # Output is to standard out. | ||
| # | ||
| +# Required to disable this option for bash >=5.2 to avoid automatically | ||
| +# replacing & by the substituted text. | ||
| +shopt | grep -q '^patsub_replacement\b' && shopt -u patsub_replacement | ||
|
|
||
| copyright=2010-2014 | ||
|
|
||
| diff --git a/src/expr/mkkind b/src/expr/mkkind | ||
| index fbf37eff4..aabc70afe 100755 | ||
| --- a/src/expr/mkkind | ||
| +++ b/src/expr/mkkind | ||
| @@ -13,6 +13,9 @@ | ||
| # | ||
| # Output is to standard out. | ||
| # | ||
| +# Required to disable this option for bash >=5.2 to avoid automatically | ||
| +# replacing & by the substituted text. | ||
| +shopt | grep -q '^patsub_replacement\b' && shopt -u patsub_replacement | ||
|
|
||
| copyright=2010-2014 | ||
|
|
||
| diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind | ||
| index e2a733ec8..e56d076d7 100755 | ||
| --- a/src/expr/mkmetakind | ||
| +++ b/src/expr/mkmetakind | ||
| @@ -16,6 +16,9 @@ | ||
| # | ||
| # Output is to standard out. | ||
| # | ||
| +# Required to disable this option for bash >=5.2 to avoid automatically | ||
| +# replacing & by the substituted text. | ||
| +shopt | grep -q '^patsub_replacement\b' && shopt -u patsub_replacement | ||
|
|
||
| copyright=2010-2014 | ||
|
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,24 @@ | ||
| diff --git a/CMakeLists.txt b/CMakeLists.txt | ||
| index bbd49612a..fb9b416f9 100644 | ||
| --- a/CMakeLists.txt | ||
| +++ b/CMakeLists.txt | ||
| @@ -229,19 +229,6 @@ if (WIN32) | ||
| add_check_c_cxx_flag("-Wno-error=unknown-pragmas") | ||
| endif () | ||
|
|
||
| -#-----------------------------------------------------------------------------# | ||
| -# Use ld.gold if available | ||
| - | ||
| -execute_process(COMMAND ${CMAKE_C_COMPILER} | ||
| - -fuse-ld=gold | ||
| - -Wl,--version ERROR_QUIET OUTPUT_VARIABLE LD_VERSION) | ||
| -if ("${LD_VERSION}" MATCHES "GNU gold") | ||
| - string(APPEND CMAKE_EXE_LINKER_FLAGS " -fuse-ld=gold") | ||
| - string(APPEND CMAKE_SHARED_LINKER_FLAGS " -fuse-ld=gold") | ||
| - string(APPEND CMAKE_MODULE_LINKER_FLAGS " -fuse-ld=gold") | ||
| - message(STATUS "Using GNU gold linker.") | ||
| -endif () | ||
| - | ||
| #-----------------------------------------------------------------------------# | ||
| # Use interprocedural optimization if requested | ||
|
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,20 @@ | ||
| diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt | ||
| index 3ff605948..d9dd4b70d 100644 | ||
| --- a/src/parser/CMakeLists.txt | ||
| +++ b/src/parser/CMakeLists.txt | ||
| @@ -107,15 +107,6 @@ flex_target(Lexer | ||
| ${CMAKE_CURRENT_BINARY_DIR}/smt2/smt2_lexer.cpp) | ||
| set_source_files_properties(${CMAKE_CURRENT_BINARY_DIR}/smt2/smt2_lexer.cpp PROPERTIES GENERATED TRUE) | ||
|
|
||
| -# The FlexLexer.h header is installed to /usr/include/, but is not found by the | ||
| -# cross-compilation environment. As a workaround we'll copy the header to the | ||
| -# current build directory and set the FLEX_INCLUDE_DIRS variable accordingly. | ||
| -if(WIN32) | ||
| - file(MAKE_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/flex) | ||
| - file(COPY /usr/include/FlexLexer.h DESTINATION ${CMAKE_CURRENT_BINARY_DIR}/flex) | ||
| - set(FLEX_INCLUDE_DIRS ${CMAKE_CURRENT_BINARY_DIR}/flex) | ||
| -endif() | ||
| - | ||
| # We don't want to enable -Wall for code generated by Flex. | ||
| set(gen_src_files ${CMAKE_CURRENT_BINARY_DIR}/smt2/smt2_lexer.cpp) | ||
| set(GEN_SRC_FLAGS "") |
Submodule cvc5
updated
1042 files