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

refactor(frontends/lua): reactivate some of the Lua extensions

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-04-28 17:57:39 -07:00
parent 5fdd2fe3a9
commit af927ecb7a
3 changed files with 15 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/CMakeLists.txt
View file

@ -229,8 +229,8 @@ set(LEAN_LIBS ${LEAN_LIBS} library)
# 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(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()

22
src/frontends/lua/register_modules.cpp
View file

@ -7,21 +7,21 @@ Author: Leonardo de Moura
#include "util/script_state.h"
#include "util/numerics/register_module.h"
#include "util/sexpr/register_module.h"
#include "library/register_module.h"
#include "library/io_state_stream.h"
#include "library/arith/register_module.h"
#include "library/simplifier/register_module.h"
#include "library/tactic/register_module.h"
#include "frontends/lean/register_module.h"
// #include "library/register_module.h"
// #include "library/io_state_stream.h"
// #include "library/arith/register_module.h"
// #include "library/simplifier/register_module.h"
// #include "library/tactic/register_module.h"
// #include "frontends/lean/register_module.h"
namespace lean {
void register_modules() {
register_numerics_module();
register_sexpr_module();
register_core_module();
register_arith_module();
register_simplifier_module();
register_tactic_module();
register_frontend_lean_module();
// register_core_module();
// register_arith_module();
// register_simplifier_module();
// register_tactic_module();
// register_frontend_lean_module();
}
}

4
src/shell/lean.cpp
View file

@ -29,8 +29,8 @@ Author: Leonardo de Moura
#include "frontends/lean/shell.h"
#include "frontends/lean/frontend.h"
#include "frontends/lean/register_module.h"
#include "frontends/lua/register_modules.h"
#endif
#include "frontends/lua/register_modules.h"
#include "version.h"
#include "githash.h" // NOLINT
@ -115,7 +115,7 @@ static struct option g_long_options[] = {
int main(int argc, char ** argv) {
lean::save_stack_info();
// lean::register_modules();
lean::register_modules();
// bool no_kernel = false;
// bool export_objects = false;
// bool trust_imported = false;