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

refactor: put all includes in include/lean/

Browse source
This commit is contained in:
Sebastian Ullrich 2020-05-18 16:04:16 +02:00 • committed by Leonardo de Moura
parent 655a16ce56
commit 9fdcf6ea59
5 changed files with 9 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/CMakeLists.txt
View file

@ -76,7 +76,6 @@ option(RUNTIME_STATS "RUNTIME_STATS" OFF)
# development-specific options
option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" ON)
set(INCLUDE_DIR "include" CACHE STRING "include dir")
set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to lean --make")
set(MINGW_LOCAL_DIR "C:/msys64/mingw64/bin" CACHE STRING "where to find MSYS2 required DLLs and binaries")
@ -480,10 +479,10 @@ endif ()
# Version
configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/version.h")
configure_file("${LEAN_SOURCE_DIR}/config.h.in" "${LEAN_BINARY_DIR}/include/config.h")
install(FILES "${LEAN_BINARY_DIR}/include/config.h" DESTINATION "${INCLUDE_DIR}")
configure_file("${LEAN_SOURCE_DIR}/config.h.in" "${LEAN_BINARY_DIR}/include/lean/config.h")
install(DIRECTORY ${LEAN_BINARY_DIR}/include/lean DESTINATION include)
configure_file("${LEAN_SOURCE_DIR}/Makefile.in" "${LEAN_BINARY_DIR}/share/lean/Makefile")
install(FILES "${LEAN_BINARY_DIR}/share/lean/Makefile" DESTINATION "share/lean")
install(DIRECTORY ${LEAN_BINARY_DIR}/share/lean DESTINATION share)
if(EMSCRIPTEN)
set(LEAN_LIBRARY_TYPE SHARED)
@ -614,8 +613,8 @@ install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION lib/lean
PATTERN "*.lean"
PATTERN "*.md")
file(COPY ${CMAKE_SOURCE_DIR}/runtime/lean.h DESTINATION ${CMAKE_BINARY_DIR}/include/runtime)
install(FILES "${CMAKE_SOURCE_DIR}/runtime/lean.h" DESTINATION "${INCLUDE_DIR}/runtime")
file(COPY ${CMAKE_SOURCE_DIR}/runtime DESTINATION ${CMAKE_BINARY_DIR}/include/lean
FILES_MATCHING PATTERN "*.h")
if("${INCLUDE_MSYS2_DLLS}" MATCHES "ON")
# TODO(Leo): do not use hardlinks to required DLLs.

2
src/Init/Lean/Compiler/IR/EmitC.lean
View file

@ -209,7 +209,7 @@ emitLn ("// Module: " ++ toString modName);
emit "// Imports:";
env.imports.forM $ fun m => emit (" " ++ toString m);
emitLn "";
emitLn "#include \"runtime/lean.h\"";
emitLn "#include <lean/runtime/lean.h>";
emitLns [
"#if defined(__clang__)",
"#pragma clang diagnostic ignored \"-Wunused-parameter\"",

2
src/bin/leanc.in
View file

@ -27,4 +27,4 @@ done
[ -f $LEAN_CXX ] || command -v $LEAN_CXX || error "no suitable C++ compiler found!"
# Note the `-x c` for treating all input as C code
@CMAKE_CXX_COMPILER_LAUNCHER@ $LEAN_CXX -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" -x c "$@" -x none "-L$bindir/../lib/lean" $linker_flags -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
@CMAKE_CXX_COMPILER_LAUNCHER@ $LEAN_CXX -D LEAN_MULTI_THREAD "-I$bindir/../include" -x c "$@" -x none "-L$bindir/../lib/lean" $linker_flags -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument

2
src/runtime/lean.h
View file

@ -24,7 +24,7 @@ extern "C" {
#include <stdatomic.h>
#define LEAN_USING_STD
#endif
#include "config.h" // NOLINT
#include <lean/config.h>
#define LEAN_CLOSURE_MAX_ARGS 16
#define LEAN_OBJECT_SIZE_DELTA 8

2
src/runtime/thread.cpp
View file

@ -12,7 +12,7 @@ Author: Leonardo de Moura
#else
#include <pthread.h>
#endif
#include "config.h" // NOLINT
#include <lean/config.h>
#include "runtime/thread.h"
#include "runtime/interrupt.h"
#include "runtime/exception.h"