diff --git a/.gitignore b/.gitignore
index 57b6aec8da..9d1bd30aa9 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,8 +1,6 @@
 *~
 \#*
 .#*
-*.olean
-*.depend
 *.lock
 build
 GPATH
@@ -12,9 +10,6 @@ GTAGS
 .projectile
 .lean_options
 .vs
-/src/stage1
-/src/config.h
-/stage0/src/config.h
 compile_commands.json
 *.idea
 tasks.json
@@ -24,4 +19,3 @@ settings.json
 *.produced.out
 CMakeSettings.json
 CppProperties.json
-/src/Makefile
diff --git a/bin/.gitignore b/bin/.gitignore
deleted file mode 100644
index 0325f4c3b9..0000000000
--- a/bin/.gitignore
+++ /dev/null
@@ -1,9 +0,0 @@
-lean
-lean.exe
-leanc
-lean_stage0
-lean_stage0.exe
-lean_stage2
-lean_stage2.exe
-*.a
-*.so
diff --git a/bin/lean_wrapped b/bin/lean_wrapped
deleted file mode 100755
index 98a9452aac..0000000000
--- a/bin/lean_wrapped
+++ /dev/null
@@ -1,17 +0,0 @@
-#!/usr/bin/env bash
-# Call `lean_stage0` when in src/Init; otherwise call `lean`.
-
-bin=$(dirname $(realpath $0))
-lib=$(dirname $bin)/src/Init
-# use dir of input file, or pwd if stdin
-if [[ "$*" == *--stdin* ]]; then
-    dir=$(pwd)
-else
-    dir=$(dirname $(realpath ${@:$#}))
-fi
-# check if `dir` starts with `$lib`
-if [[ ${dir##$lib} != $dir ]]; then
-    $bin/lean_stage0 $*
-else
-    $bin/lean $*
-fi
diff --git a/lean4-mode/lean4-settings.el b/lean4-mode/lean4-settings.el
index ce520a2195..34b9417554 100644
--- a/lean4-mode/lean4-settings.el
+++ b/lean4-mode/lean4-settings.el
@@ -21,7 +21,7 @@
 (defvar-local lean4-default-executable-name
   (cl-case system-type
     ('windows-nt   "lean.exe")
-    (t             "lean_wrapped"))
+    (t             "lean"))
   "Default executable name of Lean")
 
 (defcustom lean4-rootdir nil
diff --git a/shell.nix b/shell.nix
index 8445c2473b..b2d94253b3 100644
--- a/shell.nix
+++ b/shell.nix
@@ -14,9 +14,6 @@ let attribs = rec {
     recipe = pkgs.writeText "recipe" ''
       (lean4-mode :repo "leanprover/lean4" :fetcher github :files ("*.el"))
     '';
-    patchPhase = ''
-      sed -i 's/lean_wrapped/lean/' *.el
-    '';
     fileSpecs = [ "*.el" ];
   };
   emacs = pkgs.emacsWithPackages (epkgs:
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 560245e850..f885506665 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -459,8 +459,8 @@ if(USE_GITHASH)
   get_git_head_revision(GIT_REFSPEC GIT_SHA1)
   if(${GIT_SHA1} MATCHES "GITDIR-NOTFOUND")
     message(STATUS "Failed to read git_sha1")
-    if(EXISTS "${LEAN_SOURCE_DIR}/../bin/package_version")
-      file(STRINGS "${LEAN_SOURCE_DIR}/../bin/package_version" LEAN_PACKAGE_VERSION)
+    if(EXISTS "${LEAN_SOURCE_DIR}/bin/package_version")
+      file(STRINGS "${LEAN_SOURCE_DIR}/bin/package_version" LEAN_PACKAGE_VERSION)
       message(STATUS "Package version detected: ${LEAN_PACKAGE_VERSION}")
     endif()
   else()
@@ -468,8 +468,8 @@ if(USE_GITHASH)
   endif()
 else()
   set(GIT_SHA1 "GITDIR-NOTFOUND")
-  if(EXISTS "${LEAN_SOURCE_DIR}/../bin/package_version")
-    file(STRINGS "${LEAN_SOURCE_DIR}/../bin/package_version" LEAN_PACKAGE_VERSION)
+  if(EXISTS "${LEAN_SOURCE_DIR}/bin/package_version")
+    file(STRINGS "${LEAN_SOURCE_DIR}/bin/package_version" LEAN_PACKAGE_VERSION)
     message(STATUS "Package version detected: ${LEAN_PACKAGE_VERSION}")
   endif()
 endif()
@@ -483,14 +483,9 @@ endif ()
 
 # Version
 configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/version.h")
-# Remark: we did not put `config.h` in `${LEAN_BINARY_DIR}` because `leanc` depends on this file.
-# Note that, `leanc` already had problems with multiple configurations before we added `config.h`.
-# For example, it uses binary files located in the `bin` directory.
-configure_file("${LEAN_SOURCE_DIR}/config.h.in" "${LEAN_SOURCE_DIR}/config.h")
-install(FILES "${LEAN_SOURCE_DIR}/config.h" DESTINATION "${INCLUDE_DIR}")
-if(NOT STAGE0)
-  configure_file("${LEAN_SOURCE_DIR}/Makefile.in" "${LEAN_SOURCE_DIR}/Makefile")
-endif()
+configure_file("${LEAN_SOURCE_DIR}/config.h.in" "${LEAN_BINARY_DIR}/include/config.h")
+install(FILES "${LEAN_SOURCE_DIR}/include/config.h" DESTINATION "${INCLUDE_DIR}")
+configure_file("${LEAN_SOURCE_DIR}/Makefile.in" "${LEAN_BINARY_DIR}/share/lean/Makefile")
 
 include_directories("${LEAN_BINARY_DIR}")
 add_subdirectory(runtime)
@@ -515,7 +510,6 @@ add_subdirectory(initialize)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:initialize>)
 if(STAGE0)
   add_subdirectory(../stdlib stdlib)
-  set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:stage0>)
 endif()
 if(EMSCRIPTEN)
     set(LEAN_LIBRARY_TYPE SHARED)
@@ -534,7 +528,7 @@ if(NOT STAGE0)
       -DCHECK_OLEAN_VERSION=${CHECK_OLEAN_VERSION}
       "-DCMAKE_C_COMPILER=${CMAKE_C_COMPILER}"
       "-DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER}"
-    BUILD_COMMAND $(MAKE) lean  # build executable only
+    BUILD_COMMAND $(MAKE)  # build executable only
     BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
     INSTALL_COMMAND ""  # skip install
   )
@@ -542,42 +536,36 @@ endif()
 
 add_library(leanstatic ${LEAN_LIBRARY_TYPE} ${LEAN_OBJS})
 target_link_libraries(leanstatic ${EXTRA_LIBS})
+set_target_properties(leanstatic PROPERTIES ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib")
 
 if(LLVM)
   target_link_libraries(leanstatic ${llvm_libs})
 endif()
 
-if(NOT STAGE0)
+if(STAGE0)
+  add_library(leanstdlib STATIC $<TARGET_OBJECTS:stage0>)
+else()
   add_library(leanstdlib STATIC IMPORTED)
-  ADD_CUSTOM_TARGET(bin_lib ALL
-     COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin"
-     COMMAND "${CMAKE_COMMAND}" -E copy ${COPY_LIBS} "$<TARGET_FILE:leanstdlib>" "$<TARGET_FILE:leanstatic>" "${LEAN_SOURCE_DIR}/../bin"
-  )
-  # Configure leanc
-  configure_file("${LEAN_SOURCE_DIR}/../bin/leanc.in" "${CMAKE_CURRENT_BINARY_DIR}/tmp/leanc")
-  file(COPY "${CMAKE_CURRENT_BINARY_DIR}/tmp/leanc"
-    DESTINATION "${LEAN_SOURCE_DIR}/../bin"
-    FILE_PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
-  install(FILES "${LEAN_SOURCE_DIR}/../bin/leanc"
-    DESTINATION bin
-    PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
-
-  add_custom_target(bin ALL)
-  add_dependencies(bin bin_lib bin_lean)
 endif()
 
-# The DLL (shared library) is not being generated correctly when we use cross-compilation (i.e., generate the Windows DLL using Linux).
-# For some strange reason, it contains a copy of pthread_equal.
-# Remark: this problem does not happen when we generate the DLL using msys2 on Windows.
-if (NOT("${CROSS_COMPILE}" MATCHES "ON"))
-  if ("${STATIC}" MATCHES "OFF")
-    add_library(leanshared SHARED shared/init.cpp)
-    # see `target_link_libraries(lean ...)`
-    target_link_libraries(leanshared leanstatic leanstdlib leanstatic leanstdlib)
-    install(TARGETS leanshared DESTINATION lib)
-  endif()
-  install(TARGETS leanstatic DESTINATION lib)
-endif()
+configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/bin/leanc")
+install(FILES "${CMAKE_BINARY_DIR}/bin/leanc"
+  DESTINATION bin
+  PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
+
+# shared library deactivated until we figure out the leanstatic/leanstdlib story
+# # The DLL (shared library) is not being generated correctly when we use cross-compilation (i.e., generate the Windows DLL using Linux).
+# # For some strange reason, it contains a copy of pthread_equal.
+# # Remark: this problem does not happen when we generate the DLL using msys2 on Windows.
+# if (NOT("${CROSS_COMPILE}" MATCHES "ON"))
+#   if ("${STATIC}" MATCHES "OFF")
+#     add_library(leanshared SHARED shared/init.cpp)
+#     # see `target_link_libraries(lean ...)`
+#     target_link_libraries(leanshared leanstatic leanstdlib leanstatic leanstdlib)
+#     install(TARGETS leanshared DESTINATION lib)
+#   endif()
+#   install(TARGETS leanstatic DESTINATION lib)
+# endif()
 
 add_subdirectory(shell)
 
@@ -618,24 +606,23 @@ add_test(NAME style_check COMMAND "${PYTHON_EXECUTABLE}" "${LEAN_SOURCE_DIR}/cma
 endif()
 
 add_custom_target(clean-stdlib
-  WORKING_DIRECTORY "${LEAN_SOURCE_DIR}"
-  COMMAND find . -name '*.olean' -delete
-  COMMAND find . -name '*.depend' -delete
-  COMMAND rm -rf ../stage1 "${CMAKE_BINARY_DIR}/stage2" "${CMAKE_BINARY_DIR}/stage3" || true
-  )
+  COMMAND rm -rf "${CMAKE_BINARY_DIR}/lib" "${CMAKE_BINARY_DIR}/stage2" "${CMAKE_BINARY_DIR}/stage3" || true)
 
 add_custom_target(clean-olean
   DEPENDS clean-stdlib)
 
-install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION "${LIBRARY_DIR}"
+install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION "${LIBRARY_DIR}/lean"
+        FILES_MATCHING
+        PATTERN "*.olean")
+
+install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION "${LIBRARY_DIR}/lean/src"
         FILES_MATCHING
         PATTERN "*.lean"
-        PATTERN "*.olean"
         PATTERN "*.md")
 
-install(DIRECTORY "${CMAKE_SOURCE_DIR}/runtime" DESTINATION "${INCLUDE_DIR}"
-        FILES_MATCHING
-        PATTERN "*.h")
+add_custom_target(include_runtime ALL
+  COMMAND cmake -E copy_directory "${CMAKE_SOURCE_DIR}/runtime" "${CMAKE_BINARY_DIR}/include/runtime")
+install(FILES "${CMAKE_SOURCE_DIR}/runtime/lean.h" DESTINATION "${INCLUDE_DIR}/runtime")
 
 if("${INCLUDE_MSYS2_DLLS}" MATCHES "ON")
   # TODO(Leo): do not use hardlinks to required DLLs.
diff --git a/src/Makefile.in b/src/Makefile.in
index 4bbeb4ab04..06597b4ba8 100644
--- a/src/Makefile.in
+++ b/src/Makefile.in
@@ -1,21 +1,15 @@
 # Copyright (c) 2018 Simon Hudon. All rights reserved.
 # Released under Apache 2.0 license as described in the file LICENSE.
 # Authors: Simon Hudon, Sebastian Ullrich, Leonardo de Moura
-LEAN ?= ../bin/lean
-LEANC ?= ../bin/leanc
-LEAN_ROOT ?= .
-# Even though we copy the sources into a new directory for stage2/3, we
-# read the list of files to compile from the original directory to avoid
-# issues with stale copied files
-SRCS = $(shell cd $(LEAN_ROOT); find . -name '*.lean')
-DEPS = $(addprefix $(LEAN_ROOT)/,$(SRCS:.lean=.depend))
+SRCS = $(shell find Init -name '*.lean')
+DEPS = $(addprefix $(OUT)/temp/,$(SRCS:.lean=.depend))
 OPTS = @LEAN_EXTRA_MAKE_OPTS@
 STAGE0_DIR = ../stage0
-C_OUT ?= .
 ifndef OUT
 $(error "`OUT` must be set (use cmake)")
 endif
-OBJS = $(SRCS:.lean=.olean)
+export LEAN_PATH=Init=$(OUT)/lean/Init
+OBJS = $(addprefix $(OUT)/lean/, $(SRCS:.lean=.olean))
 # ensure deterministic ordering
 CS_CORE=$(sort $(SRCS:.lean=.c))
 
@@ -23,44 +17,49 @@ SHELL = /usr/bin/env bash -eo pipefail
 
 .PHONY: all clean
 
-all: $(OBJS)
+all: $(OBJS) $(OUT)/libleanstdlib.a
 
 depends: $(DEPS)
 
-%.depend: %.lean
-# use separate assignment to ensure failure propagation
-	@deps=`$(LEAN) --deps $< | python relative.py`; echo $(<:.lean=.olean): $$deps > $@
+$(OUT)/lean/Init:
+	@mkdir -p "$@"
 
-%.olean: %.lean %.depend $(MORE_DEPS)
+$(OUT)/temp/%.depend: %.lean | $(OUT)/lean/Init
+	@mkdir -p "$(OUT)/temp/$(*D)"
+# use separate assignment to ensure failure propagation
+# convert file separators and newlines on Windows
+	@deps=`lean --deps $< | sed 's!\\\\!/!g;s/\\r//'`; echo $(OUT)/lean/$(<:.lean=.olean): $$deps > $@
+
+$(OUT)/lean/%.olean: %.lean $(OUT)/temp/%.depend $(MORE_DEPS)
 	@echo "[    ] Building $<"
-	@mkdir -p $(C_OUT)/$(*D)
-	$(LEAN) $(OPTS) -o "$@" --c="$(C_OUT)/$*.c.tmp" $<
+	@mkdir -p $(OUT)/lean/$(*D)
+	lean $(OPTS) -o "$@" --c="$(OUT)/temp/$*.c.tmp" $<
 # create the .c file atomically
-	mv "$(C_OUT)/$*.c.tmp" "$(C_OUT)/$*.c"
+	mv "$(OUT)/temp/$*.c.tmp" "$(OUT)/temp/$*.c"
 # make sure the .olean file is newer than the .depend file to prevent infinite make cycles
 	@touch $@
 
-$(C_OUT)/%.c: %.olean
+$(OUT)/temp/%.c: $(OUT)/lean/%.olean
 	@
 
-$(OUT)/%.o: $(C_OUT)/%.c
+$(OUT)/temp/%.o: $(OUT)/temp/%.c
 	@echo "[    ] Building $<"
 	@mkdir -p "$(@D)"
-	$(LEANC) -c -o $@ $< $(LEANC_OPTS)
+	leanc -c -o $@ $< $(LEANC_OPTS)
 
-$(OUT)/libleanstdlib.a: $(addprefix $(OUT)/,$(SRCS:.lean=.o))
+$(OUT)/libleanstdlib.a: $(addprefix $(OUT)/temp/,$(SRCS:.lean=.o))
 	@rm -f $@
 	@ar rcs $@ $^
 
 update-stage0:
 	-rm -r $(STAGE0_DIR)
 	-mkdir -p $(STAGE0_DIR)/stdlib
-	for f in $(SRCS:.lean=.c); do mkdir -p `dirname $(STAGE0_DIR)/stdlib/$$f`; cp $(C_OUT)/$$f $(STAGE0_DIR)/stdlib/$$f; done
+	for f in $(SRCS:.lean=.c); do mkdir -p `dirname $(STAGE0_DIR)/stdlib/$$f`; cp $(OUT)/$$f $(STAGE0_DIR)/stdlib/$$f; done
 	echo "add_library (stage0 OBJECT $(CS_CORE))" > $(STAGE0_DIR)/stdlib/CMakeLists.txt
 # don't copy untracked crap
 	git ls-files -z . | xargs -0 -I '{}' bash -c 'mkdir -p `dirname ../stage0/src/{}` && cp {} ../stage0/src/{}'
 	-git add $(STAGE0_DIR)
 
-.PRECIOUS: %.depend $(C_OUT)/%.c
+.PRECIOUS: %.depend $(OUT)/temp/%.c
 
 include $(DEPS)
diff --git a/bin/lean-gdb.py b/src/bin/lean-gdb.py
similarity index 100%
rename from bin/lean-gdb.py
rename to src/bin/lean-gdb.py
diff --git a/bin/leanc.in b/src/bin/leanc.in
old mode 100644
new mode 100755
similarity index 100%
rename from bin/leanc.in
rename to src/bin/leanc.in
diff --git a/src/relative.py b/src/relative.py
deleted file mode 100644
index c4f8b4b615..0000000000
--- a/src/relative.py
+++ /dev/null
@@ -1,14 +0,0 @@
-# Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-# Released under Apache 2.0 license as described in the file LICENSE.
-# Authors: Simon Hudon, Sebastian Ullrich
-
-import sys
-import os
-import re
-
-for x in sys.stdin:
-  # HACK: rewrite Windows path to mingw path
-  x = re.sub(r"^(\w):", lambda m: "/" + m[1].lower(), x).replace('\\', '/').strip()
-  curr = os.path.realpath(os.curdir)
-  curr = os.path.normpath(curr)
-  print(os.path.relpath(x, curr))
diff --git a/src/runtime/CMakeLists.txt b/src/runtime/CMakeLists.txt
index d07219307e..51228101bd 100644
--- a/src/runtime/CMakeLists.txt
+++ b/src/runtime/CMakeLists.txt
@@ -4,9 +4,3 @@ serializer.cpp stackinfo.cpp compact.cpp init_module.cpp io.cpp hash.cpp
 platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp)
 add_library(runtime OBJECT ${RUNTIME_OBJS})
 add_library(leanruntime ${RUNTIME_OBJS})
-
-ADD_CUSTOM_TARGET(bin_runtime ALL
-  COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin"
-  COMMAND "${CMAKE_COMMAND}" -E copy "${CMAKE_CURRENT_BINARY_DIR}/libleanruntime.a" "${LEAN_SOURCE_DIR}/../bin"
-  DEPENDS leanruntime
-)
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index ce06a9a8d9..b0988cab65 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -1,75 +1,56 @@
 if(NOT STAGE0)
-  add_executable(lean_stage0 IMPORTED)
-  set_target_properties(lean_stage0 PROPERTIES IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage0/shell/lean${CMAKE_EXECUTABLE_SUFFIX}")
-
-  ADD_CUSTOM_TARGET(bin_lean_stage0
-    COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean_stage0>" "${LEAN_SOURCE_DIR}/../bin/lean_stage0${CMAKE_EXECUTABLE_SUFFIX}"
-    DEPENDS stage0
-  )
-
   string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
   set(LEANC_OPTS "${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}")
 
   add_custom_target(make_stdlib
     WORKING_DIRECTORY "${LEAN_SOURCE_DIR}"
-    COMMAND ${CMAKE_COMMAND} -E env "LEAN_PATH=Init=Init" $(MAKE) "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a"
-      "LEAN=$<TARGET_FILE:lean_stage0>"
-      "LEANC_OPTS=${LEANC_OPTS}"
-      "OUT=${CMAKE_BINARY_DIR}/stage1"
-      # share .c files between different build configurations
-      "C_OUT=${LEAN_SOURCE_DIR}/stage1"
+    COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/stage0/bin:$$PATH $(MAKE) -f ${CMAKE_BINARY_DIR}/share/lean/Makefile OUT=${CMAKE_BINARY_DIR}/lib"
     DEPENDS stage0)
   set_target_properties(leanstdlib PROPERTIES
-    IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a"
+    IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/libleanstdlib.a"
     IMPORTED_LINK_INTERFACE_LIBRARIES leanstatic)
   add_dependencies(leanstdlib make_stdlib)
   install(FILES "$<TARGET_FILE:leanstdlib>" DESTINATION lib)
 
-  set(PREV_LEAN "$<TARGET_FILE:lean>")
+  set(PREV_STAGE_DIR "${CMAKE_BINARY_DIR}")
+  set(PREV_STAGE_TARGET lean)
   foreach(STAGE RANGE 2 3)
     add_custom_target(make_stdlib_stage${STAGE}
-      COMMAND cd "${LEAN_SOURCE_DIR}" && find . '\(' -name Makefile -o -name relative.py -o -name '*.lean' '\)' -exec "${CMAKE_COMMAND}" -E copy_if_different '{}' ${CMAKE_BINARY_DIR}/stage${STAGE}/'{}' '\;'
-      COMMAND cd "${CMAKE_BINARY_DIR}/stage${STAGE}" && LEAN_PATH=Init=Init $(MAKE) ./libleanstdlib.a
-        "LEAN=${PREV_LEAN}"
-        "LEANC=${LEAN_SOURCE_DIR}/../bin/leanc"
-        "LEAN_ROOT=${LEAN_SOURCE_DIR}"
-        "LEANC_OPTS=${LEANC_OPTS}"
-        "OUT=."
-        # recreate everything if the previous compiler has changed
-        "MORE_DEPS=${PREV_LEAN}"
-    )
+      WORKING_DIRECTORY "${LEAN_SOURCE_DIR}"
+      # recreate everything if the previous compiler has changed
+      COMMAND bash -c "PATH=${PREV_STAGE_DIR}/bin:$$PATH $(MAKE) -f ${CMAKE_BINARY_DIR}/share/lean/Makefile OUT=${CMAKE_BINARY_DIR}/stage${STAGE}/lib MORE_DEPS=${PREV_STAGE_DIR}/bin/lean"
+      DEPENDS ${PREV_STAGE_TARGET})
     add_library(leanstdlib_stage${STAGE} STATIC IMPORTED)
     set_target_properties(leanstdlib_stage${STAGE} PROPERTIES
-      IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage${STAGE}/libleanstdlib.a"
+      IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage${STAGE}/lib/libleanstdlib.a"
       IMPORTED_LINK_INTERFACE_LIBRARIES leanstatic)
     add_dependencies(leanstdlib_stage${STAGE} make_stdlib_stage${STAGE})
     add_executable(lean_stage${STAGE} EXCLUDE_FROM_ALL lean.cpp)
     # see `target_link_libraries(lean ...)` below
     target_link_libraries(lean_stage${STAGE} leanstatic leanstdlib_stage${STAGE} leanstatic leanstdlib_stage${STAGE})
-    set(PREV_LEAN "$<TARGET_FILE:lean_stage${STAGE}>")
+    set(PREV_STAGE_DIR "${CMAKE_BINARY_DIR}/stage${STAGE}")
+    set(PREV_STAGE_TARGET lean_stage${STAGE})
   endforeach()
 
   add_custom_target(check-stage3
     COMMAND diff "$<TARGET_FILE:lean_stage2>" "$<TARGET_FILE:lean_stage3>")
 
   add_custom_target(update-stage0
-    COMMAND make update-stage0
-      "OUT=${CMAKE_BINARY_DIR}/stage1"
-      "C_OUT=${LEAN_SOURCE_DIR}/stage1"
+    COMMAND make update-stage0 -f ${CMAKE_BINARY_DIR}/share/lean/Makefile
+      "OUT=${CMAKE_BINARY_DIR}/lib"
     DEPENDS leanstdlib
     WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}")
 endif()
 
 add_executable(lean lean.cpp)
-if(STAGE0)
-  target_link_libraries(lean leanstatic)
-else()
-  # `leanstatic` and `leanstdlib` are cyclically dependent static libraries.
-  # We use the approach described at
-  # https://cmake.org/cmake/help/v3.3/command/target_link_libraries.html#cyclic-dependencies-of-static-libraries
-  # We don't want to add leanstdlib as a direct dependency of leanstatic since this is only true for stage 1.
-  target_link_libraries(lean leanstatic leanstdlib leanstatic leanstdlib)
-endif()
+set_target_properties(lean PROPERTIES RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/bin")
+
+# `leanstatic` and `leanstdlib` are cyclically dependent static libraries.
+# We use the approach described at
+# https://cmake.org/cmake/help/v3.3/command/target_link_libraries.html#cyclic-dependencies-of-static-libraries
+# We don't want to add leanstdlib as a direct dependency of leanstatic since this is only true for stage 1.
+target_link_libraries(lean leanstatic leanstdlib leanstatic leanstdlib)
+
 # create import library on Windows to link plugins against
 set_target_properties(lean PROPERTIES ENABLE_EXPORTS ON)
 if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
@@ -78,23 +59,22 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
 endif()
 install(TARGETS lean DESTINATION bin)
 
-if(NOT STAGE0)
-  if(${EMSCRIPTEN})
+if(NOT STAGE0 AND EMSCRIPTEN)
       set(NODE_JS "node --stack_size=8192")
 
-      file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/lean_with_path
-              "#!/bin/sh\nLEAN_PATH=Init=${CMAKE_CURRENT_SOURCE_DIR}/.. ${NODE_JS} ${CMAKE_CURRENT_BINARY_DIR}/lean.js \"$@\"\n")
-      execute_process(COMMAND chmod +x ${CMAKE_CURRENT_BINARY_DIR}/lean_with_path)
+      file(WRITE $<TARGET_FILE:lean>_with_path
+              "#!/bin/sh\nLEAN_PATH=Init=${CMAKE_CURRENT_SOURCE_DIR}/.. ${NODE_JS} $<TARGET_FILE:lean>.js \"$@\"\n")
+      execute_process(COMMAND chmod +x $<TARGET_FILE:lean>_with_path)
 
       ADD_CUSTOM_TARGET(bin_lean ALL
-          COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin"
-          COMMAND "${CMAKE_COMMAND}" -E copy "${CMAKE_CURRENT_BINARY_DIR}/lean_with_path" "${LEAN_SOURCE_DIR}/../bin/lean"
+          COMMAND "${CMAKE_COMMAND}" -E make_directory "${CMAKE_BINARY_DIR}/bin"
+          COMMAND "${CMAKE_COMMAND}" -E copy "$<TARGET_FILE:lean>_with_path" "${CMAKE_BINARY_DIR}/bin/lean"
           DEPENDS lean
           )
 
-      file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/lean
-              "#!/bin/sh\n${NODE_JS} ${CMAKE_CURRENT_BINARY_DIR}/lean.js \"$@\"\n")
-      execute_process(COMMAND chmod +x ${CMAKE_CURRENT_BINARY_DIR}/lean)
+      file(WRITE $<TARGET_FILE:lean>
+              "#!/bin/sh\n${NODE_JS} $<TARGET_FILE:lean>.js \"$@\"\n")
+      execute_process(COMMAND chmod +x $<TARGET_FILE:lean>)
 
       # legacy code for mkleanbook
       # copy olean files from the library into build/emscripten/shell/library/...
@@ -111,41 +91,24 @@ if(NOT STAGE0)
                -s \"BINARYEN_METHOD='native-wasm,asmjs'\"")
       add_dependencies(lean_js lean_js_library)
       set_target_properties(lean_js PROPERTIES COMPILE_FLAGS --bind -s NO_EXIT_RUNTIME=1)
-
-  else()
-    if (MSVC)
-      ADD_CUSTOM_TARGET(bin_lean ALL
-        COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean>" "$<TARGET_FILE_DIR:lean>/mpir.dll" "${LEAN_SOURCE_DIR}/../bin/"
-        DEPENDS bin_lean_stage0
-      )
-    else()
-      ADD_CUSTOM_TARGET(bin_lean ALL
-        COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean>" "$<TARGET_LINKER_FILE:lean>" "${LEAN_SOURCE_DIR}/../bin/"
-        DEPENDS bin_lean_stage0
-      )
-      ADD_CUSTOM_TARGET(bin_lean_stage2
-        COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean_stage2>" "${LEAN_SOURCE_DIR}/../bin/"
-      )
-    endif()
-  endif()
 endif()
 
-# add_test(example1_stdin1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../tests/lean/single.lean")
-# add_test(lean_export ${CMAKE_CURRENT_BINARY_DIR}/lean "-o simple.olean" "${LEAN_SOURCE_DIR}/../tests/lean/run/simple.lean")
-add_test(lean_help1    "${CMAKE_CURRENT_BINARY_DIR}/lean" --help)
-add_test(lean_help2    "${CMAKE_CURRENT_BINARY_DIR}/lean" -h)
-add_test(lean_version1 "${CMAKE_CURRENT_BINARY_DIR}/lean" --version)
+# add_test(example1_stdin1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_BINARY_DIR}/bin/lean "${LEAN_SOURCE_DIR}/../tests/lean/single.lean")
+# add_test(lean_export ${CMAKE_BINARY_DIR}/bin/lean "-o simple.olean" "${LEAN_SOURCE_DIR}/../tests/lean/run/simple.lean")
+add_test(lean_help1    "${CMAKE_BINARY_DIR}/bin/lean" --help)
+add_test(lean_help2    "${CMAKE_BINARY_DIR}/bin/lean" -h)
+add_test(lean_version1 "${CMAKE_BINARY_DIR}/bin/lean" --version)
 if (NOT ${EMSCRIPTEN})
-add_test(lean_version2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --v)
+add_test(lean_version2 "${CMAKE_BINARY_DIR}/bin/lean" --v)
 endif()
-add_test(lean_ghash1   "${CMAKE_CURRENT_BINARY_DIR}/lean" -g)
-add_test(lean_ghash2   "${CMAKE_CURRENT_BINARY_DIR}/lean" --githash)
-# add_test(lean_new_frontend "${LEAN_SOURCE_DIR}/../bin/lean" --new-frontend "${LEAN_SOURCE_DIR}/Init/Core.lean")
-add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "-z")
-add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean")
+add_test(lean_ghash1   "${CMAKE_BINARY_DIR}/bin/lean" -g)
+add_test(lean_ghash2   "${CMAKE_BINARY_DIR}/bin/lean" --githash)
+# add_test(lean_new_frontend "${CMAKE_BINARY_DIR}/bin/lean" --new-frontend "${LEAN_SOURCE_DIR}/Init/Core.lean")
+add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "-z")
+add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "boofoo.lean")
 
 # MSYS2 bash usually handles Windows paths relatively well, but not when putting them in the PATH
-string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${LEAN_SOURCE_DIR}/../bin")
+string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
 
 # LEAN TESTS
 file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
diff --git a/stage0/src/CMakeLists.txt b/stage0/src/CMakeLists.txt
index 560245e850..f885506665 100644
--- a/stage0/src/CMakeLists.txt
+++ b/stage0/src/CMakeLists.txt
@@ -459,8 +459,8 @@ if(USE_GITHASH)
   get_git_head_revision(GIT_REFSPEC GIT_SHA1)
   if(${GIT_SHA1} MATCHES "GITDIR-NOTFOUND")
     message(STATUS "Failed to read git_sha1")
-    if(EXISTS "${LEAN_SOURCE_DIR}/../bin/package_version")
-      file(STRINGS "${LEAN_SOURCE_DIR}/../bin/package_version" LEAN_PACKAGE_VERSION)
+    if(EXISTS "${LEAN_SOURCE_DIR}/bin/package_version")
+      file(STRINGS "${LEAN_SOURCE_DIR}/bin/package_version" LEAN_PACKAGE_VERSION)
       message(STATUS "Package version detected: ${LEAN_PACKAGE_VERSION}")
     endif()
   else()
@@ -468,8 +468,8 @@ if(USE_GITHASH)
   endif()
 else()
   set(GIT_SHA1 "GITDIR-NOTFOUND")
-  if(EXISTS "${LEAN_SOURCE_DIR}/../bin/package_version")
-    file(STRINGS "${LEAN_SOURCE_DIR}/../bin/package_version" LEAN_PACKAGE_VERSION)
+  if(EXISTS "${LEAN_SOURCE_DIR}/bin/package_version")
+    file(STRINGS "${LEAN_SOURCE_DIR}/bin/package_version" LEAN_PACKAGE_VERSION)
     message(STATUS "Package version detected: ${LEAN_PACKAGE_VERSION}")
   endif()
 endif()
@@ -483,14 +483,9 @@ endif ()
 
 # Version
 configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/version.h")
-# Remark: we did not put `config.h` in `${LEAN_BINARY_DIR}` because `leanc` depends on this file.
-# Note that, `leanc` already had problems with multiple configurations before we added `config.h`.
-# For example, it uses binary files located in the `bin` directory.
-configure_file("${LEAN_SOURCE_DIR}/config.h.in" "${LEAN_SOURCE_DIR}/config.h")
-install(FILES "${LEAN_SOURCE_DIR}/config.h" DESTINATION "${INCLUDE_DIR}")
-if(NOT STAGE0)
-  configure_file("${LEAN_SOURCE_DIR}/Makefile.in" "${LEAN_SOURCE_DIR}/Makefile")
-endif()
+configure_file("${LEAN_SOURCE_DIR}/config.h.in" "${LEAN_BINARY_DIR}/include/config.h")
+install(FILES "${LEAN_SOURCE_DIR}/include/config.h" DESTINATION "${INCLUDE_DIR}")
+configure_file("${LEAN_SOURCE_DIR}/Makefile.in" "${LEAN_BINARY_DIR}/share/lean/Makefile")
 
 include_directories("${LEAN_BINARY_DIR}")
 add_subdirectory(runtime)
@@ -515,7 +510,6 @@ add_subdirectory(initialize)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:initialize>)
 if(STAGE0)
   add_subdirectory(../stdlib stdlib)
-  set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:stage0>)
 endif()
 if(EMSCRIPTEN)
     set(LEAN_LIBRARY_TYPE SHARED)
@@ -534,7 +528,7 @@ if(NOT STAGE0)
       -DCHECK_OLEAN_VERSION=${CHECK_OLEAN_VERSION}
       "-DCMAKE_C_COMPILER=${CMAKE_C_COMPILER}"
       "-DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER}"
-    BUILD_COMMAND $(MAKE) lean  # build executable only
+    BUILD_COMMAND $(MAKE)  # build executable only
     BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
     INSTALL_COMMAND ""  # skip install
   )
@@ -542,42 +536,36 @@ endif()
 
 add_library(leanstatic ${LEAN_LIBRARY_TYPE} ${LEAN_OBJS})
 target_link_libraries(leanstatic ${EXTRA_LIBS})
+set_target_properties(leanstatic PROPERTIES ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib")
 
 if(LLVM)
   target_link_libraries(leanstatic ${llvm_libs})
 endif()
 
-if(NOT STAGE0)
+if(STAGE0)
+  add_library(leanstdlib STATIC $<TARGET_OBJECTS:stage0>)
+else()
   add_library(leanstdlib STATIC IMPORTED)
-  ADD_CUSTOM_TARGET(bin_lib ALL
-     COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin"
-     COMMAND "${CMAKE_COMMAND}" -E copy ${COPY_LIBS} "$<TARGET_FILE:leanstdlib>" "$<TARGET_FILE:leanstatic>" "${LEAN_SOURCE_DIR}/../bin"
-  )
-  # Configure leanc
-  configure_file("${LEAN_SOURCE_DIR}/../bin/leanc.in" "${CMAKE_CURRENT_BINARY_DIR}/tmp/leanc")
-  file(COPY "${CMAKE_CURRENT_BINARY_DIR}/tmp/leanc"
-    DESTINATION "${LEAN_SOURCE_DIR}/../bin"
-    FILE_PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
-  install(FILES "${LEAN_SOURCE_DIR}/../bin/leanc"
-    DESTINATION bin
-    PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
-
-  add_custom_target(bin ALL)
-  add_dependencies(bin bin_lib bin_lean)
 endif()
 
-# The DLL (shared library) is not being generated correctly when we use cross-compilation (i.e., generate the Windows DLL using Linux).
-# For some strange reason, it contains a copy of pthread_equal.
-# Remark: this problem does not happen when we generate the DLL using msys2 on Windows.
-if (NOT("${CROSS_COMPILE}" MATCHES "ON"))
-  if ("${STATIC}" MATCHES "OFF")
-    add_library(leanshared SHARED shared/init.cpp)
-    # see `target_link_libraries(lean ...)`
-    target_link_libraries(leanshared leanstatic leanstdlib leanstatic leanstdlib)
-    install(TARGETS leanshared DESTINATION lib)
-  endif()
-  install(TARGETS leanstatic DESTINATION lib)
-endif()
+configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/bin/leanc")
+install(FILES "${CMAKE_BINARY_DIR}/bin/leanc"
+  DESTINATION bin
+  PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
+
+# shared library deactivated until we figure out the leanstatic/leanstdlib story
+# # The DLL (shared library) is not being generated correctly when we use cross-compilation (i.e., generate the Windows DLL using Linux).
+# # For some strange reason, it contains a copy of pthread_equal.
+# # Remark: this problem does not happen when we generate the DLL using msys2 on Windows.
+# if (NOT("${CROSS_COMPILE}" MATCHES "ON"))
+#   if ("${STATIC}" MATCHES "OFF")
+#     add_library(leanshared SHARED shared/init.cpp)
+#     # see `target_link_libraries(lean ...)`
+#     target_link_libraries(leanshared leanstatic leanstdlib leanstatic leanstdlib)
+#     install(TARGETS leanshared DESTINATION lib)
+#   endif()
+#   install(TARGETS leanstatic DESTINATION lib)
+# endif()
 
 add_subdirectory(shell)
 
@@ -618,24 +606,23 @@ add_test(NAME style_check COMMAND "${PYTHON_EXECUTABLE}" "${LEAN_SOURCE_DIR}/cma
 endif()
 
 add_custom_target(clean-stdlib
-  WORKING_DIRECTORY "${LEAN_SOURCE_DIR}"
-  COMMAND find . -name '*.olean' -delete
-  COMMAND find . -name '*.depend' -delete
-  COMMAND rm -rf ../stage1 "${CMAKE_BINARY_DIR}/stage2" "${CMAKE_BINARY_DIR}/stage3" || true
-  )
+  COMMAND rm -rf "${CMAKE_BINARY_DIR}/lib" "${CMAKE_BINARY_DIR}/stage2" "${CMAKE_BINARY_DIR}/stage3" || true)
 
 add_custom_target(clean-olean
   DEPENDS clean-stdlib)
 
-install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION "${LIBRARY_DIR}"
+install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION "${LIBRARY_DIR}/lean"
+        FILES_MATCHING
+        PATTERN "*.olean")
+
+install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION "${LIBRARY_DIR}/lean/src"
         FILES_MATCHING
         PATTERN "*.lean"
-        PATTERN "*.olean"
         PATTERN "*.md")
 
-install(DIRECTORY "${CMAKE_SOURCE_DIR}/runtime" DESTINATION "${INCLUDE_DIR}"
-        FILES_MATCHING
-        PATTERN "*.h")
+add_custom_target(include_runtime ALL
+  COMMAND cmake -E copy_directory "${CMAKE_SOURCE_DIR}/runtime" "${CMAKE_BINARY_DIR}/include/runtime")
+install(FILES "${CMAKE_SOURCE_DIR}/runtime/lean.h" DESTINATION "${INCLUDE_DIR}/runtime")
 
 if("${INCLUDE_MSYS2_DLLS}" MATCHES "ON")
   # TODO(Leo): do not use hardlinks to required DLLs.
diff --git a/stage0/src/bin/lean-gdb.py b/stage0/src/bin/lean-gdb.py
new file mode 100644
index 0000000000..cd8e7fbd1f
--- /dev/null
+++ b/stage0/src/bin/lean-gdb.py
@@ -0,0 +1,323 @@
+# -*- coding: utf-8 -*-
+#
+# Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+# Released under Apache 2.0 license as described in the file LICENSE.
+#
+# Authors: Sebastian Ullrich, Gabriel Ebner
+#
+
+import gdb
+import gdb.printing
+
+def is_scalar(o):
+    return o.cast(gdb.lookup_type('uintptr_t')) & 1 == 1
+
+def box(n):
+    return gdb.Value(n << 1 | 1).cast(gdb.lookup_type('lean_object').pointer())
+
+def unbox(o):
+    return o.cast(gdb.lookup_type('uintptr_t')) >> 1
+
+def to_cnstr(o):
+    return o.cast(gdb.lookup_type('lean_ctor_object').pointer())
+
+def get_tag(header):
+    return header >> (32 + 8 + 8 + 8)
+
+def get_cnstr_tag(o):
+    return get_tag(int(o.cast(gdb.lookup_type('lean_ctor_object').pointer()).dereference()['m_header']['m_header']))
+
+def get_num_objs(header):
+    return (header >> (32 + 8 + 8)) & 0xFF
+
+def get_mem_kind(header):
+    return (header >> (32 + 8)) & 0xFF
+
+def get_rc(header):
+    return header & 0xFFFFFFFF
+
+char_p = gdb.lookup_type('char').pointer()
+
+def get_cnstr_obj_arg(o, i):
+    return o.cast(gdb.lookup_type('lean_ctor_object').pointer()).dereference()['m_objs'][i]
+
+def get_closure_arg(o, i):
+    return o.cast(gdb.lookup_type('lean_closure_object').pointer()).dereference()['m_objs'][i]
+
+def get_c_str(o):
+    return o.cast(gdb.lookup_type('lean_string_object').pointer()).dereference()['m_data'].reference_value().cast(char_p)
+
+class LeanObjectPrinter:
+    """Print a lean_object object."""
+
+    kinds = [
+        # 244, ...
+        ('ctor', []),
+        ('closure', ['m_arity', 'm_fun', 'm_num_fixed']),
+        ('array', ['m_size', 'm_capacity']),
+        ('sarray', ['m_size', 'm_capacity']),
+        ('sarray', ['m_size', 'm_capacity']),
+        ('string', ['m_size', 'm_capacity', 'm_length']),
+        ('mpz', ['m_value']),
+        ('thunk', ['m_value', 'm_closure']),
+        ('task', ['m_value', 'm_imp']),
+        ('ref', ['m_value']),
+        ('external', ['m_class', 'm_data']),
+    ]
+    lean_max_ctor_tag = 244
+
+    def __init__(self, val):
+        self.val = val.address
+        if not is_scalar(self.val):
+            self.header = int(self.val.dereference()['m_header'])
+            self.kind = max(0, get_tag(self.header) - LeanObjectPrinter.lean_max_ctor_tag)
+
+    def to_string(self):
+        if is_scalar(self.val):
+            return unbox(self.val)
+        else:
+            k = get_mem_kind(self.header)
+            return "{} ({})".format(LeanObjectPrinter.kinds[self.kind][0],
+                                    get_rc(self.header) if k == 0 else
+                                    get_rc(self.header) + "/MT" if k == 1 else
+                                    "PERSIST")
+
+    def children(self):
+        if is_scalar(self.val):
+            return
+        if self.kind >= len(LeanObjectPrinter.kinds):
+            return
+        typ, fields = LeanObjectPrinter.kinds[self.kind]
+        val = self.val.cast(gdb.lookup_type("lean_" + typ + "_object").pointer()).dereference()
+        for f in fields:
+            yield (f, val[f])
+        if typ == 'ctor':
+            for i in range(get_num_objs(self.header)):
+                yield ('', val['m_objs'][i].cast(gdb.lookup_type('lean_object').pointer()))
+        elif typ == 'array':
+            for i in range(val['m_size']):
+                yield ('', val['m_data'][i].cast(gdb.lookup_type('lean_object').pointer()))
+        elif typ == 'closure':
+            for i in range(val['m_num_fixed']):
+                yield ('', val['m_objs'][i].cast(gdb.lookup_type('lean_object').pointer()))
+        elif typ == 'string':
+            yield ('', val['m_data'].reference_value().cast(char_p))
+
+
+class LeanOptionalPrinter:
+    """Print a lean::optional object."""
+
+    def __init__(self, val):
+        self.val = val
+
+    def get_val(self):
+        if hasattr(self.val, 'm_some'):
+            if not self.val['m_some']:
+                return None
+        elif not self.val['m_value'].cast(gdb.lookup_type('char').pointer()):
+            return None
+        return self.val['m_value']
+
+    def children(self):
+        val = self.get_val()
+        return [('', val)] if val else []
+
+    def to_string(self):
+        return str(self.val.type)
+
+class LeanNamePrinter:
+    """Print a lean::name object."""
+
+    def __init__(self, val):
+        self.val = val
+
+    def to_string(self):
+        def rec(o):
+            prefix = get_cnstr_obj_arg(o, 0)
+            part = get_cnstr_obj_arg(o, 1)
+            s = ("'%s'" % get_c_str(part).string()) if get_cnstr_tag(o) == 1 else str(unbox(part))
+            if not is_scalar(prefix):
+                return "%s.%s" % (rec(prefix), s)
+            else:
+                return s
+
+        if is_scalar(self.val['m_obj']):
+            return ""
+        else:
+            return rec(self.val['m_obj'])
+
+class LeanExprPrinter:
+    """Print a lean::expr object."""
+
+    expr_kinds = [
+        ('bvar', [('idx', 'nat')]),
+        ('fvar', ['name']),
+        ('mvar', ['name', ('type', 'expr')]),
+        ('sort', ['level']),
+        ('const', ['name', ('levels', 'list_ref<lean::level>')]),
+        ('app', [('fn', 'expr'), ('arg', 'expr')]),
+        ('lam', ['name', ('type', 'expr'), ('body', 'expr')]),
+        ('pi', ['name', ('type', 'expr'), ('body', 'expr')]),
+        ('let', ['name', ('type', 'expr'), ('val', 'expr'), ('body', 'expr')]),
+        ('lit', ['literal']),
+        ('mdata', ['kvmap', 'expr']),
+        ('proj', ['name', 'nat', 'expr']),
+        ('elet', ['name', 'name', 'expr']),
+    ]
+
+
+    def __init__(self, val):
+        self.val = val
+
+    def to_string(self):
+        return 'lean::expr[{}]'.format(LeanExprPrinter.expr_kinds[get_cnstr_tag(self.val['m_obj'])][0])
+
+    def children(self):
+        _, fields = LeanExprPrinter.expr_kinds[get_cnstr_tag(self.val['m_obj'])]
+        for i, f in enumerate(fields):
+            if isinstance(f, tuple):
+                name, typ = f
+            else:
+                name, typ = f, f
+            yield (name, get_cnstr_obj_arg(self.val['m_obj'], i).cast(gdb.lookup_type('lean::' + typ)))
+
+class LeanLevelPrinter:
+    """Print a lean::level object."""
+
+    level_kinds = [
+        ('lean::level_cell', 'zero', []),
+        ('lean::level_succ', 'succ', ['m_l']),
+        ('lean::level_max_core', 'max', ['m_lhs', 'm_rhs']),
+        ('lean::level_max_core', 'imax', ['m_lhs', 'm_rhs']),
+        ('lean::level_param_core', 'param', ['m_id']),
+        ('lean::level_param_core', 'meta', ['m_id']),
+    ]
+
+    def __init__(self, val):
+        self.val = val
+
+    def to_string(self):
+        kind = int(self.val['m_obj']['m_kind'])
+        (subtype, name, fields) = LeanLevelPrinter.level_kinds[kind]
+        subtype = gdb.lookup_type(subtype)
+        val = self.val['m_obj'].cast(subtype.pointer()).dereference()
+        return "({})".format(" ".join([name] + [str(val[field]) for field in fields]))
+
+class LeanListPrinter:
+    """Print a lean::list object."""
+
+    def __init__(self, val):
+        self.val = val
+
+    def children(self):
+        l = self.val
+        i = 0
+        while l['m_obj']:
+            cell = l['m_obj'].dereference()
+            yield ('[%s]' % i, cell['m_head'])
+            l = cell['m_tail']
+            i += 1
+
+    def to_string(self):
+        return str(self.val.type)
+
+    def display_hint(self):
+        return 'array'
+
+class LeanBufferPrinter:
+    """Print a lean::buffer object."""
+
+    def __init__(self, val):
+        self.val = val
+
+    def children(self):
+        p = self.val['m_buffer']
+        for i in range(int(self.val['m_pos'])):
+            yield ('[%s]' % i, p.dereference())
+            p += 1
+
+    def to_string(self):
+        return str(self.val.type)
+
+    def display_hint(self):
+        return 'array'
+
+class LeanListRefPrinter:
+    """Print a lean::list_ref object."""
+
+    def __init__(self, val):
+        self.val = val
+
+    def children(self):
+        l = self.val['m_obj']
+        i = 0
+        while not is_scalar(l):
+            yield ('[%s]' % i, get_cnstr_obj_arg(l, 0).cast(self.val.type.template_argument(0)))
+            l = get_cnstr_obj_arg(l, 1)
+            i += 1
+
+    def to_string(self):
+        return str(self.val.type)
+
+    def display_hint(self):
+        return 'array'
+
+class LeanRBTreePrinter:
+    """Print a lean::rb_tree object."""
+
+    def __init__(self, val):
+        self.val = val
+
+    def children(self):
+        def rec(node):
+            if node['m_ptr']:
+                cell = node['m_ptr'].dereference()
+                for i in rec(cell['m_left']): yield i
+                yield ('', cell['m_value'])
+                for i in rec(cell['m_right']): yield i
+        return rec(self.val['m_root'])
+
+    def to_string(self):
+        return 'lean::rb_tree' # full type is way too verbose
+
+    def display_hint(self):
+        return 'array'
+
+class LeanRBMapPrinter:
+    """Print a lean::rb_map object."""
+
+    def __init__(self, val):
+        self.val = val
+
+    def children(self):
+        for (_, child) in LeanRBTreePrinter(self.val['m_map']).children():
+            yield ('', child['first'])
+            yield ('', child['second'])
+
+    def to_string(self):
+        return 'lean::rb_map' # full type is way too verbose
+
+    def display_hint(self):
+        return 'map'
+
+def build_pretty_printer():
+    pp = gdb.printing.RegexpCollectionPrettyPrinter("lean")
+    pp.add_printer('object', '^lean(_|::)object$', LeanObjectPrinter)
+    pp.add_printer('optional', '^lean::optional', LeanOptionalPrinter)
+    pp.add_printer('name', '^lean::name$', LeanNamePrinter)
+    pp.add_printer('expr', '^lean::expr$', LeanExprPrinter)
+    #pp.add_printer('level', '^lean::level$', LeanLevelPrinter)
+    #pp.add_printer('list', '^lean::list', LeanListPrinter)
+    pp.add_printer('buffer', '^lean::buffer', LeanBufferPrinter)
+    pp.add_printer('list_ref', '^lean::list_ref', LeanListRefPrinter)
+    pp.add_printer('rb_tree', '^lean::rb_tree', LeanRBTreePrinter)
+    pp.add_printer('rb_map', '^lean::rb_map', LeanRBMapPrinter)
+    return pp
+
+def register():
+    gdb.printing.register_pretty_printer(
+        gdb.current_objfile(),
+        build_pretty_printer(),
+        replace=True)
+
+register()
diff --git a/stage0/src/bin/leanc.in b/stage0/src/bin/leanc.in
new file mode 100755
index 0000000000..ecee8ea9d4
--- /dev/null
+++ b/stage0/src/bin/leanc.in
@@ -0,0 +1,29 @@
+#!/usr/bin/env bash
+# Lean compiler
+#
+# A simple wrapper around a C compiler. Defaults to the compiler Lean was built with,
+# which can be overridden with the environment variable `LEAN_CC`. All parameters are passed
+# as-is to the wrapped compiler.
+#
+# Interesting options:
+# * `-U LEAN_MULTI_THREAD` can be used to optimize programs not making use of multi-threading
+
+set -e
+bindir=$(dirname $0)
+
+# link to C++ part of Lean, Lean part of Lean, C++ stdlib, C math library (`sin` etc.)
+# NOTE: leanstatic and leanstdlib are cyclically dependent
+linker_flags="-lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lstdc++ -lm"
+for arg in "$@"; do
+    [[ $arg == "-shared" ]] && linker_flags="$linker_flags @LEANC_SHARED_LINKER_FLAGS@"
+done
+
+# Check C compiler
+for cc in $LEAN_CC @CMAKE_C_COMPILER@ /usr/bin/gcc; do
+    if [ -f $cc ] || command -v $cc; then
+        export LEAN_CC=$cc && break
+    fi
+done
+[ -f $LEAN_CC ] || command -v $LEAN_CC || error "no suitable C compiler found!"
+
+@CMAKE_C_COMPILER_LAUNCHER@ $LEAN_CC -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" $linker_flags -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
diff --git a/stage0/src/runtime/CMakeLists.txt b/stage0/src/runtime/CMakeLists.txt
index d07219307e..51228101bd 100644
--- a/stage0/src/runtime/CMakeLists.txt
+++ b/stage0/src/runtime/CMakeLists.txt
@@ -4,9 +4,3 @@ serializer.cpp stackinfo.cpp compact.cpp init_module.cpp io.cpp hash.cpp
 platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp)
 add_library(runtime OBJECT ${RUNTIME_OBJS})
 add_library(leanruntime ${RUNTIME_OBJS})
-
-ADD_CUSTOM_TARGET(bin_runtime ALL
-  COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin"
-  COMMAND "${CMAKE_COMMAND}" -E copy "${CMAKE_CURRENT_BINARY_DIR}/libleanruntime.a" "${LEAN_SOURCE_DIR}/../bin"
-  DEPENDS leanruntime
-)
diff --git a/stage0/src/shell/CMakeLists.txt b/stage0/src/shell/CMakeLists.txt
index 22f3b1a21a..b675a74512 100644
--- a/stage0/src/shell/CMakeLists.txt
+++ b/stage0/src/shell/CMakeLists.txt
@@ -1,75 +1,54 @@
 if(NOT STAGE0)
-  add_executable(lean_stage0 IMPORTED)
-  set_target_properties(lean_stage0 PROPERTIES IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage0/shell/lean${CMAKE_EXECUTABLE_SUFFIX}")
-
-  ADD_CUSTOM_TARGET(bin_lean_stage0
-    COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean_stage0>" "${LEAN_SOURCE_DIR}/../bin/lean_stage0${CMAKE_EXECUTABLE_SUFFIX}"
-    DEPENDS stage0
-  )
-
   string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
   set(LEANC_OPTS "${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}")
 
   add_custom_target(make_stdlib
     WORKING_DIRECTORY "${LEAN_SOURCE_DIR}"
-    COMMAND ${CMAKE_COMMAND} -E env "LEAN_PATH=Init=Init" $(MAKE) "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a"
-      "LEAN=$<TARGET_FILE:lean_stage0>"
-      "LEANC_OPTS=${LEANC_OPTS}"
-      "OUT=${CMAKE_BINARY_DIR}/stage1"
-      # share .c files between different build configurations
-      "C_OUT=${LEAN_SOURCE_DIR}/stage1"
+    COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/stage0/bin:$$PATH $(MAKE) -f ${CMAKE_BINARY_DIR}/share/lean/Makefile OUT=${CMAKE_BINARY_DIR}/lib"
     DEPENDS stage0)
   set_target_properties(leanstdlib PROPERTIES
-    IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a"
+    IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/libleanstdlib.a"
     IMPORTED_LINK_INTERFACE_LIBRARIES leanstatic)
   add_dependencies(leanstdlib make_stdlib)
   install(FILES "$<TARGET_FILE:leanstdlib>" DESTINATION lib)
 
-  set(PREV_LEAN "$<TARGET_FILE:lean>")
+  set(PREV_STAGE_DIR "${CMAKE_BINARY_DIR}")
   foreach(STAGE RANGE 2 3)
     add_custom_target(make_stdlib_stage${STAGE}
-      COMMAND cd "${LEAN_SOURCE_DIR}" && find . '\(' -name Makefile -o -name relative.py -o -name '*.lean' '\)' -exec "${CMAKE_COMMAND}" -E copy_if_different '{}' ${CMAKE_BINARY_DIR}/stage${STAGE}/'{}' '\;'
-      COMMAND cd "${CMAKE_BINARY_DIR}/stage${STAGE}" && LEAN_PATH=Init=Init $(MAKE) ./libleanstdlib.a
-        "LEAN=${PREV_LEAN}"
-        "LEANC=${LEAN_SOURCE_DIR}/../bin/leanc"
-        "LEAN_ROOT=${LEAN_SOURCE_DIR}"
-        "LEANC_OPTS=${LEANC_OPTS}"
-        "OUT=."
-        # recreate everything if the previous compiler has changed
-        "MORE_DEPS=${PREV_LEAN}"
-    )
+      # recreate everything if the previous compiler has changed
+      COMMAND bash -c "PATH=${PREV_STAGE}/bin:$$PATH $(MAKE) -f ${CMAKE_BINARY_DIR}/share/lean/Makefile OUT=${CMAKE_BINARY_DIR}/stage${STAGE}/lib MORE_DEPS=${PREV_STAGE}/bin/lean"
+      DEPENDS lean_stage${PREV_STAGE})
     add_library(leanstdlib_stage${STAGE} STATIC IMPORTED)
     set_target_properties(leanstdlib_stage${STAGE} PROPERTIES
-      IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage${STAGE}/libleanstdlib.a"
+      IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage${STAGE}/lib/libleanstdlib.a"
       IMPORTED_LINK_INTERFACE_LIBRARIES leanstatic)
     add_dependencies(leanstdlib_stage${STAGE} make_stdlib_stage${STAGE})
     add_executable(lean_stage${STAGE} EXCLUDE_FROM_ALL lean.cpp)
     # see `target_link_libraries(lean ...)` below
     target_link_libraries(lean_stage${STAGE} leanstatic leanstdlib_stage${STAGE} leanstatic leanstdlib_stage${STAGE})
-    set(PREV_LEAN "$<TARGET_FILE:lean_stage${STAGE}>")
+    set(PREV_STAGE ${STAGE})
+    set(PREV_STAGE_DIR "${CMAKE_BINARY_DIR}/stage${STAGE}")
   endforeach()
 
   add_custom_target(check-stage3
     COMMAND diff "$<TARGET_FILE:lean_stage2>" "$<TARGET_FILE:lean_stage3>")
 
   add_custom_target(update-stage0
-    COMMAND make update-stage0
-      "OUT=${CMAKE_BINARY_DIR}/stage1"
-      "C_OUT=${LEAN_SOURCE_DIR}/stage1"
+    COMMAND make update-stage0 -f ${CMAKE_BINARY_DIR}/share/lean/Makefile
+      "OUT=${CMAKE_BINARY_DIR}/lib"
     DEPENDS leanstdlib
     WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}")
 endif()
 
 add_executable(lean lean.cpp)
-if(STAGE0)
-  target_link_libraries(lean leanstatic)
-else()
-  # `leanstatic` and `leanstdlib` are cyclically dependent static libraries.
-  # We use the approach described at
-  # https://cmake.org/cmake/help/v3.3/command/target_link_libraries.html#cyclic-dependencies-of-static-libraries
-  # We don't want to add leanstdlib as a direct dependency of leanstatic since this is only true for stage 1.
-  target_link_libraries(lean leanstatic leanstdlib leanstatic leanstdlib)
-endif()
+set_target_properties(lean PROPERTIES RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/bin")
+
+# `leanstatic` and `leanstdlib` are cyclically dependent static libraries.
+# We use the approach described at
+# https://cmake.org/cmake/help/v3.3/command/target_link_libraries.html#cyclic-dependencies-of-static-libraries
+# We don't want to add leanstdlib as a direct dependency of leanstatic since this is only true for stage 1.
+target_link_libraries(lean leanstatic leanstdlib leanstatic leanstdlib)
+
 # create import library on Windows to link plugins against
 set_target_properties(lean PROPERTIES ENABLE_EXPORTS ON)
 if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
@@ -78,23 +57,22 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
 endif()
 install(TARGETS lean DESTINATION bin)
 
-if(NOT STAGE0)
-  if(${EMSCRIPTEN})
+if(NOT STAGE0 AND EMSCRIPTEN)
       set(NODE_JS "node --stack_size=8192")
 
-      file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/lean_with_path
-              "#!/bin/sh\nLEAN_PATH=Init=${CMAKE_CURRENT_SOURCE_DIR}/.. ${NODE_JS} ${CMAKE_CURRENT_BINARY_DIR}/lean.js \"$@\"\n")
-      execute_process(COMMAND chmod +x ${CMAKE_CURRENT_BINARY_DIR}/lean_with_path)
+      file(WRITE $<TARGET_FILE:lean>_with_path
+              "#!/bin/sh\nLEAN_PATH=Init=${CMAKE_CURRENT_SOURCE_DIR}/.. ${NODE_JS} $<TARGET_FILE:lean>.js \"$@\"\n")
+      execute_process(COMMAND chmod +x $<TARGET_FILE:lean>_with_path)
 
       ADD_CUSTOM_TARGET(bin_lean ALL
-          COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin"
-          COMMAND "${CMAKE_COMMAND}" -E copy "${CMAKE_CURRENT_BINARY_DIR}/lean_with_path" "${LEAN_SOURCE_DIR}/../bin/lean"
+          COMMAND "${CMAKE_COMMAND}" -E make_directory "${CMAKE_BINARY_DIR}/bin"
+          COMMAND "${CMAKE_COMMAND}" -E copy "$<TARGET_FILE:lean>_with_path" "${CMAKE_BINARY_DIR}/bin/lean"
           DEPENDS lean
           )
 
-      file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/lean
-              "#!/bin/sh\n${NODE_JS} ${CMAKE_CURRENT_BINARY_DIR}/lean.js \"$@\"\n")
-      execute_process(COMMAND chmod +x ${CMAKE_CURRENT_BINARY_DIR}/lean)
+      file(WRITE $<TARGET_FILE:lean>
+              "#!/bin/sh\n${NODE_JS} $<TARGET_FILE:lean>.js \"$@\"\n")
+      execute_process(COMMAND chmod +x $<TARGET_FILE:lean>)
 
       # legacy code for mkleanbook
       # copy olean files from the library into build/emscripten/shell/library/...
