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

chore: use leanc for all C code

Browse source
This commit is contained in:
Wojciech Nawrocki 2021-06-03 15:51:45 -04:00 • committed by Sebastian Ullrich
parent 2ef11669e8
commit c772dc49ef
7 changed files with 36 additions and 31 deletions
Show stats 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_FLAGS=-fsanitize=address,undefined -DSMALL_ALLOCATOR=OFF
CMAKE_OPTIONS: -DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_C_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_FLAGS=-fsanitize=address,undefined" "-DSMALL_ALLOCATOR=OFF" ]; };
sanitized = lean-packages.override { extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined" "-DLEANC_EXTRA_C_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_FLAGS=-fsanitize=thread" "-DCOMPRESSED_OBJECT_HEADER=OFF" ];
extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=thread" "-DLEANC_EXTRA_C_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.

6
script/update-stage0
View file

@ -2,7 +2,11 @@
set -euo pipefail
rm -r stage0 || true
mkdir -p stage0/
mkdir -p stage0/stdlib/
cat <<EOF >> stage0/stdlib/CMakeLists.txt
set(CMAKE_C_COMPILER_LAUNCHER "env;LEAN_CXX=\${CMAKE_CXX_COMPILER_LAUNCHER} \${CMAKE_CXX_COMPILER}")
set(CMAKE_C_COMPILER "\${CMAKE_BINARY_DIR}/bin/leanc")
EOF
for pkg in Init Std Lean; do
# ensure deterministic ordering
c_files="$pkg.c $(cd src; find $pkg -name '*.lean' | sed s/.lean/.c/ | LC_ALL=C sort | tr '\n' ' ')"

22
src/CMakeLists.txt
View file

@ -72,6 +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")
endif()
if ("${LAZY_RC}" MATCHES "ON")
@ -112,10 +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")
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")
endif()
if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
@ -132,10 +135,8 @@ 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(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} ${EMSCRIPTEN_SETTINGS}")
set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${EMSCRIPTEN_SETTINGS}")
set(LEANC_OPTS "${LEANC_OPTS} ${EMSCRIPTEN_SETTINGS}")
set(LEANC_GMP "${GMP_INSTALL_PREFIX}/lib/libgmp.a")
endif()
if (CMAKE_CROSSCOMPILING_EMULATOR)
# emscripten likes to quote "node"
@ -157,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_FLAGS "${LEANC_EXTRA_FLAGS} -Wl,--stack,${LEAN_WIN_STACK_SIZE}")
set(LEANC_EXTRA_LINKER_FLAGS "${LEANC_EXTRA_LINKER_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}")
@ -170,14 +171,15 @@ endif ()
if(NOT MULTI_THREAD)
message(STATUS "Disabled multi-thread support, it will not be safe to run multiple threads in parallel")
set(LEANC_OPTS "${LEANC_OPTS} -U LEAN_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")
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")
endif()
if(LLVM)
@ -189,6 +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")
# Find the libraries that correspond to the LLVM components
# that we wish to use and define llvm_libs
@ -280,6 +283,7 @@ endif ()
if ("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
include_directories(${GMP_INSTALL_PREFIX}/include)
set(GMP_LIBRARIES "${GMP_INSTALL_PREFIX}/lib/libgmp.a")
else()
# GMP
find_package(GMP 5.0.5 REQUIRED)
@ -312,6 +316,8 @@ include_directories(${CMAKE_BINARY_DIR}/include)
# the linker flags necessary on other platforms.
if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
set(LEANC_STATIC_LINKER_FLAGS "-lleancpp -lInit -lStd -lLean")
elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
set(LEANC_STATIC_LINKER_FLAGS "-lleancpp -lInit -lStd -lLean -lnodefs.js")
else()
# `-pie` defaulting is not consistent on Linux distributions, so let's default to off
set(LEANC_STATIC_LINKER_FLAGS "-no-pie -Wl,--start-group -lleancpp -lInit -lStd -lLean -Wl,--end-group")
@ -333,7 +339,7 @@ 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_FLAGS "${LEANC_EXTRA_FLAGS} -ldl")
set(LEANC_EXTRA_LINKER_FLAGS "${LEANC_EXTRA_LINKER_FLAGS} -ldl")
endif()
# Allow `lean` symbols in plugins without linking directly against it. If we linked against the
@ -343,13 +349,13 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
# import library created by the `lean` target
set(LEANC_SHARED_LINKER_FLAGS "$bindir/lean.exe.a")
elseif("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")
set(LEANC_SHARED_LINKER_FLAGS "${LEANC_EXTRA_FLAGS} -Wl,-undefined,dynamic_lookup")
set(LEANC_SHARED_LINKER_FLAGS "-Wl,-undefined,dynamic_lookup")
endif()
# Linux ignores undefined symbols in shared libraries by default
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_FLAGS "${LEANC_EXTRA_FLAGS} -pthread")
set(LEANC_EXTRA_C_FLAGS "${LEANC_EXTRA_C_FLAGS} -pthread")
endif()
# Git HASH

