diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 6af38a7925..7c5ee3e50c 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -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.
diff --git a/src/Init/Lean/Compiler/IR/EmitC.lean b/src/Init/Lean/Compiler/IR/EmitC.lean
index b85837c669..df805a34f8 100644
--- a/src/Init/Lean/Compiler/IR/EmitC.lean
+++ b/src/Init/Lean/Compiler/IR/EmitC.lean
@@ -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\"",
diff --git a/src/bin/leanc.in b/src/bin/leanc.in
index 28323233eb..1c57d1e99e 100755
--- a/src/bin/leanc.in
+++ b/src/bin/leanc.in
@@ -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
diff --git a/src/runtime/lean.h b/src/runtime/lean.h
index f591defd97..9425f00ecb 100644
--- a/src/runtime/lean.h
+++ b/src/runtime/lean.h
@@ -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
diff --git a/src/runtime/thread.cpp b/src/runtime/thread.cpp
index 23dffb6dac..e5475b4507 100644
--- a/src/runtime/thread.cpp
+++ b/src/runtime/thread.cpp
@@ -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"