@@ -111,38 +89,21 @@ if(NOT STAGE0)
                -s \"BINARYEN_METHOD='native-wasm,asmjs'\"")
       add_dependencies(lean_js lean_js_library)
       set_target_properties(lean_js PROPERTIES COMPILE_FLAGS --bind -s NO_EXIT_RUNTIME=1)
-
-  else()
-    if (MSVC)
-      ADD_CUSTOM_TARGET(bin_lean ALL
-        COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean>" "$<TARGET_FILE_DIR:lean>/mpir.dll" "${LEAN_SOURCE_DIR}/../bin/"
-        DEPENDS bin_lean_stage0
-      )
-    else()
-      ADD_CUSTOM_TARGET(bin_lean ALL
-        COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean>" "$<TARGET_LINKER_FILE:lean>" "${LEAN_SOURCE_DIR}/../bin/"
-        DEPENDS bin_lean_stage0
-      )
-      ADD_CUSTOM_TARGET(bin_lean_stage2
-        COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean_stage2>" "${LEAN_SOURCE_DIR}/../bin/"
-      )
-    endif()
-  endif()
 endif()
 
-# add_test(example1_stdin1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../tests/lean/single.lean")
-# add_test(lean_export ${CMAKE_CURRENT_BINARY_DIR}/lean "-o simple.olean" "${LEAN_SOURCE_DIR}/../tests/lean/run/simple.lean")
-add_test(lean_help1    "${CMAKE_CURRENT_BINARY_DIR}/lean" --help)
-add_test(lean_help2    "${CMAKE_CURRENT_BINARY_DIR}/lean" -h)
-add_test(lean_version1 "${CMAKE_CURRENT_BINARY_DIR}/lean" --version)
+# add_test(example1_stdin1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_BINARY_DIR}/bin/lean "${LEAN_SOURCE_DIR}/../tests/lean/single.lean")
+# add_test(lean_export ${CMAKE_BINARY_DIR}/bin/lean "-o simple.olean" "${LEAN_SOURCE_DIR}/../tests/lean/run/simple.lean")
+add_test(lean_help1    "${CMAKE_BINARY_DIR}/bin/lean" --help)
+add_test(lean_help2    "${CMAKE_BINARY_DIR}/bin/lean" -h)
+add_test(lean_version1 "${CMAKE_BINARY_DIR}/bin/lean" --version)
 if (NOT ${EMSCRIPTEN})