10
src/bin/leanc.in
View file

@ -16,8 +16,8 @@
set -e
bindir=$(dirname $0)
cflags=("-I$bindir/../include")
ldflags=("-L$bindir/../lib/lean" "${LEANC_GMP:--lgmp}" @LEANC_EXTRA_FLAGS@)
cflags=("-I$bindir/../include" @LEANC_EXTRA_C_FLAGS@)
ldflags=("-L$bindir/../lib/lean" "${LEANC_GMP:--lgmp}" @LEANC_EXTRA_LINKER_FLAGS@)
ldflags_ext=(@LEANC_STATIC_LINKER_FLAGS@)
args=("$@")
for arg in "$@"; do
@ -25,10 +25,10 @@ for arg in "$@"; do
[[ $arg == "-shared" ]] && ldflags_ext=(@LEANC_SHARED_LINKER_FLAGS@) && args=("-x" "c" "$@" "-x" "none")
# Note the `-x c` for treating all input as C code
[[ $arg == "-c" ]] && ldflags=() && ldflags_ext=() && args=("-x" "c" "$@" "-x" "none")
[[ $arg == "-print-cflags" ]] && echo "${cflags[@]} ${cflags_ext[@]}" && exit
[[ $arg == "-print-ldflags" ]] && echo "${ldflags_ext[@]} ${ldflags[@]}" && exit
[[ $arg == "-print-cflags" ]] && echo "${cflags[@]}" && exit
[[ $arg == "-print-ldflags" ]] && echo "${cflags[@]} ${ldflags_ext[@]} ${ldflags[@]}" && exit
done
[ -n "$LEAN_CXX" ] || LEAN_CXX=c++
$LEAN_CXX -D LEAN_MULTI_THREAD "${cflags[@]}" "${args[@]}" "${ldflags_ext[@]}" "${ldflags[@]}" -Wno-unused-command-line-argument
$LEAN_CXX "${cflags[@]}" "${args[@]}" "${ldflags_ext[@]}" "${ldflags[@]}" -Wno-unused-command-line-argument

22
src/shell/CMakeLists.txt
View file

@ -1,16 +1,12 @@
if (${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
add_executable(lean lean.cpp)
set_target_properties(lean PROPERTIES
RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/bin/")
target_link_libraries(lean Init Std Lean leancpp "${GMP_INSTALL_PREFIX}/lib/libgmp.a" "-lnodefs.js")
else ()
add_library(shell OBJECT lean.cpp)
add_custom_command(OUTPUT ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}
COMMAND sh -c "LEANC_GMP=${GMP_LIBRARIES} ${CMAKE_BINARY_DIR}/bin/leanc -x none ${CMAKE_EXE_LINKER_FLAGS} $<TARGET_OBJECTS:shell> -o ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"
DEPENDS Init Std Lean leancpp shell)
add_custom_target(lean ALL
DEPENDS ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX})
endif ()
add_library(shell OBJECT lean.cpp)
string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
add_custom_command(OUTPUT ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}
COMMAND sh -c "LEANC_GMP=${GMP_LIBRARIES} LEAN_CXX='${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}' ${CMAKE_BINARY_DIR}/bin/leanc ${CMAKE_EXE_LINKER_FLAGS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} $<TARGET_OBJECTS:shell> -o ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"
DEPENDS Init Std Lean leancpp shell)
add_custom_target(lean ALL
DEPENDS ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX})
install(FILES ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}
DESTINATION bin

1
src/stdlib.make.in
View file

@ -16,7 +16,6 @@ LEANMAKE_OPTS=\
BIN_OUT="${CMAKE_BINARY_DIR}/bin"\
LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -Dinterpreter.prefer_native=false"\
LEANC_OPTS+="${LEANC_OPTS}"\
LEANC_GMP="${LEANC_GMP}"\
LEAN_CXX="${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}"\
LEAN_AR="${CMAKE_AR}"\
MORE_DEPS+="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\