lean_virtual_memory_exhausted.txt

[ 51%] [ 51%] [ 51%] [ 51%] cd /root/lean/build/library/tactic && /usr/bin/c++    -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build    -o CMakeFiles/tactic.dir/contradiction_tactic.cpp.o -c /root/lean/src/library/tactic/contradiction_tactic.cpp
Building CXX object kernel/CMakeFiles/kernel.dir/equiv_manager.cpp.o
cd /root/lean/build/kernel && /usr/bin/c++    -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build    -o CMakeFiles/kernel.dir/equiv_manager.cpp.o -c /root/lean/src/kernel/equiv_manager.cpp
/usr/bin/cmake -E cmake_progress_report /root/lean/build/CMakeFiles
Building CXX object util/CMakeFiles/util.dir/utf8.cpp.o
Building CXX object util/CMakeFiles/util.dir/memory_pool.cpp.o
Building CXX object library/tactic/CMakeFiles/tactic.dir/constructor_tactic.cpp.o
/usr/bin/cmake -E cmake_progress_report /root/lean/build/CMakeFiles 26
cd /root/lean/build/util && /usr/bin/c++    -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build    -o CMakeFiles/util.dir/memory_pool.cpp.o -c /root/lean/src/util/memory_pool.cpp
Building CXX object library/CMakeFiles/library.dir/max_sharing.cpp.o
/usr/bin/cmake -E cmake_progress_report /root/lean/build/CMakeFiles 85
Building CXX object util/CMakeFiles/util.dir/name_map.cpp.o
Building CXX object library/CMakeFiles/library.dir/kernel_serializer.cpp.o
Building CXX object util/CMakeFiles/util.dir/list_fn.cpp.o
/usr/bin/cmake -E cmake_progress_report /root/lean/build/CMakeFiles
Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/decl_cmds.cpp.o
/usr/bin/cmake -E cmake_progress_report /root/lean/build/CMakeFiles
Building CXX object library/tactic/CMakeFiles/tactic.dir/injection_tactic.cpp.o
Building CXX object library/tactic/CMakeFiles/tactic.dir/exfalso_tactic.cpp.o
cd /root/lean/build/util && /usr/bin/c++    -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build    -o CMakeFiles/util.dir/utf8.cpp.o -c /root/lean/src/util/utf8.cpp
Building CXX object library/tactic/CMakeFiles/tactic.dir/congruence_tactic.cpp.o
Building CXX object library/CMakeFiles/library.dir/normalize.cpp.o
cd /root/lean/build/library && /usr/bin/c++    -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build    -o CMakeFiles/library.dir/kernel_serializer.cpp.o -c /root/lean/src/library/kernel_serializer.cpp
[ 51%] virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
make[2]: *** [frontends/lua/CMakeFiles/leanlua.dir/register_modules.cpp.o] Error 1
make[2]: Leaving directory `/root/lean/build'
make[1]: *** [frontends/lua/CMakeFiles/leanlua.dir/all] Error 2
make[1]: *** Waiting for unfinished jobs....
[ 51%] virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
make[2]: *** [kernel/CMakeFiles/kernel.dir/default_converter.cpp.o] Error 1
make[2]: *** Waiting for unfinished jobs....
virtual memory exhausted: Cannot allocate memory
make[2]: *** [frontends/lean/CMakeFiles/lean_frontend.dir/builtin_exprs.cpp.o] Error 1
make[2]: *** Waiting for unfinished jobs....
cd /root/lean/build/frontends/lean && /usr/bin/c++    -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build    -o CMakeFiles/lean_frontend.dir/decl_cmds.cpp.o -c /root/lean/src/frontends/lean/decl_cmds.cpp
make[2]: *** [util/sexpr/CMakeFiles/sexpr.dir/sexpr_fn.cpp.o] Error 1
make[2]: *** Waiting for unfinished jobs....
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/revert_tactic.cpp.o] Error 1
make[2]: *** Waiting for unfinished jobs....
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/change_tactic.cpp.o] Error 1
cd /root/lean/build/library/tactic && /usr/bin/c++    -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build    -o CMakeFiles/tactic.dir/exfalso_tactic.cpp.o -c /root/lean/src/library/tactic/exfalso_tactic.cpp
cd /root/lean/build/library && /usr/bin/c++    -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build    -o CMakeFiles/library.dir/max_sharing.cpp.o -c /root/lean/src/library/max_sharing.cpp
make[2]: *** [util/CMakeFiles/util.dir/thread_script_state.cpp.o] Error 1
make[2]: *** Waiting for unfinished jobs....
cd /root/lean/build/util && /usr/bin/c++    -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build    -o CMakeFiles/util.dir/name_map.cpp.o -c /root/lean/src/util/name_map.cpp
/usr/bin/cmake: error while loading shared libraries: libkrb5.so.26: failed to map segment from shared object: Cannot allocate memory
/usr/bin/cmake: error while loading shared libraries: liblzo2.so.2: failed to map segment from shared object: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
/usr/bin/cmake: error while loading shared libraries: libz.so.1: failed to map segment from shared object: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
make[2]: *** [kernel/CMakeFiles/kernel.dir/error_msgs.cpp.o] Error 1
make[2]: execvp: /bin/sh: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
make[2]: *** [kernel/CMakeFiles/kernel.dir/expr.cpp.o] Error 1
[ 52%] make[2]: execvp: /bin/sh: Cannot allocate memory
cd /root/lean/build/library && /usr/bin/c++    -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build    -o CMakeFiles/library.dir/normalize.cpp.o -c /root/lean/src/library/normalize.cpp
make[2]: execvp: /bin/sh: Cannot allocate memory
make[2]: *** [util/CMakeFiles/util.dir/name_set.cpp.o] Error 1
make[2]: *** [util/CMakeFiles/util.dir/script_state.cpp.o] Error 1
make[2]: *** [util/CMakeFiles/util.dir/luaref.cpp.o] Error 1
make[2]: *** [util/CMakeFiles/util.dir/lua_named_param.cpp.o] Error 1
make[2]: *** [util/CMakeFiles/util.dir/lbool.cpp.o] Error 1
make[2]: *** [util/CMakeFiles/util.dir/thread.cpp.o] Error 1
cd /root/lean/build/util && /usr/bin/c++    -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build    -o CMakeFiles/util.dir/list_fn.cpp.o -c /root/lean/src/util/list_fn.cpp
virtual memory exhausted: Cannot allocate memory
Building CXX object library/CMakeFiles/library.dir/shared_environment.cpp.o
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/util.cpp.o] Error 1
cd /root/lean/build/library/tactic && /usr/bin/c++    -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build    -o CMakeFiles/tactic.dir/constructor_tactic.cpp.o -c /root/lean/src/library/tactic/constructor_tactic.cpp
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
c++: internal compiler error: Killed (program cc1plus)
virtual memory exhausted: Cannot allocate memory
Please submit a full bug report,
with preprocessed source if appropriate.
See <file:///usr/share/doc/gcc-4.8/README.Bugs> for instructions.
make[2]: *** [library/simplifier/CMakeFiles/simplifier.dir/ceqv.cpp.o] Error 4
make[2]: *** Waiting for unfinished jobs....
make[2]: *** [util/sexpr/CMakeFiles/sexpr.dir/options.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
make[2]: *** [kernel/CMakeFiles/kernel.dir/level.cpp.o] Error 1
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/generalize_tactic.cpp.o] Error 1
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/let_tactic.cpp.o] Error 1
cd /root/lean/build/library/tactic && /usr/bin/c++    -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build    -o CMakeFiles/tactic.dir/injection_tactic.cpp.o -c /root/lean/src/library/tactic/injection_tactic.cpp
make[2]: execvp: /bin/sh: Cannot allocate memory
make[2]: *** [frontends/lean/CMakeFiles/lean_frontend.dir/builtin_cmds.cpp.o] Error 1
make[2]: *** [frontends/lean/CMakeFiles/lean_frontend.dir/server.cpp.o] Error 1
make[2]: *** [library/CMakeFiles/library.dir/expr_lt.cpp.o] Error 1
make[2]: *** Waiting for unfinished jobs....
make[2]: *** [library/CMakeFiles/library.dir/io_state.cpp.o] Error 1
make[2]: *** [library/CMakeFiles/library.dir/resolve_macro.cpp.o] Error 1
cd /root/lean/build/library && /usr/bin/c++    -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build    -o CMakeFiles/library.dir/shared_environment.cpp.o -c /root/lean/src/library/shared_environment.cpp
make[2]: *** [kernel/CMakeFiles/kernel.dir/normalizer_extension.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
make[2]: *** [kernel/quotient/CMakeFiles/quotient.dir/quotient.cpp.o] Error 1
make[2]: Leaving directory `/root/lean/build'
make[1]: *** [kernel/quotient/CMakeFiles/quotient.dir/all] Error 2
[ 53%] make[2]: *** [util/CMakeFiles/util.dir/name_map.cpp.o] Error 127
Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/util.cpp.o
cd /root/lean/build/library/tactic && /usr/bin/c++    -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build    -o CMakeFiles/tactic.dir/congruence_tactic.cpp.o -c /root/lean/src/library/tactic/congruence_tactic.cpp
virtual memory exhausted: Cannot allocate memory
make[2]: *** [library/error_handling/CMakeFiles/error_handling.dir/error_handling.cpp.o] Error 1
make[2]: Leaving directory `/root/lean/build'
make[1]: *** [library/error_handling/CMakeFiles/error_handling.dir/all] Error 2
make[2]: *** [frontends/lean/CMakeFiles/lean_frontend.dir/scanner.cpp.o] Error 1
cd /root/lean/build/frontends/lean && /usr/bin/c++    -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build    -o CMakeFiles/lean_frontend.dir/util.cpp.o -c /root/lean/src/frontends/lean/util.cpp
make[2]: *** [library/CMakeFiles/library.dir/module.cpp.o] Error 127
make[2]: *** [library/CMakeFiles/library.dir/max_sharing.cpp.o] Error 127
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/induction_tactic.cpp.o] Error 127
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/exfalso_tactic.cpp.o] Error 127
make[2]: *** [frontends/lean/CMakeFiles/lean_frontend.dir/parser_bindings.cpp.o] Error 127
make[2]: *** [frontends/lean/CMakeFiles/lean_frontend.dir/elaborator.cpp.o] Error 127
/usr/bin/cmake: error while loading shared libraries: liblzo2.so.2: failed to map segment from shared object: Cannot allocate memory
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/relation_tactics.cpp.o] Error 127
c++: internal compiler error: Killed (program cc1plus)
Please submit a full bug report,
with preprocessed source if appropriate.
See <file:///usr/share/doc/gcc-4.8/README.Bugs> for instructions.
make[2]: *** [frontends/lean/CMakeFiles/lean_frontend.dir/util.cpp.o] Error 4
virtual memory exhausted: Cannot allocate memory
make[2]: *** [library/CMakeFiles/library.dir/io_state_stream.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
make[2]: *** [kernel/CMakeFiles/kernel.dir/type_checker.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
make[2]: *** [util/CMakeFiles/util.dir/lean_path.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
make[2]: *** [util/CMakeFiles/util.dir/stackinfo.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/expr_to_tactic.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
/usr/bin/cmake: error while loading shared libraries: /usr/lib/x86_64-linux-gnu/libroken.so.18: cannot allocate version reference table: Cannot allocate memory
make[2]: *** [frontends/lean/CMakeFiles/lean_frontend.dir/inductive_cmd.cpp.o] Error 127
/usr/bin/cmake: error while loading shared libraries: /usr/lib/x86_64-linux-gnu/libroken.so.18: cannot allocate version reference table: Cannot allocate memory
make[2]: *** [frontends/lean/CMakeFiles/lean_frontend.dir/dependencies.cpp.o] Error 127
virtual memory exhausted: Cannot allocate memory
make[2]: *** [library/definitional/CMakeFiles/definitional.dir/brec_on.cpp.o] Error 1
make[2]: *** Waiting for unfinished jobs....
make[2]: *** [kernel/CMakeFiles/kernel.dir/converter.cpp.o] Error 1
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/tactic.cpp.o] Error 1
make[2]: *** [kernel/CMakeFiles/kernel.dir/environment.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
make[2]: *** [kernel/CMakeFiles/kernel.dir/expr_eq_fn.cpp.o] Error 1
make[2]: *** [util/interval/CMakeFiles/interval.dir/interval_instances.cpp.o] Error 1
make[2]: Leaving directory `/root/lean/build'
make[1]: *** [util/interval/CMakeFiles/interval.dir/all] Error 2
virtual memory exhausted: Cannot allocate memory
c++: internal compiler error: Killed (program cc1plus)
make[2]: *** [init/CMakeFiles/init.dir/init.cpp.o] Error 1
make[2]: Leaving directory `/root/lean/build'
make[1]: *** [init/CMakeFiles/init.dir/all] Error 2
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
Please submit a full bug report,
with preprocessed source if appropriate.
See <file:///usr/share/doc/gcc-4.8/README.Bugs> for instructions.
make[2]: *** [util/CMakeFiles/util.dir/trace.cpp.o] Error 1
make[2]: *** [kernel/inductive/CMakeFiles/inductive.dir/inductive.cpp.o] Error 4
make[2]: Leaving directory `/root/lean/build'
make[1]: *** [kernel/inductive/CMakeFiles/inductive.dir/all] Error 2
make[2]: *** [kernel/CMakeFiles/kernel.dir/instantiate.cpp.o] Error 1
make[2]: *** [library/CMakeFiles/library.dir/shared_environment.cpp.o] Error 1
make[2]: *** [util/CMakeFiles/util.dir/memory_pool.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
make[2]: *** [frontends/lean/CMakeFiles/lean_frontend.dir/parse_table.cpp.o] Error 1
make[2]: *** [frontends/lean/CMakeFiles/lean_frontend.dir/notation_cmd.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
make[2]: *** [util/CMakeFiles/util.dir/script_exception.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
make[2]: *** [util/CMakeFiles/util.dir/list_fn.cpp.o] Error 1
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/exact_tactic.cpp.o] Error 1
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/trace_tactic.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
make[2]: *** [kernel/CMakeFiles/kernel.dir/abstract.cpp.o] Error 1
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/congruence_tactic.cpp.o] Error 1
make[2]: *** [util/numerics/CMakeFiles/numerics.dir/primes.cpp.o] Error 1
make[2]: *** Waiting for unfinished jobs....
virtual memory exhausted: Cannot allocate memory
c++: internal compiler error: Killed (program cc1plus)
Please submit a full bug report,
with preprocessed source if appropriate.
See <file:///usr/share/doc/gcc-4.8/README.Bugs> for instructions.
make[2]: *** [util/sexpr/CMakeFiles/sexpr.dir/sexpr.cpp.o] Error 4
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
make[2]: *** [kernel/CMakeFiles/kernel.dir/equiv_manager.cpp.o] Error 1
make[2]: *** [library/CMakeFiles/library.dir/bin_app.cpp.o] Error 1
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/inversion_tactic.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
make[2]: *** [util/CMakeFiles/util.dir/safe_arith.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/contradiction_tactic.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
make[2]: *** [kernel/CMakeFiles/kernel.dir/declaration.cpp.o] Error 1
make[2]: *** [kernel/CMakeFiles/kernel.dir/for_each_fn.cpp.o] Error 1
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/proof_state.cpp.o] Error 1
make[2]: *** [library/definitional/CMakeFiles/definitional.dir/induction_on.cpp.o] Error 1
make[2]: *** [kernel/CMakeFiles/kernel.dir/formatter.cpp.o] Error 1
make[2]: *** [frontends/lean/CMakeFiles/lean_frontend.dir/calc.cpp.o] Error 1
make[2]: *** [util/CMakeFiles/util.dir/name.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
make[2]: *** [kernel/CMakeFiles/kernel.dir/free_vars.cpp.o] Error 1
as: error while loading shared libraries: libbfd-2.24-system.so: failed to map segment from shared object: Cannot allocate memory
make[2]: *** [util/CMakeFiles/util.dir/utf8.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
c++: internal compiler error: Killed (program cc1plus)
Please submit a full bug report,
with preprocessed source if appropriate.
See <file:///usr/share/doc/gcc-4.8/README.Bugs> for instructions.
make[2]: *** [library/definitional/CMakeFiles/definitional.dir/projection.cpp.o] Error 4
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
make[2]: *** [frontends/lean/CMakeFiles/lean_frontend.dir/parser.cpp.o] Error 1
make[2]: *** [library/CMakeFiles/library.dir/deep_copy.cpp.o] Error 1
make[2]: *** [util/CMakeFiles/util.dir/shared_mutex.cpp.o] Error 1
make[2]: *** [library/definitional/CMakeFiles/definitional.dir/no_confusion.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
make[2]: *** [kernel/CMakeFiles/kernel.dir/constraint.cpp.o] Error 1
make[2]: *** [library/CMakeFiles/library.dir/occurs.cpp.o] Error 1
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/intros_tactic.cpp.o] Error 1
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/rename_tactic.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
make[2]: *** [util/CMakeFiles/util.dir/realpath.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
make[2]: *** [frontends/lean/CMakeFiles/lean_frontend.dir/tokens.cpp.o] Error 1make[2]: *** [library/tactic/CMakeFiles/tactic.dir/apply_tactic.cpp.o] Error 1
make[2]: *** [shell/CMakeFiles/shell.dir/emscripten.cpp.o] Error 1
make[2]: *** [util/sexpr/CMakeFiles/sexpr.dir/format.cpp.o] Error 1make[2]: Leaving directory `/root/lean/build'

make[1]: *** [shell/CMakeFiles/shell.dir/all] Error 2
make[2]: *** [util/CMakeFiles/util.dir/exception.cpp.o] Error 1

make[2]: *** [util/numerics/CMakeFiles/numerics.dir/mpz.cpp.o] Error 1
make[2]: *** [library/simplifier/CMakeFiles/simplifier.dir/simp_rule_set.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
make[2]: *** [kernel/CMakeFiles/kernel.dir/init_module.cpp.o] Error 1
make[2]: *** [library/definitional/CMakeFiles/definitional.dir/rec_on.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
c++: internal compiler error: Killed (program cc1plus)
virtual memory exhausted: Cannot allocate memory
make[2]: *** [kernel/CMakeFiles/kernel.dir/justification.cpp.o] Error 1
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/elaborate.cpp.o] Error 1
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/init_module.cpp.o] Error 1
make[2]: *** [kernel/CMakeFiles/kernel.dir/expr_cache.cpp.o] Error 1
Please submit a full bug report,
with preprocessed source if appropriate.
See <file:///usr/share/doc/gcc-4.8/README.Bugs> for instructions.
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/check_expr_tactic.cpp.o] Error 1
make[2]: *** [library/definitional/CMakeFiles/definitional.dir/equations.cpp.o] Error 4
make[2]: *** [library/CMakeFiles/library.dir/constants.cpp.o] Error 1
make[2]: *** [kernel/hits/CMakeFiles/hits.dir/hits.cpp.o] Error 1
make[2]: Leaving directory `/root/lean/build'
make[1]: *** [kernel/hits/CMakeFiles/hits.dir/all] Error 2
make[2]: *** [util/numerics/CMakeFiles/numerics.dir/mpfp.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
make[2]: *** [frontends/lean/CMakeFiles/lean_frontend.dir/token_table.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
make[2]: *** [kernel/CMakeFiles/kernel.dir/kernel_exception.cpp.o] Error 1
make[2]: *** [util/CMakeFiles/util.dir/rb_map.cpp.o] Error 1
make[2]: *** [util/CMakeFiles/util.dir/bitap_fuzzy_search.cpp.o] Error 1
make[2]: *** [kernel/CMakeFiles/kernel.dir/extension_context.cpp.o] Error 1
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/clear_tactic.cpp.o] Error 1
make[2]: *** [util/CMakeFiles/util.dir/lua.cpp.o] Error 1
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/goal.cpp.o] Error 1
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/assert_tactic.cpp.o] Error 1
make[2]: *** [kernel/CMakeFiles/kernel.dir/metavar.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
make[2]: *** [library/tactic/CMakeFiles/tactic.dir/injection_tactic.cpp.o] Error 1
make[2]: *** [frontends/lean/CMakeFiles/lean_frontend.dir/decl_cmds.cpp.o] Error 1
make[2]: *** [util/CMakeFiles/util.dir/serializer.cpp.o] Error 1
make[2]: *** [frontends/lean/CMakeFiles/lean_frontend.dir/parser_config.cpp.o] Error 1
make[2]: *** [util/numerics/CMakeFiles/numerics.dir/init_module.cpp.o] Error 1
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
virtual memory exhausted: Cannot allocate memory
make[2]: *** [util/numerics/CMakeFiles/numerics.dir/float.cpp.o] Error 1
make[2]: *** [library/CMakeFiles/library.dir/kernel_bindings.cpp.o] Error 1
make[2]: *** [library/definitional/CMakeFiles/definitional.dir/init_module.cpp.o] Error 1
make[2]: *** [util/numerics/CMakeFiles/numerics.dir/double.cpp.o] Error 1
make[2]: *** [library/definitional/CMakeFiles/definitional.dir/cases_on.cpp.o] Error 1
make[2]: Leaving directory `/root/lean/build'
make[1]: *** [library/definitional/CMakeFiles/definitional.dir/all] Error 2
make[2]: Leaving directory `/root/lean/build'
make[1]: *** [util/CMakeFiles/util.dir/all] Error 2
make[2]: Leaving directory `/root/lean/build'
make[1]: *** [util/sexpr/CMakeFiles/sexpr.dir/all] Error 2
make[2]: Leaving directory `/root/lean/build'
make[1]: *** [util/numerics/CMakeFiles/numerics.dir/all] Error 2
make[2]: Leaving directory `/root/lean/build'
make[1]: *** [kernel/CMakeFiles/kernel.dir/all] Error 2
make[2]: Leaving directory `/root/lean/build'
make[1]: *** [frontends/lean/CMakeFiles/lean_frontend.dir/all] Error 2
make[2]: Leaving directory `/root/lean/build'
make[1]: *** [library/simplifier/CMakeFiles/simplifier.dir/all] Error 2
make[2]: Leaving directory `/root/lean/build'
make[1]: *** [library/CMakeFiles/library.dir/all] Error 2
make[2]: Leaving directory `/root/lean/build'
make[1]: *** [library/tactic/CMakeFiles/tactic.dir/all] Error 2
make[1]: Leaving directory `/root/lean/build'
make: *** [all] Error 2