-add_test(lean_version2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --v)
+add_test(lean_version2 "${CMAKE_BINARY_DIR}/bin/lean" --v)
 endif()
-add_test(lean_ghash1   "${CMAKE_CURRENT_BINARY_DIR}/lean" -g)
-add_test(lean_ghash2   "${CMAKE_CURRENT_BINARY_DIR}/lean" --githash)
-# add_test(lean_new_frontend "${LEAN_SOURCE_DIR}/../bin/lean" --new-frontend "${LEAN_SOURCE_DIR}/Init/Core.lean")
-add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "-z")
-add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean")
+add_test(lean_ghash1   "${CMAKE_BINARY_DIR}/bin/lean" -g)
+add_test(lean_ghash2   "${CMAKE_BINARY_DIR}/bin/lean" --githash)
+# add_test(lean_new_frontend "${CMAKE_BINARY_DIR}/bin/lean" --new-frontend "${LEAN_SOURCE_DIR}/Init/Core.lean")
+add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "-z")
+add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "boofoo.lean")
 
 # LEAN TESTS
 file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
@@ -151,7 +112,7 @@ FOREACH(T ${LEANTESTS})
     GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
     add_test(NAME "leantest_${T_NAME}"
              WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean"
-             COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}")
+             COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/bin:$PATH ./test_single.sh ${T_NAME}")
   endif()
 ENDFOREACH(T)
 
