From ab974c1c4cfffe3d1a5542654ef7cd84e5decf8e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 20 Mar 2019 14:27:17 +0100 Subject: [PATCH] chore(shell/CMakeLists,library/Makefile): store stage1 C++ output in build directory --- library/Makefile.in | 4 +++- src/CMakeLists.txt | 2 +- src/shell/CMakeLists.txt | 4 ++-- src/stage0/init/control/except.cpp | 30 ++++++++++++++++++++++++++++++ src/stage0/init/io.cpp | 30 ------------------------------ 5 files changed, 36 insertions(+), 34 deletions(-) diff --git a/library/Makefile.in b/library/Makefile.in index 9263800083..7d77ae3673 100644 --- a/library/Makefile.in +++ b/library/Makefile.in @@ -7,7 +7,9 @@ OBJS = $(SRCS:.lean=.olean) DEPS = $(SRCS:.lean=.depend) OPTS = @LEAN_EXTRA_MAKE_OPTS@ STAGE0_DIR = ../src/stage0 -STAGE1_DIR = ../src/stage1 +ifndef STAGE1_DIR +$(error "`STAGE1_DIR` must be set (use cmake)") +endif CPPS = $(addprefix $(STAGE1_DIR)/,$(patsubst %.lean,%.cpp,$(SRCS))) # ensure deterministic ordering CPPS_CORE=$(sort $(patsubst %.lean,%.cpp,$(SRCS))) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 02e6c4e74f..8d79d4ae36 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -536,7 +536,7 @@ endif() add_custom_target(clean-stdlib WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library" - COMMAND make clean + COMMAND make clean STAGE1_DIR="${CMAKE_BINARY_DIR}/stage1" ) add_custom_target(clean-leanpkg diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 826d20fdb9..1c024a5cb8 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -10,11 +10,11 @@ add_custom_target(stdlib # '-G Ninja' complains otherwise BYPRODUCTS "${LEAN_SOURCE_DIR}/stage1/libleanstdlib.a" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library" - COMMAND make -j8 ../src/stage1/libleanstdlib.a "LEAN=$" + COMMAND make -j8 "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a" "LEAN=$" "STAGE1_DIR=${CMAKE_BINARY_DIR}/stage1" DEPENDS lean_stage0) add_custom_target(update-stage0 - COMMAND make update-stage0 + COMMAND make update-stage0 "STAGE1_DIR=${CMAKE_BINARY_DIR}/stage1" DEPENDS lean WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}/../library") diff --git a/src/stage0/init/control/except.cpp b/src/stage0/init/control/except.cpp index 5347ca8e52..8c075b95e8 100644 --- a/src/stage0/init/control/except.cpp +++ b/src/stage0/init/control/except.cpp @@ -50,6 +50,7 @@ obj* l_monad__except_orelse___boxed(obj*, obj*); obj* l_except__t_monad(obj*, obj*); obj* l_except__t_return___boxed(obj*, obj*); obj* l_except__t_bind__cont___at_except__t_monad___spec__6___rarg___boxed(obj*, obj*, obj*, obj*, obj*); +obj* l_except_inhabited___rarg(obj*); obj* l_monad__except_lift__except___rarg___boxed(obj*, obj*, obj*, obj*, obj*); obj* l_except__t_monad__functor(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_except_monad___lambda__4___boxed(obj*, obj*, obj*, obj*); @@ -68,6 +69,7 @@ obj* l_except_monad___closed__1; obj* l_except__t_catch___rarg___lambda__1(obj*, obj*, obj*); obj* l_except_monad___lambda__2(obj*, obj*, obj*, obj*); obj* l_except__t_bind__cont___at_except__t_monad___spec__2___boxed(obj*, obj*); +obj* l_except_inhabited(obj*, obj*); obj* l_except__t_monad__run___boxed(obj*, obj*, obj*); obj* l_except_repr___boxed(obj*, obj*); obj* l_except_has__to__string___boxed(obj*, obj*); @@ -143,6 +145,7 @@ obj* l_except_monad__except___lambda__1___boxed(obj*, obj*); obj* l_except__t_bind__cont___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_except_monad___lambda__2___boxed(obj*, obj*, obj*, obj*); obj* l_except_map__error___main___rarg(obj*, obj*); +obj* l_except_inhabited___boxed(obj*, obj*); obj* l_except_repr___main___rarg(obj*, obj*, obj*); obj* l_except_to__bool(obj*, obj*); obj* l_except__t_bind__cont___at_except__t_monad___spec__5___rarg(obj*, obj*, obj*, obj*, obj*); @@ -231,6 +234,33 @@ obj* l_except__t_bind__cont___at_except__t_monad___spec__2___rarg(obj*, obj*, ob obj* l_except__t_monad___rarg___lambda__8(obj*, obj*); obj* l_except__t_catch___rarg(obj*, obj*, obj*, obj*); obj* l_except__t_return(obj*, obj*); +obj* l_except_inhabited___rarg(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = lean::alloc_cnstr(0, 1, 0); +lean::cnstr_set(x_1, 0, x_0); +return x_1; +} +} +obj* l_except_inhabited(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::alloc_closure(reinterpret_cast(l_except_inhabited___rarg), 1, 0); +return x_2; +} +} +obj* l_except_inhabited___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = l_except_inhabited(x_0, x_1); +lean::dec(x_0); +lean::dec(x_1); +return x_2; +} +} obj* _init_l_except_to__string___main___rarg___closed__1() { _start: { diff --git a/src/stage0/init/io.cpp b/src/stage0/init/io.cpp index 5cca6cc6ab..05aca59046 100644 --- a/src/stage0/init/io.cpp +++ b/src/stage0/init/io.cpp @@ -87,7 +87,6 @@ obj* l_eio_monad__except___boxed(obj*); obj* l_io_ref_read(obj*, obj*); extern "C" obj* lean_io_prim_handle_close(obj*, obj*); obj* l_io_lazy__pure___boxed(obj*); -obj* l_io_prim_inhabited(obj*, obj*); obj* l_io_ref_read___rarg(obj*, obj*, obj*); obj* l_io_println___boxed(obj*); obj* l_io_prim_iterate(obj*, obj*); @@ -104,7 +103,6 @@ obj* l_io_prim_lift__io___rarg(obj*, obj*); obj* l_io_ref_read___boxed(obj*, obj*); obj* l_eio_monad(obj*); obj* l_io_ref_modify___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*); -obj* l_io_prim_inhabited___rarg(obj*); obj* l_io_fs_handle_close___rarg(obj*, obj*); obj* l_eio_monad__except(obj*); obj* l_io_ref_swap___boxed(obj*, obj*); @@ -152,7 +150,6 @@ obj* l_io_ref_modify___rarg___boxed(obj*, obj*, obj*, obj*, obj*); obj* l___private_init_io_1__put__str___at_has__repr_has__eval___spec__3(obj*, obj*); obj* l_io_fs_handle_mk___rarg___boxed(obj*, obj*, obj*, obj*); extern "C" obj* lean_io_timeit(obj*, obj*, obj*, obj*); -obj* l_io_prim_inhabited___boxed(obj*, obj*); obj* l_io_fs_handle_close(obj*, obj*); obj* l_io_prim_iterate___at_io_fs_handle_read__to__end___spec__3___lambda__1(obj*, obj*, obj*); obj* l_io_prim_iterate___at_io_fs_handle_read__to__end___spec__3___lambda__1___boxed(obj*, obj*, obj*); @@ -545,33 +542,6 @@ lean::dec(x_1); return x_2; } } -obj* l_io_prim_inhabited___rarg(obj* x_0) { -_start: -{ -obj* x_1; -x_1 = lean::alloc_cnstr(0, 1, 0); -lean::cnstr_set(x_1, 0, x_0); -return x_1; -} -} -obj* l_io_prim_inhabited(obj* x_0, obj* x_1) { -_start: -{ -obj* x_2; -x_2 = lean::alloc_closure(reinterpret_cast(l_io_prim_inhabited___rarg), 1, 0); -return x_2; -} -} -obj* l_io_prim_inhabited___boxed(obj* x_0, obj* x_1) { -_start: -{ -obj* x_2; -x_2 = l_io_prim_inhabited(x_0, x_1); -lean::dec(x_0); -lean::dec(x_1); -return x_2; -} -} obj* l_io_prim_put__str___boxed(obj* x_0, obj* x_1) { _start: {