From 1b6b33b3f5c8edf4ea079daef5369192a81cffec Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 12 Feb 2014 10:54:03 -0800
Subject: [PATCH] refactor(kernel): start version 0.2, new kernel with universe
 polymorphism and better/cleaner support for metavariables

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/CMakeLists.txt        | 56 +++++++++++++++++++--------------------
 src/kernel/CMakeLists.txt | 17 +++++++-----
 2 files changed, 38 insertions(+), 35 deletions(-)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 22eea3a4d..d15e70526 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1,7 +1,7 @@
 cmake_minimum_required(VERSION 2.8.7)
 project(LEAN CXX)
 set(LEAN_VERSION_MAJOR 0)
-set(LEAN_VERSION_MINOR 1)
+set(LEAN_VERSION_MINOR 2)
 
 set(CMAKE_COLOR_MAKEFILE ON)
 enable_testing()
@@ -213,24 +213,24 @@ add_subdirectory(util/interval)
 set(LEAN_LIBS ${LEAN_LIBS} interval)
 add_subdirectory(kernel)
 set(LEAN_LIBS ${LEAN_LIBS} kernel)
-add_subdirectory(library)
-set(LEAN_LIBS ${LEAN_LIBS} library)
-add_subdirectory(library/arith)
-set(LEAN_LIBS ${LEAN_LIBS} arithlib)
-add_subdirectory(library/rewriter)
-set(LEAN_LIBS ${LEAN_LIBS} rewriter)
-add_subdirectory(library/simplifier)
-set(LEAN_LIBS ${LEAN_LIBS} simplifier)
-add_subdirectory(library/elaborator)
-set(LEAN_LIBS ${LEAN_LIBS} elaborator)
-add_subdirectory(library/tactic)
-set(LEAN_LIBS ${LEAN_LIBS} tactic)
-add_subdirectory(library/error_handling)
-set(LEAN_LIBS ${LEAN_LIBS} error_handling)
-add_subdirectory(frontends/lean)
-set(LEAN_LIBS ${LEAN_LIBS} lean_frontend)
-add_subdirectory(frontends/lua)
-set(LEAN_LIBS ${LEAN_LIBS} leanlua)
+# add_subdirectory(library)
+# set(LEAN_LIBS ${LEAN_LIBS} library)
+# add_subdirectory(library/arith)
+# set(LEAN_LIBS ${LEAN_LIBS} arithlib)
+# add_subdirectory(library/rewriter)
+# set(LEAN_LIBS ${LEAN_LIBS} rewriter)
+# add_subdirectory(library/simplifier)
+# set(LEAN_LIBS ${LEAN_LIBS} simplifier)
+# add_subdirectory(library/elaborator)
+# set(LEAN_LIBS ${LEAN_LIBS} elaborator)
+# add_subdirectory(library/tactic)
+# set(LEAN_LIBS ${LEAN_LIBS} tactic)
+# add_subdirectory(library/error_handling)
+# set(LEAN_LIBS ${LEAN_LIBS} error_handling)
+# add_subdirectory(frontends/lean)
+# set(LEAN_LIBS ${LEAN_LIBS} lean_frontend)
+# add_subdirectory(frontends/lua)
+# set(LEAN_LIBS ${LEAN_LIBS} leanlua)
 if("${MULTI_THREAD}" MATCHES "ON")
    set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINKER_FLAGS}")
 else()
@@ -238,19 +238,19 @@ else()
 endif()
 set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage")
 set(EXTRA_LIBS ${LEAN_LIBS} ${EXTRA_LIBS})
-add_subdirectory(shell)
-add_subdirectory(builtin)
-add_subdirectory(emacs)
+# add_subdirectory(shell)
+# add_subdirectory(builtin)
+# add_subdirectory(emacs)
 
 add_subdirectory(tests/util)
 add_subdirectory(tests/util/numerics)
 add_subdirectory(tests/util/interval)
-add_subdirectory(tests/kernel)
-add_subdirectory(tests/library)
-add_subdirectory(tests/library/rewriter)
-add_subdirectory(tests/library/tactic)
-add_subdirectory(tests/library/elaborator)
-add_subdirectory(tests/frontends/lean)
+# add_subdirectory(tests/kernel)
+# add_subdirectory(tests/library)
+# add_subdirectory(tests/library/rewriter)
+# add_subdirectory(tests/library/tactic)
+# add_subdirectory(tests/library/elaborator)
+# add_subdirectory(tests/frontends/lean)
 
 # Include style check
 include(StyleCheck)
diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index 97bb50efb..f4352fd02 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -1,9 +1,12 @@
-add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp
-  normalizer.cpp context.cpp level.cpp object.cpp environment.cpp
-  type_checker.cpp kernel.cpp occurs.cpp metavar.cpp
-  justification.cpp unification_constraint.cpp kernel_exception.cpp
-  type_checker_justification.cpp pos_info_provider.cpp
-  replace_visitor.cpp update_expr.cpp io_state.cpp max_sharing.cpp
-  universe_constraints.cpp)
+add_library(kernel level.cpp
+# expr.cpp
+# free_vars.cpp abstract.cpp instantiate.cpp
+# normalizer.cpp context.cpp level.cpp object.cpp environment.cpp
+# type_checker.cpp kernel.cpp occurs.cpp metavar.cpp
+# justification.cpp unification_constraint.cpp kernel_exception.cpp
+# type_checker_justification.cpp pos_info_provider.cpp
+# replace_visitor.cpp update_expr.cpp io_state.cpp max_sharing.cpp
+# universe_constraints.cpp
+)
 
 target_link_libraries(kernel ${LEAN_LIBS})