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

chore: restore LEANC_EXTRA_FLAGS

Browse Source 
We now pass them to both compilers and linkers. For example, -pthread should be given to both: https://stackoverflow.com/questions/2127797/significance-of-pthread-flag-when-compiling
This commit is contained in:
Wojciech Nawrocki
2021-06-04 18:47:08 -04:00
committed by Sebastian Ullrich
parent c772dc49ef
commit d92e4a7cf1
4 changed files with 17 additions and 15 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
.github/workflows/ci.yml vendored
View File

@@ -38,7 +38,7 @@ jobs:
- name: Linux fsanitize
os: ubuntu-latest
# turn off custom allocator to make LSAN do its magic
CMAKE_OPTIONS: -DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_C_FLAGS=-fsanitize=address,undefined -DSMALL_ALLOCATOR=OFF
CMAKE_OPTIONS: -DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS=-fsanitize=address,undefined -DSMALL_ALLOCATOR=OFF
- name: macOS
os: macos-latest
release: true

4
flake.nix
View File

@@ -34,10 +34,10 @@
packages = lean-packages // rec {
debug = lean-packages.override { debug = true; };
stage0debug = lean-packages.override { stage0debug = true; };
sanitized = lean-packages.override { extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined" "-DLEANC_EXTRA_C_FLAGS=-fsanitize=address,undefined" "-DSMALL_ALLOCATOR=OFF" ]; };
sanitized = lean-packages.override { extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined" "-DLEANC_EXTRA_FLAGS=-fsanitize=address,undefined" "-DSMALL_ALLOCATOR=OFF" ]; };
sandebug = sanitized.override { debug = true; };
tsan = lean-packages.override {
extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=thread" "-DLEANC_EXTRA_C_FLAGS=-fsanitize=thread" "-DCOMPRESSED_OBJECT_HEADER=OFF" ];
extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=thread" "-DLEANC_EXTRA_FLAGS=-fsanitize=thread" "-DCOMPRESSED_OBJECT_HEADER=OFF" ];
stage0 = (lean-packages.override {
# Compressed headers currently trigger data race reports in tsan.
# Turn them off for stage 0 as well so stage 1 can read its own stdlib.

22
src/CMakeLists.txt
View File

@@ -72,7 +72,7 @@ set(MINGW_LOCAL_DIR "C:/msys64/mingw64/bin" CACHE STRING "where to fi
if ("${FAKE_FREE}" MATCHES "ON")
set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_FAKE_FREE")
set(LEANC_EXTRA_C_FLAGS "${LEANC_EXTRA_C_FLAGS} -D LEAN_FAKE_FREE")
set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -D LEAN_FAKE_FREE")
endif()
if ("${LAZY_RC}" MATCHES "ON")
@@ -113,12 +113,12 @@ endif()
if ("${RUNTIME_STATS}" MATCHES "ON")
set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_RUNTIME_STATS")
set(LEANC_EXTRA_C_FLAGS "${LEANC_EXTRA_C_FLAGS} -D LEAN_RUNTIME_STATS")
set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -D LEAN_RUNTIME_STATS")
endif()
if (NOT("${CHECK_OLEAN_VERSION}" MATCHES "ON"))
set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_IGNORE_OLEAN_VERSION")
set(LEANC_EXTRA_C_FLAGS "${LEANC_EXTRA_C_FLAGS} -D LEAN_IGNORE_OLEAN_VERSION")
set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -D LEAN_IGNORE_OLEAN_VERSION")
endif()
if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
@@ -135,7 +135,7 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
# > The simple and safe thing is to pass all -s flags at both compile and link time.
set(EMSCRIPTEN_SETTINGS "-s ALLOW_MEMORY_GROWTH=1 -s DISABLE_EXCEPTION_CATCHING=0 -s MAIN_MODULE=1 -fexceptions")
set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_EMSCRIPTEN ${EMSCRIPTEN_SETTINGS}")
set(LEANC_EXTRA_C_FLAGS "${LEANC_EXTRA_C_FLAGS} -D LEAN_EMSCRIPTEN ${EMSCRIPTEN_SETTINGS}")
set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -D LEAN_EMSCRIPTEN ${EMSCRIPTEN_SETTINGS}")
set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} ${EMSCRIPTEN_SETTINGS}")
endif()
if (CMAKE_CROSSCOMPILING_EMULATOR)
@@ -158,7 +158,7 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} /STACK:${LEAN_WIN_STACK_SIZE}")
else()
set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -Wl,--stack,${LEAN_WIN_STACK_SIZE}")
set(LEANC_EXTRA_LINKER_FLAGS "${LEANC_EXTRA_LINKER_FLAGS} -Wl,--stack,${LEAN_WIN_STACK_SIZE}")
set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -Wl,--stack,${LEAN_WIN_STACK_SIZE}")
set(EXTRA_UTIL_LIBS ${EXTRA_UTIL_LIBS} -lpsapi)
endif()
set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_WINDOWS -D LEAN_WIN_STACK_SIZE=${LEAN_WIN_STACK_SIZE}")
@@ -174,12 +174,12 @@ if(NOT MULTI_THREAD)
set(AUTO_THREAD_FINALIZATION OFF)
else()
set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_MULTI_THREAD")
set(LEANC_EXTRA_C_FLAGS "${LEANC_EXTRA_C_FLAGS} -D LEAN_MULTI_THREAD")
set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -D LEAN_MULTI_THREAD")
endif()
if(AUTO_THREAD_FINALIZATION AND NOT MSVC)
set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_AUTO_THREAD_FINALIZATION")
set(LEANC_EXTRA_C_FLAGS "${LEANC_EXTRA_C_FLAGS} -D LEAN_AUTO_THREAD_FINALIZATION")
set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -D LEAN_AUTO_THREAD_FINALIZATION")
endif()
if(LLVM)
@@ -191,7 +191,7 @@ if(LLVM)
include_directories(${LLVM_INCLUDE_DIRS})
set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_LLVM")
set(LEANC_EXTRA_C_FLAGS "${LEANC_EXTRA_C_FLAGS} -D LEAN_LLVM")
set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -D LEAN_LLVM")
# Find the libraries that correspond to the LLVM components
# that we wish to use and define llvm_libs
@@ -339,7 +339,8 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
set(LEAN_EXTRA_MAKE_OPTS "-Dcompiler.extract_closed=false")
else()
set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS} -rdynamic")
set(LEANC_EXTRA_LINKER_FLAGS "${LEANC_EXTRA_LINKER_FLAGS} -ldl")
set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -ldl")
set(LEANC_SHARED_LINKER_FLAGS "${LEANC_SHARED_LINKER_FLAGS} -ldl")
endif()
# Allow `lean` symbols in plugins without linking directly against it. If we linked against the
@@ -355,7 +356,7 @@ endif()
if(MULTI_THREAD AND NOT MSVC AND (NOT ("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")))
set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread")
set(LEANC_EXTRA_C_FLAGS "${LEANC_EXTRA_C_FLAGS} -pthread")
set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -pthread")
endif()
# Git HASH
@@ -440,6 +441,7 @@ if(PREV_STAGE)
file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
# These are used in lean.mk and passed through by stdlib.make
set(LEANC_OPTS "${LEANC_OPTS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}")
configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make)

4
src/bin/leanc.in
View File

@@ -16,8 +16,8 @@
set -e
bindir=$(dirname $0)
cflags=("-I$bindir/../include" @LEANC_EXTRA_C_FLAGS@)
ldflags=("-L$bindir/../lib/lean" "${LEANC_GMP:--lgmp}" @LEANC_EXTRA_LINKER_FLAGS@)
cflags=("-I$bindir/../include" @LEANC_EXTRA_FLAGS@)
ldflags=("-L$bindir/../lib/lean" "${LEANC_GMP:--lgmp}")
ldflags_ext=(@LEANC_STATIC_LINKER_FLAGS@)
args=("$@")
for arg in "$@"; do