michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(kernel): start version 0.2, new kernel with universe polymorphism and better/cleaner support for metavariables

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-12 10:54:03 -08:00
parent 0c1674ab70
commit 1b6b33b3f5
2 changed files with 38 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

56
src/CMakeLists.txt
View file

@ -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)

17
src/kernel/CMakeLists.txt
View file

@ -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})