@@ -162,7 +123,7 @@ FOREACH(T ${LEANRUNTESTS})
     GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
     add_test(NAME "leanruntest_${T_NAME}"
              WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run"
-             COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}")
+             COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/bin:$PATH ./test_single.sh ${T_NAME}")
   endif()
 ENDFOREACH(T)
 
@@ -173,7 +134,7 @@ FOREACH(T ${LEANNEWFRONTENDTESTS})
     GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
     add_test(NAME "leannewfrontendtest_${T_NAME}"
              WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/newfrontend"
-             COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}")
+             COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/bin:$PATH ./test_single.sh ${T_NAME}")
   endif()
 ENDFOREACH(T)
 
@@ -183,7 +144,7 @@ FOREACH(T ${LEANCOMPTESTS})
   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
   add_test(NAME "leancomptest_${T_NAME}"
            WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler"
-           COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}")
+           COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/bin:$PATH ./test_single.sh ${T_NAME}")
 ENDFOREACH(T)
 
 # LEAN INTERPRETER TESTS
@@ -193,7 +154,7 @@ FOREACH(T ${LEANINTERPTESTS})
     GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
     add_test(NAME "leaninterptest_${T_NAME}"
              WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler"
-             COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single_interpret.sh ${T_NAME}")
+             COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/bin:$PATH ./test_single_interpret.sh ${T_NAME}")
   endif()
 ENDFOREACH(T)
 
@@ -205,7 +166,7 @@ FOREACH(T_OUT ${LEANBENCHTESTS})
   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
   add_test(NAME "leanbenchtest_${T_NAME}"
            WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/bench"
-           COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}")
+           COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/bin:$PATH ./test_single.sh ${T_NAME}")
 ENDFOREACH(T_OUT)
 
 # LEAN PLUGIN TESTS
@@ -214,7 +175,7 @@ FOREACH(T ${LEANINTERPTESTS})
   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
   add_test(NAME "leanplugintest_${T_NAME}"
            WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/plugin"
-           COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}")
+           COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/bin:$PATH ./test_single.sh ${T_NAME}")
 ENDFOREACH(T)
 
 # LEAN TESTS using --trust=0
@@ -223,5 +184,5 @@ FOREACH(T ${LEANT0TESTS})
   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
   add_test(NAME "leant0test_${T_NAME}"
            WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/trust0"
-           COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}")
+           COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/bin:$PATH ./test_single.sh ${T_NAME}")
 ENDFOREACH(T)
diff --git a/tests/.gitignore b/tests/.gitignore
new file mode 100644
index 0000000000..a6f6b3d04f
--- /dev/null
+++ b/tests/.gitignore
@@ -0,0 +1 @@
+*.olean
\ No newline at end of file
diff --git a/tests/lean/ctor_layout.lean b/tests/lean/ctor_layout.lean
index 1ac357fc1b..ae61cf7f62 100644
--- a/tests/lean/ctor_layout.lean
+++ b/tests/lean/ctor_layout.lean
@@ -3,8 +3,7 @@ open Lean
 open Lean.IR
 
 def tst : IO Unit :=
-do initSearchPath "Init=../../src/Init";
-   env ← importModules [{module := `Init.Lean.Compiler.IR.Basic}];
+do env ← importModules [{module := `Init.Lean.Compiler.IR.Basic}];
    ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.IR.Expr.reuse;
    ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
    IO.println "---";