max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove old frontend, equation compiler and tactics from build

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-25 10:20:30 -07:00
parent e28b337a2c
commit 94bc5ed7a3
3 changed files with 16 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/CMakeLists.txt
View file

@ -402,16 +402,10 @@ else()
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:kernel>)
add_subdirectory(library)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:library>)
add_subdirectory(library/tactic)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:tactic>)
add_subdirectory(library/constructions)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:constructions>)
add_subdirectory(library/equations_compiler)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:equations_compiler>)
add_subdirectory(library/compiler)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:compiler>)
add_subdirectory(frontends/lean)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:lean_frontend>)
add_subdirectory(initialize)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:initialize>)
if(${STAGE} EQUAL 0)

9
src/initialize/init.cpp
View file

@ -11,12 +11,9 @@ Author: Leonardo de Moura
#include "util/io.h"
#include "kernel/init_module.h"
#include "library/init_module.h"
#include "library/tactic/init_module.h"
#include "library/constructions/init_module.h"
#include "library/equations_compiler/init_module.h"
#include "library/print.h"
#include "library/compiler/init_module.h"
#include "frontends/lean/init_module.h"
#include "initialize/init.h"
namespace lean {
@ -33,10 +30,7 @@ extern "C" void lean_initialize() {
initialize_library_core_module();
initialize_library_module();
initialize_compiler_module();
initialize_tactic_module();
initialize_constructions_module();
initialize_equations_compiler_module();
initialize_frontend_lean_module();
}
void initialize() {
@ -45,10 +39,7 @@ void initialize() {
void finalize() {
run_thread_finalizers();
finalize_frontend_lean_module();
finalize_equations_compiler_module();
finalize_constructions_module();
finalize_tactic_module();
finalize_compiler_module();
finalize_library_module();
finalize_library_core_module();

19
src/shell/lean.cpp
View file

@ -383,10 +383,23 @@ void environment_free_regions(environment && env) {
consume_io_result(lean_environment_free_regions(env.steal(), io_mk_world()));
}
pos_info get_message_pos(object_ref const & msg);
message_severity get_message_severity(object_ref const & msg);
std::string get_message_string(object_ref const & msg);
extern "C" object * lean_message_pos(object * msg);
extern "C" uint8 lean_message_severity(object * msg);
extern "C" object * lean_message_string(object * msg);
pos_info get_message_pos(object_ref const & msg) {
auto p = pair_ref<nat, nat>(lean_message_pos(msg.to_obj_arg()));
return pos_info(p.fst().get_small_value(), p.snd().get_small_value());
}
message_severity get_message_severity(object_ref const & msg) {
return static_cast<message_severity>(lean_message_severity(msg.to_obj_arg()));
}
std::string get_message_string(object_ref const & msg) {
string_ref r(lean_message_string(msg.to_obj_arg()));
return r.to_std_string();
}
}
void check_optarg(char const * option_name) {