refactor(*): integrate emscripten build
This commit is contained in:
Gabriel Ebner
Leonardo de Moura
parent
0f72de217a
commit
ec0aa6d248
14 changed files with 331 additions and 80 deletions
|
|
@ -463,7 +463,7 @@ def make_build_ninja(args):
|
|||
|
||||
print("""rule LEAN""", file=f)
|
||||
print(""" depfile = ${DLEAN_FILE}""", file=f)
|
||||
print(""" command = "%s" %s $in -o "${OLEAN_FILE}" """ \
|
||||
print(""" command = "%s" %s -o ${OLEAN_FILE} $in""" \
|
||||
% (g_lean_path, " ".join(args.lean_options)), file=f)
|
||||
|
||||
print("build all: phony", end=' ', file=f)
|
||||
|
|
|
|||
|
|
@ -4,6 +4,19 @@ set(LEAN_VERSION_MAJOR 0)
|
|||
set(LEAN_VERSION_MINOR 3)
|
||||
set(LEAN_VERSION_PATCH 0)
|
||||
|
||||
set(LEAN_EXTRA_LINKER_FLAGS "")
|
||||
set(LEAN_EXTRA_CXX_FLAGS "")
|
||||
|
||||
if("${CMAKE_C_COMPILER}" MATCHES "emcc")
|
||||
set(EMSCRIPTEN ON)
|
||||
set(CROSS_COMPILE ON)
|
||||
set(IGNORE_SORRY ON)
|
||||
set(MULTI_THREAD OFF)
|
||||
set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_EMSCRIPTEN")
|
||||
set(LEAN_JS_LIBRARY "${CMAKE_CURRENT_SOURCE_DIR}/../library" CACHE STRING
|
||||
"location of olean files for lean.js")
|
||||
endif()
|
||||
|
||||
if (NOT CMAKE_BUILD_TYPE)
|
||||
message(STATUS "No build type selected, default to Release")
|
||||
set(CMAKE_BUILD_TYPE "Release")
|
||||
|
|
@ -63,9 +76,6 @@ include(CTest)
|
|||
configure_file("${LEAN_SOURCE_DIR}/CTestCustom.cmake.in"
|
||||
"${LEAN_BINARY_DIR}/CTestCustom.cmake" @ONLY)
|
||||
|
||||
set(LEAN_EXTRA_LINKER_FLAGS "")
|
||||
set(LEAN_EXTRA_CXX_FLAGS "")
|
||||
|
||||
# Windows does not support ulimit -s unlimited. So, we reserve a lot of stack space: 100Mb
|
||||
if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
|
||||
message(STATUS "Windows detected")
|
||||
|
|
@ -112,12 +122,6 @@ if(STATIC)
|
|||
set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -static")
|
||||
endif()
|
||||
|
||||
if("${CMAKE_C_COMPILER}" MATCHES "emcc")
|
||||
set(EMSCRIPTEN ON)
|
||||
set(CROSS_COMPILE ON)
|
||||
set(IGNORE_SORRY ON)
|
||||
endif()
|
||||
|
||||
# Set Module Path
|
||||
set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules")
|
||||
|
||||
|
|
@ -128,7 +132,7 @@ set(CMAKE_CXX_FLAGS_MINSIZEREL "-Os -DNDEBUG")
|
|||
set(CMAKE_CXX_FLAGS_RELEASE "-O3 -DNDEBUG")
|
||||
set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g")
|
||||
set(CMAKE_CXX_FLAGS_GPROF "-O2 -g -pg")
|
||||
set(CMAKE_CXX_FLAGS_EMSCRIPTEN "-Oz -O3 -s ALLOW_MEMORY_GROWTH=1 --llvm-lto 1 -s DISABLE_EXCEPTION_CATCHING=0 -D LEAN_EMSCRIPTEN -Wno-warn-absolute-paths --bind")
|
||||
set(CMAKE_CXX_FLAGS_EMSCRIPTEN "-Oz -O3 -s ALLOW_MEMORY_GROWTH=1 --llvm-lto 1 -s DISABLE_EXCEPTION_CATCHING=0 -Wno-warn-absolute-paths")
|
||||
|
||||
# OSX .dmg generation (this is working in progress)
|
||||
set(CPACK_DMG_BACKGROUND_IMAGE "${LEAN_SOURCE_DIR}/../images/lean.png")
|
||||
|
|
@ -209,15 +213,47 @@ if (BOOST AND MULTI_THREAD)
|
|||
endif()
|
||||
endif()
|
||||
|
||||
# MPFR
|
||||
find_package(MPFR 3.1.0 REQUIRED)
|
||||
include_directories(${MPFR_INCLUDES})
|
||||
set(EXTRA_LIBS ${EXTRA_LIBS} ${MPFR_LIBRARIES})
|
||||
if (${EMSCRIPTEN})
|
||||
include(ExternalProject)
|
||||
set(gmp_install_prefix ${CMAKE_CURRENT_BINARY_DIR}/gmp-root)
|
||||
# The plethory of configure arguments only makes sure that gmp thinks sizeof(mp_limb_t) == sizeof(long) == 4
|
||||
ExternalProject_Add(
|
||||
gmp
|
||||
URL https://leanprover.github.io/lean.js/gmp-5.1.1.tar.bz2
|
||||
URL_HASH SHA256=9a30128284cb710cdc0d71866ed582bc0c97cff3a077ff70739f1d979c76279e
|
||||
BUILD_IN_SOURCE 1
|
||||
CONFIGURE_COMMAND emconfigure ./configure CFLAGS=-m32\ -DPIC --build=i686-pc-linux-gnu --disable-assembly --prefix=${gmp_install_prefix}
|
||||
BUILD_COMMAND emmake make -j4
|
||||
INSTALL_COMMAND make install
|
||||
)
|
||||
set(mpfr_install_prefix ${CMAKE_CURRENT_BINARY_DIR}/mpfr-root)
|
||||
ExternalProject_Add(
|
||||
mpfr
|
||||
DEPENDS gmp
|
||||
URL https://leanprover.github.io/lean.js/mpfr-3.1.1.tar.bz2
|
||||
URL_HASH SHA256=7b66c3f13dc8385f08264c805853f3e1a8eedab8071d582f3e661971c9acd5fd
|
||||
BUILD_IN_SOURCE 1
|
||||
CONFIGURE_COMMAND emconfigure ./configure --prefix=${mpfr_install_prefix} --with-gmp-include=${gmp_install_prefix}/include --with-gmp-lib=${gmp_install_prefix}/lib
|
||||
BUILD_COMMAND emmake make -j4
|
||||
INSTALL_COMMAND make install
|
||||
)
|
||||
|
||||
# GMP
|
||||
find_package(GMP 5.0.5 REQUIRED)
|
||||
include_directories(${GMP_INCLUDE_DIR})
|
||||
set(EXTRA_LIBS ${EXTRA_LIBS} ${GMP_LIBRARIES})
|
||||
add_library(lean_external_deps INTERFACE)
|
||||
target_link_libraries(lean_external_deps INTERFACE ${gmp_install_prefix}/lib/libgmp.a ${mpfr_install_prefix}/lib/libmpfr.a)
|
||||
include_directories(lean_external_deps INTERFACE ${gmp_install_prefix}/include ${mpfr_install_prefix}/include)
|
||||
add_dependencies(lean_external_deps gmp mpfr)
|
||||
set(EXTRA_LIBS lean_external_deps)
|
||||
else()
|
||||
# MPFR
|
||||
find_package(MPFR 3.1.0 REQUIRED)
|
||||
include_directories(${MPFR_INCLUDES})
|
||||
set(EXTRA_LIBS ${EXTRA_LIBS} ${MPFR_LIBRARIES})
|
||||
|
||||
# GMP
|
||||
find_package(GMP 5.0.5 REQUIRED)
|
||||
include_directories(${GMP_INCLUDE_DIR})
|
||||
set(EXTRA_LIBS ${EXTRA_LIBS} ${GMP_LIBRARIES})
|
||||
endif()
|
||||
|
||||
# TRACK_MEMORY_USAGE
|
||||
if(TRACK_MEMORY_USAGE)
|
||||
|
|
@ -362,9 +398,13 @@ if(MULTI_THREAD AND (NOT ("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")) AND (NOT BOO
|
|||
set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread")
|
||||
endif()
|
||||
set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage")
|
||||
if(NOT EMSCRIPTEN)
|
||||
add_library(leanstatic ${LEAN_OBJS})
|
||||
if(EMSCRIPTEN)
|
||||
set(LEAN_LIBRARY_TYPE SHARED)
|
||||
else()
|
||||
set(LEAN_LIBRARY_TYPE STATIC)
|
||||
endif()
|
||||
add_library(leanstatic ${LEAN_LIBRARY_TYPE} ${LEAN_OBJS})
|
||||
target_link_libraries(leanstatic ${EXTRA_LIBS})
|
||||
if ((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
|
||||
set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -Wl,--export-all")
|
||||
endif()
|
||||
|
|
@ -416,30 +456,6 @@ add_style_check_target(style "${LEAN_SOURCES}")
|
|||
add_test(NAME style_check COMMAND "${PYTHON_EXECUTABLE}" "${LEAN_SOURCE_DIR}/cmake/Modules/cpplint.py" ${LEAN_SOURCES})
|
||||
endif()
|
||||
|
||||
# Set PROCESSOR_COUNT
|
||||
if(NOT DEFINED PROCESSOR_COUNT)
|
||||
# Unknown:
|
||||
set(PROCESSOR_COUNT 1)
|
||||
|
||||
# Linux:
|
||||
set(cpuinfo_file "/proc/cpuinfo")
|
||||
if(EXISTS "${cpuinfo_file}")
|
||||
file(STRINGS "${cpuinfo_file}" procs REGEX "^processor.: [0-9]+$")
|
||||
list(LENGTH procs PROCESSOR_COUNT)
|
||||
endif()
|
||||
|
||||
# Mac:
|
||||
if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
|
||||
execute_process(COMMAND "sysctl" "hw.ncpu" OUTPUT_VARIABLE info)
|
||||
string(REGEX REPLACE "^hw.ncpu: ([0-9]+).*$" "\\1" PROCESSOR_COUNT "${info}")
|
||||
endif()
|
||||
|
||||
# Windows:
|
||||
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
|
||||
set(PROCESSOR_COUNT "$ENV{NUMBER_OF_PROCESSORS}")
|
||||
endif()
|
||||
endif()
|
||||
|
||||
if("${CROSS_COMPILE}" MATCHES "ON" OR "${CMAKE_C_COMPILER}" MATCHES "emcc")
|
||||
message(STATUS "Lean standard library will not be compiled when using cross-compilation.")
|
||||
else()
|
||||
|
|
|
|||
|
|
@ -344,7 +344,6 @@ struct import_modules_fn {
|
|||
}
|
||||
|
||||
module_info_ptr load_module_file(std::string const & base, module_name const & mname) {
|
||||
std::string fname_lean = find_lean_file(base, mname);
|
||||
std::string fname = find_olean_file(base, mname);
|
||||
auto it = m_module_info.find(fname);
|
||||
if (it)
|
||||
|
|
@ -357,8 +356,11 @@ struct import_modules_fn {
|
|||
try {
|
||||
module_metadata metadata;
|
||||
metadata.m_mname = mname;
|
||||
metadata.m_lean_mod_time = get_mtime(fname_lean);
|
||||
metadata.m_olean_mod_time = get_mtime(fname);
|
||||
try {
|
||||
std::string fname_lean = find_lean_file(base, mname);
|
||||
metadata.m_lean_mod_time = get_mtime(fname_lean);
|
||||
} catch (...) {}
|
||||
try { metadata.m_olean_mod_time = get_mtime(fname); } catch (...) {}
|
||||
m_imported.insert(fname, metadata);
|
||||
|
||||
unsigned major, minor, patch, claimed_hash;
|
||||
|
|
@ -500,7 +502,7 @@ struct import_modules_fn {
|
|||
object_readers & readers = get_object_readers();
|
||||
auto it = readers.find(k);
|
||||
if (it == readers.end())
|
||||
throw exception(sstream() << "file '" << r->m_fname << "' has been corrupted, unknown object");
|
||||
throw exception(sstream() << "file '" << r->m_fname << "' has been corrupted, unknown object: " << k);
|
||||
it->second(d, m_senv, add_asynch_update, add_delayed_update);
|
||||
}
|
||||
obj_counter++;
|
||||
|
|
|
|||
|
|
@ -1,19 +1,49 @@
|
|||
add_executable(lean lean.cpp json.cpp server.cpp)
|
||||
target_link_libraries(lean leanstatic)
|
||||
install(TARGETS lean DESTINATION bin)
|
||||
|
||||
add_executable(lean_js lean_js.cpp)
|
||||
target_link_libraries(lean_js leanstatic)
|
||||
|
||||
if(${EMSCRIPTEN})
|
||||
add_executable(lean.js lean.cpp emscripten.cpp ${LEAN_OBJS})
|
||||
target_link_libraries(lean.js ${EXTRA_LIBS} "--embed-file library --memory-init-file 0")
|
||||
target_link_libraries(lean "--memory-init-file 0")
|
||||
|
||||
file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/run_lean_js
|
||||
"#!/bin/sh\nLEAN_PATH=${CMAKE_CURRENT_SOURCE_DIR}/../../library node ${CMAKE_CURRENT_BINARY_DIR}/lean.js \"$@\"\n")
|
||||
execute_process(COMMAND chmod +x ${CMAKE_CURRENT_BINARY_DIR}/run_lean_js)
|
||||
|
||||
# FIXME(gabriel): we rebuild the library using lean.js because the serialization is different
|
||||
file(READ ${CMAKE_CURRENT_SOURCE_DIR}/../../bin/linja.in linja_code)
|
||||
string(REGEX REPLACE "\ng_lean_path[^\n]* = [^\n]*" "\ng_lean_path = '${CMAKE_CURRENT_BINARY_DIR}/run_lean_js'" linja_js_code ${linja_code})
|
||||
string(REGEX REPLACE "ninja_option = \\[\\]" "ninja_option = ['-j1']" linja_js_code ${linja_js_code})
|
||||
string(REGEX REPLACE " make_deps_all_files\\(args\\)" " #" linja_js_code ${linja_js_code})
|
||||
file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/linja_js ${linja_js_code})
|
||||
execute_process(COMMAND chmod +x ${CMAKE_CURRENT_BINARY_DIR}/linja_js)
|
||||
add_custom_target(build_lean_js_library
|
||||
COMMAND find -name \\*.olean -exec rm '{}' \\\;
|
||||
COMMAND ${CMAKE_CURRENT_BINARY_DIR}/linja_js
|
||||
WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/../../library)
|
||||
|
||||
# copy olean files from the library into build/emscripten/shell/library/...
|
||||
add_custom_target(lean_js_library
|
||||
COMMAND rm -rf ${CMAKE_CURRENT_BINARY_DIR}/library
|
||||
COMMAND mkdir -p ${CMAKE_CURRENT_BINARY_DIR}/library
|
||||
COMMAND bash -c "(cd ${LEAN_JS_LIBRARY}; tar c `find -name '*.olean'`) | (cd ${CMAKE_CURRENT_BINARY_DIR}/library; tar x)"
|
||||
VERBATIM)
|
||||
|
||||
file(COPY ${CMAKE_CURRENT_SOURCE_DIR}/lean_js.html DESTINATION ${CMAKE_CURRENT_BINARY_DIR})
|
||||
|
||||
target_link_libraries(lean_js "--embed-file library --memory-init-file 0 --bind")
|
||||
add_dependencies(lean_js lean_js_library)
|
||||
set_target_properties(lean_js PROPERTIES COMPILE_FLAGS --bind -s NO_EXIT_RUNTIME=1)
|
||||
else()
|
||||
add_executable(lean lean.cpp emscripten.cpp json.cpp server.cpp)
|
||||
target_link_libraries(lean leanstatic ${EXTRA_LIBS})
|
||||
ADD_CUSTOM_COMMAND(TARGET lean
|
||||
POST_BUILD
|
||||
COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin"
|
||||
COMMAND "${CMAKE_COMMAND}" -E copy "${CMAKE_CURRENT_BINARY_DIR}/lean${CMAKE_EXECUTABLE_SUFFIX}" "${LEAN_SOURCE_DIR}/../bin/"
|
||||
)
|
||||
install(TARGETS lean DESTINATION bin)
|
||||
endif()
|
||||
|
||||
add_library(shell OBJECT emscripten.cpp)
|
||||
|
||||
# add_test(example1_stdin1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../tests/lean/single.lean")
|
||||
# add_test(lean_export ${CMAKE_CURRENT_BINARY_DIR}/lean "-o simple.olean" "${LEAN_SOURCE_DIR}/../tests/lean/run/simple.lean")
|
||||
add_test(lean_help1 "${CMAKE_CURRENT_BINARY_DIR}/lean" --help)
|
||||
|
|
|
|||
|
|
@ -37,12 +37,14 @@ Author: Leonardo de Moura
|
|||
#include "frontends/lean/opt_cmd.h"
|
||||
#include "frontends/smt2/parser.h"
|
||||
#include "init/init.h"
|
||||
#include "shell/emscripten.h"
|
||||
#include "shell/simple_pos_info_provider.h"
|
||||
#include "shell/json.h"
|
||||
#if defined(LEAN_SERVER)
|
||||
#include "shell/server.h"
|
||||
#endif
|
||||
#if defined(LEAN_EMSCRIPTEN)
|
||||
#include <emscripten.h>
|
||||
#endif
|
||||
#include "version.h"
|
||||
#include "githash.h" // NOLINT
|
||||
|
||||
|
|
@ -210,15 +212,6 @@ options set_config_option(options const & opts, char const * in) {
|
|||
}
|
||||
}
|
||||
|
||||
#if defined(LEAN_EMSCRIPTEN)
|
||||
#include <emscripten/bind.h>
|
||||
EMSCRIPTEN_BINDINGS(LEAN_JS) {
|
||||
emscripten::function("lean_init", &initialize_emscripten);
|
||||
emscripten::function("lean_import_module", &emscripten_import_module);
|
||||
emscripten::function("lean_process_file", &emscripten_process_file);
|
||||
}
|
||||
int main() { return 0; }
|
||||
#else
|
||||
class initializer {
|
||||
private:
|
||||
lean::initializer m_init;
|
||||
|
|
@ -236,6 +229,26 @@ public:
|
|||
};
|
||||
|
||||
int main(int argc, char ** argv) {
|
||||
#if defined(LEAN_EMSCRIPTEN)
|
||||
EM_ASM(
|
||||
var lean_path = process.env['LEAN_PATH'];
|
||||
if (lean_path) {
|
||||
ENV['LEAN_PATH'] = lean_path;
|
||||
}
|
||||
|
||||
try {
|
||||
// emscripten cannot mount all of / in the vfs,
|
||||
// we can only mount subdirectories...
|
||||
FS.mount(NODEFS, { root: '/home' }, '/home');
|
||||
FS.mkdir('/root');
|
||||
FS.mount(NODEFS, { root: '/root' }, '/root');
|
||||
|
||||
FS.chdir(process.cwd());
|
||||
} catch (e) {
|
||||
console.log(e);
|
||||
}
|
||||
);
|
||||
#endif
|
||||
initializer init;
|
||||
bool export_objects = false;
|
||||
unsigned trust_lvl = LEAN_BELIEVER_TRUST_LEVEL+1;
|
||||
|
|
@ -449,4 +462,3 @@ int main(int argc, char ** argv) {
|
|||
}
|
||||
return 1;
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
103
src/shell/lean_js.cpp
Normal file
103
src/shell/lean_js.cpp
Normal file
|
|
@ -0,0 +1,103 @@
|
|||
/*
|
||||
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include <string>
|
||||
#include "library/flycheck.h"
|
||||
#include "library/module.h"
|
||||
#include "library/standard_kernel.h"
|
||||
#include "library/type_context.h"
|
||||
#include "frontends/lean/pp.h"
|
||||
#include "frontends/lean/parser.h"
|
||||
#include "init/init.h"
|
||||
#include "shell/simple_pos_info_provider.h"
|
||||
|
||||
namespace lean {
|
||||
class emscripten_shell {
|
||||
private:
|
||||
unsigned trust_lvl;
|
||||
unsigned num_threads;
|
||||
options opts;
|
||||
environment env;
|
||||
io_state ios;
|
||||
|
||||
public:
|
||||
emscripten_shell() : trust_lvl(LEAN_BELIEVER_TRUST_LEVEL+1), num_threads(1),
|
||||
env(mk_environment(trust_lvl)), ios(opts, lean::mk_pretty_formatter_factory()) {
|
||||
ios.set_message_channel(std::make_shared<flycheck_message_stream>(std::cout));
|
||||
}
|
||||
|
||||
int import_module(std::string mname) {
|
||||
try {
|
||||
module_name mod(mname);
|
||||
std::string base = ".";
|
||||
bool num_threads = 1;
|
||||
// FIXME(gabriel): discarding proofs fails at the moment with "invalid equation lemma, unexpected form"
|
||||
bool keep_proofs = true;
|
||||
env = import_modules(env, base, 1, &mod, num_threads, keep_proofs, ios);
|
||||
} catch (lean::exception & ex) {
|
||||
lean::message_builder(env, ios, "import_module", lean::pos_info(1, 1), lean::ERROR).set_exception(ex).report();
|
||||
return 1;
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
||||
int process_file(std::string input_filename) {
|
||||
bool ok = true;
|
||||
try {
|
||||
environment temp_env(env);
|
||||
io_state temp_ios(ios);
|
||||
if (!parse_commands(temp_env, temp_ios, input_filename.c_str(), optional<std::string>(), false, num_threads)) {
|
||||
ok = false;
|
||||
}
|
||||
} catch (lean::exception & ex) {
|
||||
lean::message_builder(env, ios, input_filename, lean::pos_info(1, 1), lean::ERROR).set_exception(ex).report();
|
||||
ok = false;
|
||||
}
|
||||
return ok ? 0 : 1;
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
static lean::initializer * g_init = nullptr;
|
||||
static lean::emscripten_shell * g_shell = nullptr;
|
||||
|
||||
void initialize_emscripten() {
|
||||
g_init = new lean::initializer();
|
||||
g_shell = new lean::emscripten_shell();
|
||||
}
|
||||
|
||||
void finalize_emscripten() {
|
||||
delete g_shell;
|
||||
delete g_init;
|
||||
}
|
||||
|
||||
int emscripten_import_module(std::string mname) {
|
||||
return g_shell->import_module(mname);
|
||||
}
|
||||
|
||||
int emscripten_process_file(std::string input_filename) {
|
||||
return g_shell->process_file(input_filename);
|
||||
}
|
||||
|
||||
#if defined(LEAN_EMSCRIPTEN)
|
||||
|
||||
#include <emscripten/bind.h>
|
||||
EMSCRIPTEN_BINDINGS(LEAN_JS) {
|
||||
emscripten::function("lean_init", &initialize_emscripten);
|
||||
emscripten::function("lean_import_module", &emscripten_import_module);
|
||||
emscripten::function("lean_process_file", &emscripten_process_file);
|
||||
}
|
||||
|
||||
int main() { return 0; }
|
||||
|
||||
#else
|
||||
|
||||
int main(int, char **) {
|
||||
initialize_emscripten();
|
||||
emscripten_import_module("standard");
|
||||
}
|
||||
|
||||
#endif
|
||||
81
src/shell/lean_js.html
Normal file
81
src/shell/lean_js.html
Normal file
|
|
@ -0,0 +1,81 @@
|
|||
<html>
|
||||
<head>
|
||||
<title>lean.js minimal working example</title>
|
||||
<meta charset="utf-8">
|
||||
</head>
|
||||
<body>
|
||||
|
||||
<p>Small example of using lean.js</p>
|
||||
|
||||
<pre id="output"></pre>
|
||||
|
||||
<script type="text/javascript">
|
||||
var myTimer = null;
|
||||
function now () { return (new Date()).getTime(); }
|
||||
function startTimer () { myTimer = now(); }
|
||||
function checkTimer () { return '(took ' + (now() - myTimer) + 'ms)'; }
|
||||
|
||||
var outputElement = document.getElementById("output");
|
||||
function outputLog(msg) {
|
||||
console.log(msg);
|
||||
outputElement.appendChild(document.createTextNode(String(msg) + "\n"));
|
||||
}
|
||||
|
||||
/*
|
||||
* "Module" must be initialized before the <script> tag for lean.js.
|
||||
* The lean.js script populates Module with compiled Lean code,
|
||||
* but it needs to know about the parameters below or it will throw errors.
|
||||
*/
|
||||
outputLog('--- Loading Lean VM...'); startTimer();
|
||||
Module = { };
|
||||
Module.TOTAL_MEMORY = 64 * 1024 * 1024;
|
||||
Module.noExitRuntime = true;
|
||||
Module.print = function(text) { outputLog(text); };
|
||||
Module.preRun = [
|
||||
function () {
|
||||
outputLog('--- Lean VM loaded. ' + checkTimer());
|
||||
outputLog('--- Running Lean VM...'); startTimer();
|
||||
}
|
||||
];
|
||||
Module.postRun = function () {
|
||||
outputLog('--- Lean VM has been run. ' + checkTimer());
|
||||
}
|
||||
</script>
|
||||
|
||||
<!-- Import the Lean javascript module generated by emscripten. -->
|
||||
<script src="lean_js.js" type="text/javascript" charset="utf-8"></script>
|
||||
|
||||
<script type="text/javascript" charset="utf-8">
|
||||
|
||||
outputLog('--- Calling lean_init()...'); startTimer();
|
||||
Module.lean_init();
|
||||
outputLog('--- lean_init() complete. ' + checkTimer());
|
||||
|
||||
outputLog('--- Importing standard library...'); startTimer();
|
||||
Module.lean_import_module('standard');
|
||||
outputLog('--- Import complete. ' + checkTimer());
|
||||
|
||||
outputLog('--- Writing test.lean to virtual FS...'); startTimer();
|
||||
testfile = ''
|
||||
+ 'variables p q r s : Prop\n'
|
||||
+ 'theorem and_comm : p ∧ q ↔ q ∧ p :=\n'
|
||||
+ 'iff.intro\n'
|
||||
+ ' (assume Hpq : p ∧ q,\n'
|
||||
+ ' and.intro (and.elim_right Hpq) (and.elim_left Hpq))\n'
|
||||
+ ' (assume Hqp : q ∧ p,\n'
|
||||
+ ' and.intro (and.elim_right Hqp) (and.elim_left Hqp))\n'
|
||||
+ 'check @nat.rec_on\n'
|
||||
+ 'print "end of file!"\n';
|
||||
outputLog( testfile );
|
||||
FS.writeFile('test.lean', testfile, { encoding: 'utf8' });
|
||||
outputLog('--- test.lean written. ' + checkTimer());
|
||||
|
||||
outputLog('--- Running Lean on test.lean...'); startTimer();
|
||||
Module.lean_process_file('test.lean');
|
||||
outputLog('--- Lean has been run on test.lean. ' + checkTimer());
|
||||
|
||||
outputLog("--- Finished.");
|
||||
|
||||
</script>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -56,7 +56,9 @@ void server::run() {
|
|||
/* Leo: we use std::setlocale to make sure decimal period is displayed as ".".
|
||||
We added this hack because the json library code used for ensuring this property
|
||||
was crashing when compiling Lean on Windows with mingw. */
|
||||
#if !defined(LEAN_EMSCRIPTEN)
|
||||
std::setlocale(LC_NUMERIC, "C");
|
||||
#endif
|
||||
while (true) {
|
||||
try {
|
||||
std::string req_string;
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
add_executable(shell_test shell.cpp ${LEAN_OBJS} $<TARGET_OBJECTS:shell>)
|
||||
add_executable(shell_test shell.cpp ${LEAN_OBJS})
|
||||
target_link_libraries(shell_test ${EXTRA_LIBS})
|
||||
|
||||
# TODO(Leo): add after stdlib is activated again
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ Author: Leonardo de Moura
|
|||
*/
|
||||
#include <vector>
|
||||
#include "util/test.h"
|
||||
#include "shell/emscripten.h"
|
||||
#include "shell/lean_js.h"
|
||||
using namespace lean;
|
||||
|
||||
int main() {
|
||||
|
|
|
|||
|
|
@ -40,7 +40,13 @@ bool is_directory(char const * pathname) {
|
|||
return info.st_mode & S_IFDIR;
|
||||
}
|
||||
|
||||
#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
|
||||
#if defined(LEAN_EMSCRIPTEN)
|
||||
// emscripten version
|
||||
static char g_path_sep = ':';
|
||||
static char g_sep = '/';
|
||||
static char g_bad_sep = '\\';
|
||||
bool is_path_sep(char c) { return c == g_path_sep; }
|
||||
#elif defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
|
||||
// Windows version
|
||||
static char g_path_sep = ';';
|
||||
static char g_path_alt_sep = ':';
|
||||
|
|
@ -118,19 +124,19 @@ std::string get_path(std::string f) {
|
|||
}
|
||||
|
||||
void init_lean_path() {
|
||||
#if defined(LEAN_EMSCRIPTEN)
|
||||
*g_lean_path = "/library";
|
||||
g_lean_path_vector->push_back(*g_lean_path);
|
||||
#else
|
||||
char * r = nullptr;
|
||||
r = getenv("LEAN_PATH");
|
||||
if (r == nullptr) {
|
||||
#ifdef LEAN_EMSCRIPTEN
|
||||
*g_lean_path = "/library";
|
||||
#else
|
||||
std::string exe_path = get_path(get_exe_location());
|
||||
*g_lean_path = exe_path + g_sep + ".." + g_sep + "library";
|
||||
*g_lean_path += g_path_sep;
|
||||
*g_lean_path += exe_path + g_sep + ".." + g_sep + "lib" + g_sep + "lean" + g_sep + "library";
|
||||
*g_lean_path += g_path_sep;
|
||||
*g_lean_path += ".";
|
||||
#endif
|
||||
} else {
|
||||
*g_lean_path = r;
|
||||
}
|
||||
|
|
@ -148,7 +154,6 @@ void init_lean_path() {
|
|||
}
|
||||
if (j > i)
|
||||
g_lean_path_vector->push_back(g_lean_path->substr(i, j - i));
|
||||
#endif
|
||||
}
|
||||
|
||||
static char g_sep_str[2];
|
||||
|
|
|
|||
|
|
@ -85,10 +85,8 @@ name::name(name const & prefix, char const * name) {
|
|||
m_ptr = new (mem) imp(true, prefix.m_ptr);
|
||||
std::memcpy(mem + sizeof(imp), name, sz + 1);
|
||||
m_ptr->m_str = mem + sizeof(imp);
|
||||
if (m_ptr->m_prefix)
|
||||
m_ptr->m_hash = hash_str(sz, name, m_ptr->m_prefix->m_hash);
|
||||
else
|
||||
m_ptr->m_hash = hash_str(sz, name, 0);
|
||||
// Emscripten easily breaks with small changes here. The main fix seems to be to use m_ptr->m_str instead of name.
|
||||
m_ptr->m_hash = hash_str(static_cast<unsigned>(sz), m_ptr->m_str, prefix.hash());
|
||||
}
|
||||
|
||||
name::name(name const & prefix, unsigned k, bool) {
|
||||
|
|
|
|||
|
|
@ -21,7 +21,9 @@ Author: Leonardo de Moura
|
|||
|
||||
namespace lean {
|
||||
std::string lrealpath(char const * fname) {
|
||||
#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
|
||||
#if defined(LEAN_EMSCRIPTEN)
|
||||
return fname;
|
||||
#elif defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
|
||||
constexpr unsigned BufferSize = 8192;
|
||||
char buffer[BufferSize];
|
||||
DWORD retval = GetFullPathName(fname, BufferSize, buffer, nullptr);
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue