search

leanprover / lean3

Lean Theorem Prover
http://leanprover.github.io/
Apache License 2.0
2.15k stars 216 forks source link

Build error #1058

Closed abooij closed 8 years ago

abooij commented 8 years ago 
$ ninja -v
[1/93] : && /usr/bin/c++   -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_AUTO_THREAD_FINALIZATION -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -D HAS_TCMALLOC -O3 -DNDEBUG  -pthread util/CMakeFiles/util.dir/debug.cpp.o util/CMakeFiles/util.dir/name.cpp.o util/CMakeFiles/util.dir/name_set.cpp.o util/CMakeFiles/util.dir/fresh_name.cpp.o util/CMakeFiles/util.dir/exception.cpp.o util/CMakeFiles/util.dir/interrupt.cpp.o util/CMakeFiles/util.dir/hash.cpp.o util/CMakeFiles/util.dir/escaped.cpp.o util/CMakeFiles/util.dir/bit_tricks.cpp.o util/CMakeFiles/util.dir/safe_arith.cpp.o util/CMakeFiles/util.dir/ascii.cpp.o util/CMakeFiles/util.dir/memory.cpp.o util/CMakeFiles/util.dir/shared_mutex.cpp.o util/CMakeFiles/util.dir/realpath.cpp.o util/CMakeFiles/util.dir/stackinfo.cpp.o util/CMakeFiles/util.dir/lean_path.cpp.o util/CMakeFiles/util.dir/serializer.cpp.o util/CMakeFiles/util.dir/lbool.cpp.o util/CMakeFiles/util.dir/bitap_fuzzy_search.cpp.o util/CMakeFiles/util.dir/init_module.cpp.o util/CMakeFiles/util.dir/thread.cpp.o util/CMakeFiles/util.dir/memory_pool.cpp.o util/CMakeFiles/util.dir/utf8.cpp.o util/CMakeFiles/util.dir/name_map.cpp.o util/CMakeFiles/util.dir/list_fn.cpp.o util/CMakeFiles/util.dir/null_ostream.cpp.o util/CMakeFiles/util.dir/file_lock.cpp.o tests/util/CMakeFiles/scoped_set.dir/scoped_set.cpp.o  -o tests/util/scoped_set  -rdynamic -lmpfr -lgmp -ltcmalloc && :
[2/93] : && /usr/bin/c++   -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_AUTO_THREAD_FINALIZATION -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -D HAS_TCMALLOC -O3 -DNDEBUG  -pthread util/CMakeFiles/util.dir/debug.cpp.o util/CMakeFiles/util.dir/name.cpp.o util/CMakeFiles/util.dir/name_set.cpp.o util/CMakeFiles/util.dir/fresh_name.cpp.o util/CMakeFiles/util.dir/exception.cpp.o util/CMakeFiles/util.dir/interrupt.cpp.o util/CMakeFiles/util.dir/hash.cpp.o util/CMakeFiles/util.dir/escaped.cpp.o util/CMakeFiles/util.dir/bit_tricks.cpp.o util/CMakeFiles/util.dir/safe_arith.cpp.o util/CMakeFiles/util.dir/ascii.cpp.o util/CMakeFiles/util.dir/memory.cpp.o util/CMakeFiles/util.dir/shared_mutex.cpp.o util/CMakeFiles/util.dir/realpath.cpp.o util/CMakeFiles/util.dir/stackinfo.cpp.o util/CMakeFiles/util.dir/lean_path.cpp.o util/CMakeFiles/util.dir/serializer.cpp.o util/CMakeFiles/util.dir/lbool.cpp.o util/CMakeFiles/util.dir/bitap_fuzzy_search.cpp.o util/CMakeFiles/util.dir/init_module.cpp.o util/CMakeFiles/util.dir/thread.cpp.o util/CMakeFiles/util.dir/memory_pool.cpp.o util/CMakeFiles/util.dir/utf8.cpp.o util/CMakeFiles/util.dir/name_map.cpp.o util/CMakeFiles/util.dir/list_fn.cpp.o util/CMakeFiles/util.dir/null_ostream.cpp.o util/CMakeFiles/util.dir/file_lock.cpp.o tests/util/CMakeFiles/stackinfo.dir/stackinfo.cpp.o  -o tests/util/stackinfo  -rdynamic -lmpfr -lgmp -ltcmalloc && :
[3/93] cd /tmp/lean/hott && /usr/bin/python /tmp/lean/src/../bin/linja all tags
FAILED: CMakeFiles/hott_lib 
cd /tmp/lean/hott && /usr/bin/python /tmp/lean/src/../bin/linja all tags
[1/158] "/tmp/lean/bin/lean"  /tmp/lean/hott/algebra/category/constructions/discrete.hlean -o "/tmp/lean/hott/algebra/category/constructions/discrete.olean" -c "/tmp/lean/hott/algebra/category/constructions/discrete.clean" -i "/tmp/lean/hott/algebra/category/constructions/discrete.ilean" 
FAILED: /tmp/lean/hott/algebra/category/constructions/discrete.olean /tmp/lean/hott/algebra/category/constructions/discrete.ilean /tmp/lean/hott/algebra/category/constructions/discrete.clean 
"/tmp/lean/bin/lean"  /tmp/lean/hott/algebra/category/constructions/discrete.hlean -o "/tmp/lean/hott/algebra/category/constructions/discrete.olean" -c "/tmp/lean/hott/algebra/category/constructions/discrete.clean" -i "/tmp/lean/hott/algebra/category/constructions/discrete.ilean" 
[2/158] "/tmp/lean/bin/lean"  /tmp/lean/hott/algebra/category/limits/functor_preserve.hlean -o "/tmp/lean/hott/algebra/category/limits/functor_preserve.olean" -c "/tmp/lean/hott/algebra/category/limits/functor_preserve.clean" -i "/tmp/lean/hott/algebra/category/limits/functor_preserve.ilean" 
FAILED: /tmp/lean/hott/algebra/category/limits/functor_preserve.olean /tmp/lean/hott/algebra/category/limits/functor_preserve.ilean /tmp/lean/hott/algebra/category/limits/functor_preserve.clean 
"/tmp/lean/bin/lean"  /tmp/lean/hott/algebra/category/limits/functor_preserve.hlean -o "/tmp/lean/hott/algebra/category/limits/functor_preserve.olean" -c "/tmp/lean/hott/algebra/category/limits/functor_preserve.clean" -i "/tmp/lean/hott/algebra/category/limits/functor_preserve.ilean" 
[3/158] "/tmp/lean/bin/lean"  /tmp/lean/hott/cubical/default.hlean -o "/tmp/lean/hott/cubical/default.olean" -c "/tmp/lean/hott/cubical/default.clean" -i "/tmp/lean/hott/cubical/default.ilean" 
FAILED: /tmp/lean/hott/cubical/default.olean /tmp/lean/hott/cubical/default.ilean /tmp/lean/hott/cubical/default.clean 
"/tmp/lean/bin/lean"  /tmp/lean/hott/cubical/default.hlean -o "/tmp/lean/hott/cubical/default.olean" -c "/tmp/lean/hott/cubical/default.clean" -i "/tmp/lean/hott/cubical/default.ilean" 
[4/158] "/tmp/lean/bin/lean"  /tmp/lean/hott/cubical/square.hlean -o "/tmp/lean/hott/cubical/square.olean" -c "/tmp/lean/hott/cubical/square.clean" -i "/tmp/lean/hott/cubical/square.ilean" 
FAILED: /tmp/lean/hott/cubical/square.olean /tmp/lean/hott/cubical/square.ilean /tmp/lean/hott/cubical/square.clean 
"/tmp/lean/bin/lean"  /tmp/lean/hott/cubical/square.hlean -o "/tmp/lean/hott/cubical/square.olean" -c "/tmp/lean/hott/cubical/square.clean" -i "/tmp/lean/hott/cubical/square.ilean" 
[5/158] "/tmp/lean/bin/lean"  /tmp/lean/hott/algebra/category/constructions/initial.hlean -o "/tmp/lean/hott/algebra/category/constructions/initial.olean" -c "/tmp/lean/hott/algebra/category/constructions/initial.clean" -i "/tmp/lean/hott/algebra/category/constructions/initial.ilean"
FAILED: /tmp/lean/hott/algebra/category/constructions/initial.olean /tmp/lean/hott/algebra/category/constructions/initial.ilean /tmp/lean/hott/algebra/category/constructions/initial.clean 
"/tmp/lean/bin/lean"  /tmp/lean/hott/algebra/category/constructions/initial.hlean -o "/tmp/lean/hott/algebra/category/constructions/initial.olean" -c "/tmp/lean/hott/algebra/category/constructions/initial.clean" -i "/tmp/lean/hott/algebra/category/constructions/initial.ilean" 
[6/158] "/tmp/lean/bin/lean"  /tmp/lean/hott/algebra/category/functor/adjoint.hlean -o "/tmp/lean/hott/algebra/category/functor/adjoint.olean" -c "/tmp/lean/hott/algebra/category/functor/adjoint.clean" -i "/tmp/lean/hott/algebra/category/functor/adjoint.ilean" 
FAILED: /tmp/lean/hott/algebra/category/functor/adjoint.olean /tmp/lean/hott/algebra/category/functor/adjoint.ilean /tmp/lean/hott/algebra/category/functor/adjoint.clean 
"/tmp/lean/bin/lean"  /tmp/lean/hott/algebra/category/functor/adjoint.hlean -o "/tmp/lean/hott/algebra/category/functor/adjoint.olean" -c "/tmp/lean/hott/algebra/category/functor/adjoint.clean" -i "/tmp/lean/hott/algebra/category/functor/adjoint.ilean" 
ninja: build stopped: subcommand failed.
[4/93] cd /tmp/lean/library && /usr/bin/python /tmp/lean/src/../bin/linja all tags
FAILED: CMakeFiles/standard_lib 
cd /tmp/lean/library && /usr/bin/python /tmp/lean/src/../bin/linja all tags
[1/194] "/tmp/lean/bin/lean"  /tmp/lean/library/data/nat/sub.lean -o "/tmp/lean/library/data/nat/sub.olean" -c "/tmp/lean/library/data/nat/sub.clean" -i "/tmp/lean/library/data/nat/sub.ilean" 
FAILED: /tmp/lean/library/data/nat/sub.olean /tmp/lean/library/data/nat/sub.ilean /tmp/lean/library/data/nat/sub.clean 
"/tmp/lean/bin/lean"  /tmp/lean/library/data/nat/sub.lean -o "/tmp/lean/library/data/nat/sub.olean" -c "/tmp/lean/library/data/nat/sub.clean" -i "/tmp/lean/library/data/nat/sub.ilean" 
[2/194] "/tmp/lean/bin/lean"  /tmp/lean/library/logic/examples/double_negation_translation.lean -o "/tmp/lean/library/logic/examples/double_negation_translation.olean" -c "/tmp/lean/library/logic/examples/double_negation_translation.clean" -i "/tmp/lean/library/logic/examples/double_negation_translation.ilean" 
FAILED: /tmp/lean/library/logic/examples/double_negation_translation.olean /tmp/lean/library/logic/examples/double_negation_translation.ilean /tmp/lean/library/logic/examples/double_negation_translation.clean 
"/tmp/lean/bin/lean"  /tmp/lean/library/logic/examples/double_negation_translation.lean -o "/tmp/lean/library/logic/examples/double_negation_translation.olean" -c "/tmp/lean/library/logic/examples/double_negation_translation.clean" -i "/tmp/lean/library/logic/examples/double_negation_translation.ilean" 
[3/194] "/tmp/lean/bin/lean"  /tmp/lean/library/init/setoid.lean -o "/tmp/lean/library/init/setoid.olean" -c "/tmp/lean/library/init/setoid.clean" -i "/tmp/lean/library/init/setoid.ilean" 
FAILED: /tmp/lean/library/init/setoid.olean /tmp/lean/library/init/setoid.ilean /tmp/lean/library/init/setoid.clean 
"/tmp/lean/bin/lean"  /tmp/lean/library/init/setoid.lean -o "/tmp/lean/library/init/setoid.olean" -c "/tmp/lean/library/init/setoid.clean" -i "/tmp/lean/library/init/setoid.ilean" 
[4/194] "/tmp/lean/bin/lean"  /tmp/lean/library/data/nat/power.lean -o "/tmp/lean/library/data/nat/power.olean" -c "/tmp/lean/library/data/nat/power.clean" -i "/tmp/lean/library/data/nat/power.ilean" 
FAILED: /tmp/lean/library/data/nat/power.olean /tmp/lean/library/data/nat/power.ilean /tmp/lean/library/data/nat/power.clean 
"/tmp/lean/bin/lean"  /tmp/lean/library/data/nat/power.lean -o "/tmp/lean/library/data/nat/power.olean" -c "/tmp/lean/library/data/nat/power.clean" -i "/tmp/lean/library/data/nat/power.ilean" 
[5/194] "/tmp/lean/bin/lean"  /tmp/lean/library/logic/weak_fan.lean -o "/tmp/lean/library/logic/weak_fan.olean" -c "/tmp/lean/library/logic/weak_fan.clean" -i "/tmp/lean/library/logic/weak_fan.ilean" 
FAILED: /tmp/lean/library/logic/weak_fan.olean /tmp/lean/library/logic/weak_fan.ilean /tmp/lean/library/logic/weak_fan.clean 
"/tmp/lean/bin/lean"  /tmp/lean/library/logic/weak_fan.lean -o "/tmp/lean/library/logic/weak_fan.olean" -c "/tmp/lean/library/logic/weak_fan.clean" -i "/tmp/lean/library/logic/weak_fan.ilean" 
[6/194] "/tmp/lean/bin/lean"  /tmp/lean/library/data/set/card.lean -o "/tmp/lean/library/data/set/card.olean" -c "/tmp/lean/library/data/set/card.clean" -i "/tmp/lean/library/data/set/card.ilean" 
FAILED: /tmp/lean/library/data/set/card.olean /tmp/lean/library/data/set/card.ilean /tmp/lean/library/data/set/card.clean 
"/tmp/lean/bin/lean"  /tmp/lean/library/data/set/card.lean -o "/tmp/lean/library/data/set/card.olean" -c "/tmp/lean/library/data/set/card.clean" -i "/tmp/lean/library/data/set/card.ilean" 
ninja: build stopped: subcommand failed.
[5/93] /usr/bin/c++    -Isrc -I. -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_AUTO_THREAD_FINALIZATION -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -D HAS_TCMALLOC -O3 -DNDEBUG -MMD -MT tests/util/CMakeFiles/exception.dir/exception.cpp.o -MF tests/util/CMakeFiles/exception.dir/exception.cpp.o.d -o tests/util/CMakeFiles/exception.dir/exception.cpp.o -c src/tests/util/exception.cpp
[6/93] /usr/bin/c++    -Isrc -I. -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_AUTO_THREAD_FINALIZATION -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -D HAS_TCMALLOC -O3 -DNDEBUG -MMD -MT tests/util/CMakeFiles/splay_map.dir/splay_map.cpp.o -MF tests/util/CMakeFiles/splay_map.dir/splay_map.cpp.o.d -o tests/util/CMakeFiles/splay_map.dir/splay_map.cpp.o -c src/tests/util/splay_map.cpp
[7/93] /usr/bin/c++    -Isrc -I. -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_AUTO_THREAD_FINALIZATION -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -D HAS_TCMALLOC -O3 -DNDEBUG -MMD -MT tests/util/CMakeFiles/splay_tree.dir/splay_tree.cpp.o -MF tests/util/CMakeFiles/splay_tree.dir/splay_tree.cpp.o.d -o tests/util/CMakeFiles/splay_tree.dir/splay_tree.cpp.o -c src/tests/util/splay_tree.cpp
[8/93] /usr/bin/c++    -Isrc -I. -Wall -Wextra -std=c++11  -D LEAN_MULTI_THREAD -D LEAN_AUTO_THREAD_FINALIZATION -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -D HAS_TCMALLOC -O3 -DNDEBUG -MMD -MT tests/util/CMakeFiles/lazy_list.dir/lazy_list.cpp.o -MF tests/util/CMakeFiles/lazy_list.dir/lazy_list.cpp.o.d -o tests/util/CMakeFiles/lazy_list.dir/lazy_list.cpp.o -c src/tests/util/lazy_list.cpp
ninja: build stopped: subcommand failed.
abooij commented 8 years ago

I get similar errors when using the Makefile-based AUR build script

soonhokong commented 8 years ago
Kha commented 8 years ago

With an up-to-date Arch Linux system, this is likely to be #1044. If @soonhokong's lean command gives a segmentation fault, you could try again with https://github.com/Kha/lean/tree/sized-delete.

abooij commented 8 years ago

@soonhokong: Thanks for your quick help. Respectively:

Yes, this is Arch. However this is a rolling release style distribution (and this particular install is up to date).

$ c++ --version
c++ (GCC) 6.1.1 20160501
Copyright (C) 2016 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
$ /tmp/lean/bin/lean /tmp/lean/hott/algebra/category/constructions/discrete.hlean
[1]    1806 segmentation fault (core dumped)  /tmp/lean/bin/lean

@Kha: Thanks for the suggestion. I ran the same command as in that bug just now:

$ /tmp/lean/bin/lean library/standard.lean
[1]    1833 segmentation fault (core dumped)  /tmp/lean/bin/lean library/standard.lean

Not sure if that's a confirmation or not...

Kha commented 8 years ago

Yes, the commit on the linked branch should fix that (and break all older compilers, which is why it's not a pull request yet).

abooij commented 8 years ago

@Kha: negative; my segfaults persists with your commit.

edit: to be safe, I the entire "/tmp/lean" directory and cloned github.com:Kha/lean.git , built it again, and ran the commands i listed above - same output.

edit2: oops, didn't get the right branch. BRB!

abooij commented 8 years ago

Okay, now that I checked out the right branch:

$ /tmp/lean/bin/lean library/standard.lean
library/standard.lean:9:0: error: invalid import, unknown module 'init'
library/standard.lean:9:7: error: invalid import, unknown module 'logic'
library/standard.lean:9:13: error: invalid import, unknown module 'data'
$ /tmp/lean/bin/lean /tmp/lean/hott/algebra/category/constructions/discrete.hlean
/tmp/lean/hott/algebra/category/constructions/discrete.hlean:10:0: error: invalid import, unknown module 'init'
/tmp/lean/hott/algebra/category/constructions/discrete.hlean:10:9: error: invalid import, unknown module 'groupoid'
/tmp/lean/hott/algebra/category/constructions/discrete.hlean:10:18: error: invalid import, unknown module 'types.bool'
/tmp/lean/hott/algebra/category/constructions/discrete.hlean:10:31: error: invalid import, unknown module 'nat_trans'
/tmp/lean/hott/algebra/category/constructions/discrete.hlean:12:5: error: invalid namespace name 'eq'
/tmp/lean/hott/algebra/category/constructions/discrete.hlean:16:65: error: unknown identifier 'is_trunc'
/tmp/lean/hott/algebra/category/constructions/discrete.hlean: error: /tmp/lean/hott/algebra/category/constructions/discrete.hlean:18:26: error: unexpected token
$ ninja
[5/106] cd /tmp/lean/library && /usr/bin/python /tmp/lean/src/../bin/linja all tags
FAILED: CMakeFiles/standard_lib 
cd /tmp/lean/library && /usr/bin/python /tmp/lean/src/../bin/linja all tags
[1/194] "/tmp/lean/bin/lean"  /tmp/lean/library/logic/examples/leftinv_of_inj.lean -o "/tmp/lean/library/logic/examples/leftinv_of_inj.olean" -c "/tmp/lean/library/logic/examples/leftinv_of_inj.clean" -i "/tmp/lean/library/logic/examples/leftinv_of_inj.ilean" 
FAILED: /tmp/lean/library/logic/examples/leftinv_of_inj.olean /tmp/lean/library/logic/examples/leftinv_of_inj.ilean /tmp/lean/library/logic/examples/leftinv_of_inj.clean 
"/tmp/lean/bin/lean"  /tmp/lean/library/logic/examples/leftinv_of_inj.lean -o "/tmp/lean/library/logic/examples/leftinv_of_inj.olean" -c "/tmp/lean/library/logic/examples/leftinv_of_inj.clean" -i "/tmp/lean/library/logic/examples/leftinv_of_inj.ilean" 
/tmp/lean/library/logic/examples/leftinv_of_inj.lean:12:0: error: invalid import, unknown module 'init'
/tmp/lean/library/logic/examples/leftinv_of_inj.lean:12:5: error: invalid namespace name 'function'
/tmp/lean/library/logic/examples/leftinv_of_inj.lean:14:55: error: unknown identifier 'nonempty'
/tmp/lean/library/logic/examples/leftinv_of_inj.lean: error: /tmp/lean/library/logic/examples/leftinv_of_inj.lean:15:18: error: unexpected token
[2/194] "/tmp/lean/bin/lean"  /tmp/lean/library/data/examples/depchoice.lean -o "/tmp/lean/library/data/examples/depchoice.olean" -c "/tmp/lean/library/data/examples/depchoice.clean" -i "/tmp/lean/library/data/examples/depchoice.ilean" 
FAILED: /tmp/lean/library/data/examples/depchoice.olean /tmp/lean/library/data/examples/depchoice.ilean /tmp/lean/library/data/examples/depchoice.clean 
"/tmp/lean/bin/lean"  /tmp/lean/library/data/examples/depchoice.lean -o "/tmp/lean/library/data/examples/depchoice.olean" -c "/tmp/lean/library/data/examples/depchoice.clean" -i "/tmp/lean/library/data/examples/depchoice.ilean" 
/tmp/lean/library/data/examples/depchoice.lean:6:0: error: invalid import, unknown module 'init'
/tmp/lean/library/data/examples/depchoice.lean:6:7: error: invalid import, unknown module 'data.encodable'
/tmp/lean/library/data/examples/depchoice.lean:7:5: error: invalid namespace name 'nat'
/tmp/lean/library/data/examples/depchoice.lean:14:52: error: unknown identifier 'Prop'
/tmp/lean/library/data/examples/depchoice.lean: error: /tmp/lean/library/data/examples/depchoice.lean:15:10: error: unexpected token
[3/194] "/tmp/lean/bin/lean"  /tmp/lean/library/data/finset/comb.lean -o "/tmp/lean/library/data/finset/comb.olean" -c "/tmp/lean/library/data/finset/comb.clean" -i "/tmp/lean/library/data/finset/comb.ilean" 
FAILED: /tmp/lean/library/data/finset/comb.olean /tmp/lean/library/data/finset/comb.ilean /tmp/lean/library/data/finset/comb.clean 
"/tmp/lean/bin/lean"  /tmp/lean/library/data/finset/comb.lean -o "/tmp/lean/library/data/finset/comb.olean" -c "/tmp/lean/library/data/finset/comb.clean" -i "/tmp/lean/library/data/finset/comb.ilean" 
/tmp/lean/library/data/finset/comb.lean:8:0: error: invalid import, unknown module 'init'
/tmp/lean/library/data/finset/comb.lean:8:7: error: invalid import, unknown module 'data.finset.basic'
/tmp/lean/library/data/finset/comb.lean:8:25: error: invalid import, unknown module 'logic.identities'
/tmp/lean/library/data/finset/comb.lean:9:5: error: invalid namespace name 'list'
/tmp/lean/library/data/finset/comb.lean:16:14: error: unknown identifier 'decidable_eq'
/tmp/lean/library/data/finset/comb.lean:17:8: error: invalid include/omit command, 'h' is not a parameter/variable
/tmp/lean/library/data/finset/comb.lean:19:34: error: unknown identifier 'finset'
/tmp/lean/library/data/finset/comb.lean:24:16: error: unknown identifier 'finset.prio'
/tmp/lean/library/data/finset/comb.lean: error: /tmp/lean/library/data/finset/comb.lean:24:30: error: unexpected token
[4/194] "/tmp/lean/bin/lean"  /tmp/lean/library/data/hlist.lean -o "/tmp/lean/library/data/hlist.olean" -c "/tmp/lean/library/data/hlist.clean" -i "/tmp/lean/library/data/hlist.ilean" 
FAILED: /tmp/lean/library/data/hlist.olean /tmp/lean/library/data/hlist.ilean /tmp/lean/library/data/hlist.clean 
"/tmp/lean/bin/lean"  /tmp/lean/library/data/hlist.lean -o "/tmp/lean/library/data/hlist.olean" -c "/tmp/lean/library/data/hlist.clean" -i "/tmp/lean/library/data/hlist.ilean" 
/tmp/lean/library/data/hlist.lean:8:0: error: invalid import, unknown module 'init'
/tmp/lean/library/data/hlist.lean:8:7: error: invalid import, unknown module 'data.list'
/tmp/lean/library/data/hlist.lean:8:17: error: invalid import, unknown module 'logic.cast'
/tmp/lean/library/data/hlist.lean:9:5: error: invalid namespace name 'list'
/tmp/lean/library/data/hlist.lean:12:19: error: invalid expression
/tmp/lean/library/data/hlist.lean:18:27: error: unknown identifier 'hlist'
/tmp/lean/library/data/hlist.lean:21:41: error: unknown identifier 'hlist'
/tmp/lean/library/data/hlist.lean: error: /tmp/lean/library/data/hlist.lean:21:69: error: unexpected token
[5/194] "/tmp/lean/bin/lean"  /tmp/lean/library/theories/finite_group_theory/hom.lean -o "/tmp/lean/library/theories/finite_group_theory/hom.olean" -c "/tmp/lean/library/theories/finite_group_theory/hom.clean" -i "/tmp/lean/library/theories/finite_group_theory/hom.ilean" 
FAILED: /tmp/lean/library/theories/finite_group_theory/hom.olean /tmp/lean/library/theories/finite_group_theory/hom.ilean /tmp/lean/library/theories/finite_group_theory/hom.clean 
"/tmp/lean/bin/lean"  /tmp/lean/library/theories/finite_group_theory/hom.lean -o "/tmp/lean/library/theories/finite_group_theory/hom.olean" -c "/tmp/lean/library/theories/finite_group_theory/hom.clean" -i "/tmp/lean/library/theories/finite_group_theory/hom.ilean" 
/tmp/lean/library/theories/finite_group_theory/hom.lean:7:0: error: invalid import, unknown module 'init'
/tmp/lean/library/theories/finite_group_theory/hom.lean:7:7: error: invalid import, unknown module 'algebra.group'
/tmp/lean/library/theories/finite_group_theory/hom.lean:7:21: error: invalid import, unknown module 'data.set'
/tmp/lean/library/theories/finite_group_theory/hom.lean:7:31: error: invalid import, unknown module 'subgroup'
/tmp/lean/library/theories/finite_group_theory/hom.lean:13:20: error: unknown identifier 'eq.subst'
/tmp/lean/library/theories/finite_group_theory/hom.lean:14:5: error: invalid namespace name 'set'
/tmp/lean/library/theories/finite_group_theory/hom.lean:15:5: error: invalid namespace name 'function'
/tmp/lean/library/theories/finite_group_theory/hom.lean:16:5: error: invalid namespace name 'group_theory.ops'
/tmp/lean/library/theories/finite_group_theory/hom.lean:17:5: error: invalid namespace name 'quot'
/tmp/lean/library/theories/finite_group_theory/hom.lean:18:16: error: unknown identifier 'set'
/tmp/lean/library/theories/finite_group_theory/hom.lean:18:20: error: unknown command 'section'
/tmp/lean/library/theories/finite_group_theory/hom.lean:23:15: error: unknown identifier 'group'
/tmp/lean/library/theories/finite_group_theory/hom.lean:24:15: error: unknown identifier 'group'
/tmp/lean/library/theories/finite_group_theory/hom.lean:25:8: error: invalid include/omit command, 's1' is not a parameter/variable
/tmp/lean/library/theories/finite_group_theory/hom.lean:26:8: error: invalid include/omit command, 's2' is not a parameter/variable
/tmp/lean/library/theories/finite_group_theory/hom.lean:29:49: error: unknown identifier 'Prop'
/tmp/lean/library/theories/finite_group_theory/hom.lean: error: /tmp/lean/library/theories/finite_group_theory/hom.lean:29:68: error: unexpected token
[6/194] "/tmp/lean/bin/lean"  /tmp/lean/library/theories/measure_theory/extended_real.lean -o "/tmp/lean/library/theories/measure_theory/extended_real.olean" -c "/tmp/lean/library/theories/measure_theory/extended_real.clean" -i "/tmp/lean/library/theories/measure_theory/extended_real.ilean" 
FAILED: /tmp/lean/library/theories/measure_theory/extended_real.olean /tmp/lean/library/theories/measure_theory/extended_real.ilean /tmp/lean/library/theories/measure_theory/extended_real.clean 
"/tmp/lean/bin/lean"  /tmp/lean/library/theories/measure_theory/extended_real.lean -o "/tmp/lean/library/theories/measure_theory/extended_real.olean" -c "/tmp/lean/library/theories/measure_theory/extended_real.clean" -i "/tmp/lean/library/theories/measure_theory/extended_real.ilean" 
/tmp/lean/library/theories/measure_theory/extended_real.lean:8:0: error: invalid import, unknown module 'init'
/tmp/lean/library/theories/measure_theory/extended_real.lean:8:7: error: invalid import, unknown module 'data.real'
/tmp/lean/library/theories/measure_theory/extended_real.lean:9:5: error: invalid namespace name 'real'
/tmp/lean/library/theories/measure_theory/extended_real.lean:13:33: error: unknown identifier 'zero_mul'
/tmp/lean/library/theories/measure_theory/extended_real.lean:14:33: error: unknown identifier 'mul_zero'
/tmp/lean/library/theories/measure_theory/extended_real.lean:15:33: error: unknown identifier 'neg_neg'
/tmp/lean/library/theories/measure_theory/extended_real.lean:19:0: error: unknown declaration 'ℝ'
/tmp/lean/library/theories/measure_theory/extended_real.lean:24:10: error: unknown identifier 'ereal.of_real'
/tmp/lean/library/theories/measure_theory/extended_real.lean:24:24: error: unknown command 'notation'
/tmp/lean/library/theories/measure_theory/extended_real.lean:25:16: error: unknown identifier 'ereal.infty'
/tmp/lean/library/theories/measure_theory/extended_real.lean:26:17: error: unknown identifier 'ereal.neginfty'
/tmp/lean/library/theories/measure_theory/extended_real.lean:30:29: error: unknown identifier 'num.pred'
/tmp/lean/library/theories/measure_theory/extended_real.lean:34:47: error: unknown identifier 'ereal.prio'
/tmp/lean/library/theories/measure_theory/extended_real.lean:37:46: error: unknown identifier 'ereal.prio'
/tmp/lean/library/theories/measure_theory/extended_real.lean:40:27: error: unknown identifier 'ereal'
/tmp/lean/library/theories/measure_theory/extended_real.lean: error: /tmp/lean/library/theories/measure_theory/extended_real.lean:42:2: error: unexpected token
ninja: build stopped: subcommand failed.
[6/106] cd /tmp/lean/hott && /usr/bin/python /tmp/lean/src/../bin/linja all tags
FAILED: CMakeFiles/hott_lib 
cd /tmp/lean/hott && /usr/bin/python /tmp/lean/src/../bin/linja all tags
[1/158] "/tmp/lean/bin/lean"  /tmp/lean/hott/init/funext.hlean -o "/tmp/lean/hott/init/funext.olean" -c "/tmp/lean/hott/init/funext.clean" -i "/tmp/lean/hott/init/funext.ilean" 
FAILED: /tmp/lean/hott/init/funext.olean /tmp/lean/hott/init/funext.ilean /tmp/lean/hott/init/funext.clean 
"/tmp/lean/bin/lean"  /tmp/lean/hott/init/funext.hlean -o "/tmp/lean/hott/init/funext.olean" -c "/tmp/lean/hott/init/funext.clean" -i "/tmp/lean/hott/init/funext.ilean" 
/tmp/lean/hott/init/funext.hlean:10:8: error: invalid import, unknown module 'trunc'
/tmp/lean/hott/init/funext.hlean:10:15: error: invalid import, unknown module 'equiv'
/tmp/lean/hott/init/funext.hlean:10:22: error: invalid import, unknown module 'ua'
/tmp/lean/hott/init/funext.hlean:11:5: error: invalid namespace name 'eq'
/tmp/lean/hott/init/funext.hlean:22:56: error: unknown identifier 'is_equiv'
/tmp/lean/hott/init/funext.hlean:26:50: error: unexpected token
/tmp/lean/hott/init/funext.hlean: error: /tmp/lean/hott/init/funext.hlean:26:59: error: unexpected token
[2/158] "/tmp/lean/bin/lean"  /tmp/lean/hott/algebra/category/strict.hlean -o "/tmp/lean/hott/algebra/category/strict.olean" -c "/tmp/lean/hott/algebra/category/strict.clean" -i "/tmp/lean/hott/algebra/category/strict.ilean" 
FAILED: /tmp/lean/hott/algebra/category/strict.olean /tmp/lean/hott/algebra/category/strict.ilean /tmp/lean/hott/algebra/category/strict.clean 
"/tmp/lean/bin/lean"  /tmp/lean/hott/algebra/category/strict.hlean -o "/tmp/lean/hott/algebra/category/strict.olean" -c "/tmp/lean/hott/algebra/category/strict.clean" -i "/tmp/lean/hott/algebra/category/strict.ilean" 
/tmp/lean/hott/algebra/category/strict.hlean:7:0: error: invalid import, unknown module 'init'
/tmp/lean/hott/algebra/category/strict.hlean:7:8: error: invalid import, unknown module 'functor.basic'
/tmp/lean/hott/algebra/category/strict.hlean:9:5: error: invalid namespace name 'is_trunc'
/tmp/lean/hott/algebra/category/strict.hlean:12:59: error: unknown identifier 'precategory'
/tmp/lean/hott/algebra/category/strict.hlean:15:12: error: unknown identifier 'strict_precategory.is_set_ob'
/tmp/lean/hott/algebra/category/strict.hlean:15:41: error: unknown command 'definition'
/tmp/lean/hott/algebra/category/strict.hlean:17:64: error: unknown identifier 'precategory'
/tmp/lean/hott/algebra/category/strict.hlean:23:14: error: unknown identifier 'strict_precategory'
/tmp/lean/hott/algebra/category/strict.hlean:25:12: error: unknown identifier 'Strict_precategory.struct'
/tmp/lean/hott/algebra/category/strict.hlean:25:38: error: unknown command '[coercion]'
/tmp/lean/hott/algebra/category/strict.hlean:25:49: error: unknown command 'definition'
/tmp/lean/hott/algebra/category/strict.hlean:28:9: error: unknown identifier 'Strict_precategory'
/tmp/lean/hott/algebra/category/strict.hlean:31:7: error: invalid namespace name 'functor'
/tmp/lean/hott/algebra/category/strict.hlean:34:60: error: unknown identifier 'precategory'
/tmp/lean/hott/algebra/category/strict.hlean: error: /tmp/lean/hott/algebra/category/strict.hlean:35:27: error: unexpected token
[3/158] "/tmp/lean/bin/lean"  /tmp/lean/hott/function.hlean -o "/tmp/lean/hott/function.olean" -c "/tmp/lean/hott/function.clean" -i "/tmp/lean/hott/function.ilean" 
FAILED: /tmp/lean/hott/function.olean /tmp/lean/hott/function.ilean /tmp/lean/hott/function.clean 
"/tmp/lean/bin/lean"  /tmp/lean/hott/function.hlean -o "/tmp/lean/hott/function.olean" -c "/tmp/lean/hott/function.clean" -i "/tmp/lean/hott/function.ilean" 
/tmp/lean/hott/function.hlean:10:0: error: invalid import, unknown module 'init'
/tmp/lean/hott/function.hlean:10:7: error: invalid import, unknown module 'hit.trunc'
/tmp/lean/hott/function.hlean:10:17: error: invalid import, unknown module 'types.equiv'
/tmp/lean/hott/function.hlean:10:29: error: invalid import, unknown module 'cubical.square'
/tmp/lean/hott/function.hlean:12:5: error: invalid namespace name 'equiv'
/tmp/lean/hott/function.hlean:17:62: error: unexpected token
/tmp/lean/hott/function.hlean: error: /tmp/lean/hott/function.hlean:17:74: error: unexpected token
[4/158] "/tmp/lean/bin/lean"  /tmp/lean/hott/init/pathover.hlean -o "/tmp/lean/hott/init/pathover.olean" -c "/tmp/lean/hott/init/pathover.clean" -i "/tmp/lean/hott/init/pathover.ilean" 
FAILED: /tmp/lean/hott/init/pathover.olean /tmp/lean/hott/init/pathover.ilean /tmp/lean/hott/init/pathover.clean 
"/tmp/lean/bin/lean"  /tmp/lean/hott/init/pathover.hlean -o "/tmp/lean/hott/init/pathover.olean" -c "/tmp/lean/hott/init/pathover.clean" -i "/tmp/lean/hott/init/pathover.ilean" 
/tmp/lean/hott/init/pathover.hlean:10:8: error: invalid import, unknown module 'path'
/tmp/lean/hott/init/pathover.hlean:10:14: error: invalid import, unknown module 'equiv'
/tmp/lean/hott/init/pathover.hlean:12:5: error: invalid namespace name 'equiv'
/tmp/lean/hott/init/pathover.hlean:15:37: error: unexpected token
/tmp/lean/hott/init/pathover.hlean: error: /tmp/lean/hott/init/pathover.hlean:15:52: error: unexpected token
[5/158] "/tmp/lean/bin/lean"  /tmp/lean/hott/homotopy/cellcomplex.hlean -o "/tmp/lean/hott/homotopy/cellcomplex.olean" -c "/tmp/lean/hott/homotopy/cellcomplex.clean" -i "/tmp/lean/hott/homotopy/cellcomplex.ilean" 
FAILED: /tmp/lean/hott/homotopy/cellcomplex.olean /tmp/lean/hott/homotopy/cellcomplex.ilean /tmp/lean/hott/homotopy/cellcomplex.clean 
"/tmp/lean/bin/lean"  /tmp/lean/hott/homotopy/cellcomplex.hlean -o "/tmp/lean/hott/homotopy/cellcomplex.olean" -c "/tmp/lean/hott/homotopy/cellcomplex.clean" -i "/tmp/lean/hott/homotopy/cellcomplex.ilean" 
/tmp/lean/hott/homotopy/cellcomplex.hlean:6:0: error: invalid import, unknown module 'init'
/tmp/lean/hott/homotopy/cellcomplex.hlean:6:7: error: invalid import, unknown module 'types.trunc'
/tmp/lean/hott/homotopy/cellcomplex.hlean:6:19: error: invalid import, unknown module 'homotopy.sphere'
/tmp/lean/hott/homotopy/cellcomplex.hlean:6:35: error: invalid import, unknown module 'hit.pushout'
/tmp/lean/hott/homotopy/cellcomplex.hlean:8:5: error: invalid namespace name 'eq'
/tmp/lean/hott/homotopy/cellcomplex.hlean:11:28: error: unexpected token
/tmp/lean/hott/homotopy/cellcomplex.hlean:16:24: error: unknown identifier 'ℕ'
/tmp/lean/hott/homotopy/cellcomplex.hlean:37:39: error: unknown identifier 'ℕ'
/tmp/lean/hott/homotopy/cellcomplex.hlean: error: /tmp/lean/hott/homotopy/cellcomplex.hlean:46:7: error: unexpected token
[6/158] "/tmp/lean/bin/lean"  /tmp/lean/hott/algebra/category/default.hlean -o "/tmp/lean/hott/algebra/category/default.olean" -c "/tmp/lean/hott/algebra/category/default.clean" -i "/tmp/lean/hott/algebra/category/default.ilean" 
FAILED: /tmp/lean/hott/algebra/category/default.olean /tmp/lean/hott/algebra/category/default.ilean /tmp/lean/hott/algebra/category/default.clean 
"/tmp/lean/bin/lean"  /tmp/lean/hott/algebra/category/default.hlean -o "/tmp/lean/hott/algebra/category/default.olean" -c "/tmp/lean/hott/algebra/category/default.clean" -i "/tmp/lean/hott/algebra/category/default.ilean" 
/tmp/lean/hott/algebra/category/default.hlean:7:0: error: invalid import, unknown module 'init'
/tmp/lean/hott/algebra/category/default.hlean:7:8: error: invalid import, unknown module 'category'
/tmp/lean/hott/algebra/category/default.hlean:7:18: error: invalid import, unknown module 'strict'
/tmp/lean/hott/algebra/category/default.hlean:7:26: error: invalid import, unknown module 'groupoid'
/tmp/lean/hott/algebra/category/default.hlean:7:36: error: invalid import, unknown module 'constructions'
ninja: build stopped: subcommand failed.
[10/106] Building CXX object tests/util/CMakeFiles/rb_tree.dir/rb_tree.cpp.o
ninja: build stopped: subcommand failed.
soonhokong commented 8 years ago

@abooij, could you try ninja clean and ninja and check you still get the same error?

soonhokong commented 8 years ago

@abooij, just to make sure please do cd /tmp/lean/library && git clean -fxd and cd /tmp/lean/hott && git clean -fxd before you do ninja.

soonhokong commented 8 years ago

For now, another way to avoid the problem is to pass -DTCMALLOC=OFF. @Kha, can you confirm that we can only reproduce the problem with tcmalloc?

Kha commented 8 years ago

@soonhokong Ah, that's probably the simplest solution. Can confirm that passing the flag and thus selection jemalloc fixes the problem.

abooij commented 8 years ago

@soonhokong: "ninja clean" was not sufficient (which is what i did before). but doing a big git clean did help. so yes, that means @Kha's patch does work.

soonhokong commented 8 years ago

@mgrabovsky, could you update https://aur.archlinux.org/cgit/aur.git/?h=lean-git to pass -DTCMALLOC=OFF to cmake?

soonhokong commented 8 years ago

So, it turns out that this is a duplicate of #1044. I'm closing it.