Created
August 25, 2016 16:06
-
-
Save spl/417fb18d876200a87199033707f52211 to your computer and use it in GitHub Desktop.
Errors compiling lean on Mac
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
$ mkdir -p build/debug | |
$ cd build/debug/ | |
$ cmake -DCMAKE_BUILD_TYPE=DEBUG -G Ninja ../../src | |
-- The CXX compiler identification is AppleClang 7.3.0.7030031 | |
-- The C compiler identification is AppleClang 7.3.0.7030031 | |
-- Check for working CXX compiler: /Library/Developer/CommandLineTools/usr/bin/c++ | |
-- Check for working CXX compiler: /Library/Developer/CommandLineTools/usr/bin/c++ -- works | |
-- Detecting CXX compiler ABI info | |
-- Detecting CXX compiler ABI info - done | |
-- Detecting CXX compile features | |
-- Detecting CXX compile features - done | |
-- Check for working C compiler: /Library/Developer/CommandLineTools/usr/bin/cc | |
-- Check for working C compiler: /Library/Developer/CommandLineTools/usr/bin/cc -- works | |
-- Detecting C compiler ABI info | |
-- Detecting C compiler ABI info - done | |
-- Detecting C compile features | |
-- Detecting C compile features - done | |
-- Emacs dependecies directory ~/projects/lean/src/emacs/dependencies | |
-- Lean emacs-mode will be installed at /usr/local/share/emacs/site-lisp/lean | |
-- Lean library will be installed at /usr/local/lib/lean | |
-- Looking for C++ include unistd.h | |
-- Looking for C++ include unistd.h - found | |
-- Found MPFR: /usr/local/include (Required is at least version "3.1.0") | |
-- Found GMP: /usr/local/include (Required is at least version "5.0.5") | |
-- Could NOT find TCMALLOC (missing: TCMALLOC_INCLUDE_DIR TCMALLOC_LIBRARIES) | |
*** WARNING: failed to find tcmalloc | |
*** The (optional) tcmalloc library is available at: https://code.google.com/p/gperftools | |
-- Failed to find tcmalloc, using standard malloc. | |
-- Found malloc_size | |
-- Found PythonInterp: /usr/bin/python (found version "2.7.10") | |
-- git commit sha1: cc70845332e63a1f1be21dc1f96d17269fc85909 | |
-- Checking flags for C++11 | |
-- Checking flags for C++11 - Found: -std=c++11 | |
-- Checking flags for C++14 | |
-- Checking flags for C++14 - Found: -std=c++14 | |
-- Checking flags for C++17 | |
-- Checking flags for C++17 - Found: -std=c++1z | |
-- Checking for feature sized_deallocation | |
-- Checking for feature sized_deallocation - Failed | |
-- Emacs dependencies directory does not exist. Therefore, they will not be included in the binary installation package. The Emacs packages required by Lean Emacs mode can be retrieved from the repository https://github.com/leanprover/emacs-dependencies. The cmake option EMACS_DEPENDENCIES can be used to specify where these files are located. | |
-- Configuring done | |
-- Generating done | |
-- Build files have been written to: ~/projects/lean/build/debug | |
$ ninja | |
[480/481] cd ~/projects/lean/library && /usr/bin/python ~/projects/lean/src/../bin/linja all tags | |
FAILED: CMakeFiles/standard_lib | |
cd ~/projects/lean/library && /usr/bin/python ~/projects/lean/src/../bin/linja all tags | |
[193/195] generating dep... ~/projects/lean/library/theories/group_theory/quotient.d | |
[1/196] "~/projects/lean/bin/lean" ~/projects/lean/library/data/examples/notencodable.lean -o "~/projects/lean/library/data/examples/notencodable.olean" -c "~/projects/lean/library/data/examples/notencodable.clean" -i "~/projects/lean/library/data/examples/notencodable.ilean" | |
FAILED: ~/projects/lean/library/data/examples/notencodable.olean ~/projects/lean/library/data/examples/notencodable.ilean ~/projects/lean/library/data/examples/notencodable.clean | |
"~/projects/lean/bin/lean" ~/projects/lean/library/data/examples/notencodable.lean -o "~/projects/lean/library/data/examples/notencodable.olean" -c "~/projects/lean/library/data/examples/notencodable.clean" -i "~/projects/lean/library/data/examples/notencodable.ilean" | |
~/projects/lean/library/data/examples/notencodable.lean:8:0: error: invalid import, unknown module 'init' | |
~/projects/lean/library/data/examples/notencodable.lean:8:7: error: invalid import, unknown module 'data.encodable' | |
~/projects/lean/library/data/examples/notencodable.lean:9:5: error: invalid namespace name 'nat' | |
~/projects/lean/library/data/examples/notencodable.lean:12:31: error: unknown identifier 'encodable' | |
~/projects/lean/library/data/examples/notencodable.lean:14:35: error: unknown identifier 'nat' | |
~/projects/lean/library/data/examples/notencodable.lean:17:35: error: unknown identifier 'nat' | |
~/projects/lean/library/data/examples/notencodable.lean:20:34: error: unknown identifier 'nat' | |
~/projects/lean/library/data/examples/notencodable.lean: error: ~/projects/lean/library/data/examples/notencodable.lean:20:71: error: unexpected token | |
[2/196] "~/projects/lean/bin/lean" ~/projects/lean/library/data/bool.lean -o "~/projects/lean/library/data/bool.olean" -c "~/projects/lean/library/data/bool.clean" -i "~/projects/lean/library/data/bool.ilean" | |
FAILED: ~/projects/lean/library/data/bool.olean ~/projects/lean/library/data/bool.ilean ~/projects/lean/library/data/bool.clean | |
"~/projects/lean/bin/lean" ~/projects/lean/library/data/bool.lean -o "~/projects/lean/library/data/bool.olean" -c "~/projects/lean/library/data/bool.clean" -i "~/projects/lean/library/data/bool.ilean" | |
~/projects/lean/library/data/bool.lean:6:0: error: invalid import, unknown module 'init' | |
~/projects/lean/library/data/bool.lean:6:7: error: invalid import, unknown module 'logic.eq' | |
~/projects/lean/library/data/bool.lean:9:18: error: unknown identifier 'bor' | |
~/projects/lean/library/data/bool.lean:9:22: error: unknown command 'local' | |
~/projects/lean/library/data/bool.lean:10:18: error: unknown identifier 'band' | |
~/projects/lean/library/data/bool.lean:10:23: error: unknown command 'theorem' | |
~/projects/lean/library/data/bool.lean:12:25: error: unknown identifier 'bool' | |
~/projects/lean/library/data/bool.lean: error: ~/projects/lean/library/data/bool.lean:12:35: error: unexpected token | |
[3/196] "~/projects/lean/bin/lean" ~/projects/lean/library/data/examples/depchoice.lean -o "~/projects/lean/library/data/examples/depchoice.olean" -c "~/projects/lean/library/data/examples/depchoice.clean" -i "~/projects/lean/library/data/examples/depchoice.ilean" | |
FAILED: ~/projects/lean/library/data/examples/depchoice.olean ~/projects/lean/library/data/examples/depchoice.ilean ~/projects/lean/library/data/examples/depchoice.clean | |
"~/projects/lean/bin/lean" ~/projects/lean/library/data/examples/depchoice.lean -o "~/projects/lean/library/data/examples/depchoice.olean" -c "~/projects/lean/library/data/examples/depchoice.clean" -i "~/projects/lean/library/data/examples/depchoice.ilean" | |
~/projects/lean/library/data/examples/depchoice.lean:6:0: error: invalid import, unknown module 'init' | |
~/projects/lean/library/data/examples/depchoice.lean:6:7: error: invalid import, unknown module 'data.encodable' | |
~/projects/lean/library/data/examples/depchoice.lean:7:5: error: invalid namespace name 'nat' | |
~/projects/lean/library/data/examples/depchoice.lean:14:52: error: unknown identifier 'Prop' | |
~/projects/lean/library/data/examples/depchoice.lean: error: ~/projects/lean/library/data/examples/depchoice.lean:15:10: error: unexpected token | |
[4/196] "~/projects/lean/bin/lean" ~/projects/lean/library/logic/examples/leftinv_of_inj.lean -o "~/projects/lean/library/logic/examples/leftinv_of_inj.olean" -c "~/projects/lean/library/logic/examples/leftinv_of_inj.clean" -i "~/projects/lean/library/logic/examples/leftinv_of_inj.ilean" | |
FAILED: ~/projects/lean/library/logic/examples/leftinv_of_inj.olean ~/projects/lean/library/logic/examples/leftinv_of_inj.ilean ~/projects/lean/library/logic/examples/leftinv_of_inj.clean | |
"~/projects/lean/bin/lean" ~/projects/lean/library/logic/examples/leftinv_of_inj.lean -o "~/projects/lean/library/logic/examples/leftinv_of_inj.olean" -c "~/projects/lean/library/logic/examples/leftinv_of_inj.clean" -i "~/projects/lean/library/logic/examples/leftinv_of_inj.ilean" | |
~/projects/lean/library/logic/examples/leftinv_of_inj.lean:12:0: error: invalid import, unknown module 'init' | |
~/projects/lean/library/logic/examples/leftinv_of_inj.lean:12:5: error: invalid namespace name 'function' | |
~/projects/lean/library/logic/examples/leftinv_of_inj.lean:14:55: error: unknown identifier 'nonempty' | |
~/projects/lean/library/logic/examples/leftinv_of_inj.lean: error: ~/projects/lean/library/logic/examples/leftinv_of_inj.lean:15:18: error: unexpected token | |
[5/196] "~/projects/lean/bin/lean" ~/projects/lean/library/data/uprod.lean -o "~/projects/lean/library/data/uprod.olean" -c "~/projects/lean/library/data/uprod.clean" -i "~/projects/lean/library/data/uprod.ilean" | |
FAILED: ~/projects/lean/library/data/uprod.olean ~/projects/lean/library/data/uprod.ilean ~/projects/lean/library/data/uprod.clean | |
"~/projects/lean/bin/lean" ~/projects/lean/library/data/uprod.lean -o "~/projects/lean/library/data/uprod.olean" -c "~/projects/lean/library/data/uprod.clean" -i "~/projects/lean/library/data/uprod.ilean" | |
~/projects/lean/library/data/uprod.lean:8:0: error: invalid import, unknown module 'init' | |
~/projects/lean/library/data/uprod.lean:8:7: error: invalid import, unknown module 'data.prod' | |
~/projects/lean/library/data/uprod.lean:8:17: error: invalid import, unknown module 'logic.identities' | |
~/projects/lean/library/data/uprod.lean:9:5: error: invalid namespace name 'prod' | |
~/projects/lean/library/data/uprod.lean:11:45: error: unexpected token | |
~/projects/lean/library/data/uprod.lean: error: ~/projects/lean/library/data/uprod.lean:12:3: error: unexpected token | |
[6/196] "~/projects/lean/bin/lean" ~/projects/lean/library/data/rat/countable.lean -o "~/projects/lean/library/data/rat/countable.olean" -c "~/projects/lean/library/data/rat/countable.clean" -i "~/projects/lean/library/data/rat/countable.ilean" | |
FAILED: ~/projects/lean/library/data/rat/countable.olean ~/projects/lean/library/data/rat/countable.ilean ~/projects/lean/library/data/rat/countable.clean | |
"~/projects/lean/bin/lean" ~/projects/lean/library/data/rat/countable.lean -o "~/projects/lean/library/data/rat/countable.olean" -c "~/projects/lean/library/data/rat/countable.clean" -i "~/projects/lean/library/data/rat/countable.ilean" | |
~/projects/lean/library/data/rat/countable.lean:6:0: error: invalid import, unknown module 'init' | |
~/projects/lean/library/data/rat/countable.lean:6:7: error: invalid import, unknown module 'data.rat.basic' | |
~/projects/lean/library/data/rat/countable.lean:6:22: error: invalid import, unknown module 'data.countable' | |
~/projects/lean/library/data/rat/countable.lean:6:37: error: invalid import, unknown module 'data.encodable' | |
~/projects/lean/library/data/rat/countable.lean:6:52: error: invalid import, unknown module 'data.int.countable' | |
~/projects/lean/library/data/rat/countable.lean:7:5: error: invalid namespace name 'encodable' | |
~/projects/lean/library/data/rat/countable.lean:10:27: error: unknown identifier 'prerat' | |
~/projects/lean/library/data/rat/countable.lean:13:30: error: unknown identifier 'nat' | |
~/projects/lean/library/data/rat/countable.lean: error: ~/projects/lean/library/data/rat/countable.lean:19:25: error: unexpected token | |
[7/196] "~/projects/lean/bin/lean" ~/projects/lean/library/data/bv.lean -o "~/projects/lean/library/data/bv.olean" -c "~/projects/lean/library/data/bv.clean" -i "~/projects/lean/library/data/bv.ilean" | |
FAILED: ~/projects/lean/library/data/bv.olean ~/projects/lean/library/data/bv.ilean ~/projects/lean/library/data/bv.clean | |
"~/projects/lean/bin/lean" ~/projects/lean/library/data/bv.lean -o "~/projects/lean/library/data/bv.olean" -c "~/projects/lean/library/data/bv.clean" -i "~/projects/lean/library/data/bv.ilean" | |
~/projects/lean/library/data/bv.lean:10:0: error: invalid import, unknown module 'init' | |
~/projects/lean/library/data/bv.lean:10:7: error: invalid import, unknown module 'data.list' | |
~/projects/lean/library/data/bv.lean:11:7: error: invalid import, unknown module 'data.tuple' | |
~/projects/lean/library/data/bv.lean:14:5: error: invalid namespace name 'bool' | |
~/projects/lean/library/data/bv.lean:15:5: error: invalid namespace name 'eq.ops' | |
~/projects/lean/library/data/bv.lean:16:5: error: invalid namespace name 'list' | |
~/projects/lean/library/data/bv.lean:17:5: error: invalid namespace name 'nat' | |
~/projects/lean/library/data/bv.lean:18:5: error: invalid namespace name 'prod' | |
~/projects/lean/library/data/bv.lean:19:5: error: invalid namespace name 'subtype' | |
~/projects/lean/library/data/bv.lean:20:5: error: invalid namespace name 'tuple' | |
~/projects/lean/library/data/bv.lean:22:31: error: unknown identifier 'ℕ' | |
~/projects/lean/library/data/bv.lean:25:24: error: unknown identifier 'ℕ' | |
~/projects/lean/library/data/bv.lean:28:28: error: unknown identifier 'ℕ' | |
~/projects/lean/library/data/bv.lean:32:26: error: unknown identifier 'ℕ' | |
~/projects/lean/library/data/bv.lean: error: ~/projects/lean/library/data/bv.lean:32:34: error: unexpected token | |
[8/196] "~/projects/lean/bin/lean" ~/projects/lean/library/data/list/sorted.lean -o "~/projects/lean/library/data/list/sorted.olean" -c "~/projects/lean/library/data/list/sorted.clean" -i "~/projects/lean/library/data/list/sorted.ilean" | |
FAILED: ~/projects/lean/library/data/list/sorted.olean ~/projects/lean/library/data/list/sorted.ilean ~/projects/lean/library/data/list/sorted.clean | |
"~/projects/lean/bin/lean" ~/projects/lean/library/data/list/sorted.lean -o "~/projects/lean/library/data/list/sorted.olean" -c "~/projects/lean/library/data/list/sorted.clean" -i "~/projects/lean/library/data/list/sorted.ilean" | |
~/projects/lean/library/data/list/sorted.lean:6:0: error: invalid import, unknown module 'init' | |
~/projects/lean/library/data/list/sorted.lean:6:7: error: invalid import, unknown module 'data.list.comb' | |
~/projects/lean/library/data/list/sorted.lean:6:22: error: invalid import, unknown module 'data.list.perm' | |
~/projects/lean/library/data/list/sorted.lean:10:22: error: unknown identifier 'Prop' | |
~/projects/lean/library/data/list/sorted.lean:13:25: error: invalid expression | |
~/projects/lean/library/data/list/sorted.lean:18:18: error: invalid expression | |
~/projects/lean/library/data/list/sorted.lean:22:16: error: invalid expression | |
~/projects/lean/library/data/list/sorted.lean:25:9: error: invalid variable binder type update, 'R' is not a variable | |
~/projects/lean/library/data/list/sorted.lean:27:30: error: unknown identifier 'hd_rel' | |
~/projects/lean/library/data/list/sorted.lean:28:42: error: invalid end of scope, begin/end mistmatch, scope starts with 'list', and ends with '[anonymous]' | |
~/projects/lean/library/data/list/sorted.lean:30:28: error: unknown identifier 'sorted' | |
~/projects/lean/library/data/list/sorted.lean: error: ~/projects/lean/library/data/list/sorted.lean:30:59: error: unexpected token | |
[9/196] "~/projects/lean/bin/lean" ~/projects/lean/library/data/int/basic.lean -o "~/projects/lean/library/data/int/basic.olean" -c "~/projects/lean/library/data/int/basic.clean" -i "~/projects/lean/library/data/int/basic.ilean" | |
FAILED: ~/projects/lean/library/data/int/basic.olean ~/projects/lean/library/data/int/basic.ilean ~/projects/lean/library/data/int/basic.clean | |
"~/projects/lean/bin/lean" ~/projects/lean/library/data/int/basic.lean -o "~/projects/lean/library/data/int/basic.olean" -c "~/projects/lean/library/data/int/basic.clean" -i "~/projects/lean/library/data/int/basic.ilean" | |
~/projects/lean/library/data/int/basic.lean:28:0: error: invalid import, unknown module 'init' | |
~/projects/lean/library/data/int/basic.lean:28:7: error: invalid import, unknown module 'data.nat.sub' | |
~/projects/lean/library/data/int/basic.lean:28:20: error: invalid import, unknown module 'algebra.relation' | |
~/projects/lean/library/data/int/basic.lean:28:37: error: invalid import, unknown module 'data.prod' | |
~/projects/lean/library/data/int/basic.lean:29:5: error: invalid namespace name 'eq.ops' | |
~/projects/lean/library/data/int/basic.lean:30:5: error: invalid namespace name 'prod' | |
~/projects/lean/library/data/int/basic.lean:31:5: error: invalid namespace name 'decidable' | |
~/projects/lean/library/data/int/basic.lean:35:0: error: unknown declaration 'nat' | |
~/projects/lean/library/data/int/basic.lean:39:16: error: unknown identifier 'int' | |
~/projects/lean/library/data/int/basic.lean:40:64: error: unknown identifier 'num' | |
~/projects/lean/library/data/int/basic.lean:45:10: error: unknown identifier 'int.of_nat' | |
~/projects/lean/library/data/int/basic.lean:45:21: error: unknown command 'notation' | |
~/projects/lean/library/data/int/basic.lean:47:26: error: unknown identifier 'int.neg_succ_of_nat' | |
~/projects/lean/library/data/int/basic.lean:49:28: error: unknown identifier 'num' | |
~/projects/lean/library/data/int/basic.lean:51:45: error: unknown identifier 'int.prio' | |
~/projects/lean/library/data/int/basic.lean:54:44: error: unknown identifier 'int.prio' | |
~/projects/lean/library/data/int/basic.lean:57:22: error: unknown identifier 'of_nat' | |
~/projects/lean/library/data/int/basic.lean: error: ~/projects/lean/library/data/int/basic.lean:57:37: error: unexpected token | |
[10/196] "~/projects/lean/bin/lean" ~/projects/lean/library/init/reserved_notation.lean -o "~/projects/lean/library/init/reserved_notation.olean" -c "~/projects/lean/library/init/reserved_notation.clean" -i "~/projects/lean/library/init/reserved_notation.ilean" | |
FAILED: ~/projects/lean/library/init/reserved_notation.olean ~/projects/lean/library/init/reserved_notation.ilean ~/projects/lean/library/init/reserved_notation.clean | |
"~/projects/lean/bin/lean" ~/projects/lean/library/init/reserved_notation.lean -o "~/projects/lean/library/init/reserved_notation.olean" -c "~/projects/lean/library/init/reserved_notation.clean" -i "~/projects/lean/library/init/reserved_notation.ilean" | |
~/projects/lean/library/init/reserved_notation.lean:7:7: error: invalid import, unknown module 'init.datatypes' | |
~/projects/lean/library/init/reserved_notation.lean:20:56: error: unknown identifier 'Prop' | |
~/projects/lean/library/init/reserved_notation.lean:22:55: error: unknown identifier 'Prop' | |
~/projects/lean/library/init/reserved_notation.lean:23:55: error: unknown identifier 'Prop' | |
~/projects/lean/library/init/reserved_notation.lean:31:32: error: unknown identifier 'has_dvd' | |
~/projects/lean/library/init/reserved_notation.lean:35:32: error: unknown identifier 'has_le' | |
~/projects/lean/library/init/reserved_notation.lean:36:32: error: unknown identifier 'has_lt' | |
~/projects/lean/library/init/reserved_notation.lean:38:42: error: unknown identifier 'has_le' | |
~/projects/lean/library/init/reserved_notation.lean:39:42: error: unknown identifier 'has_lt' | |
~/projects/lean/library/init/reserved_notation.lean:43:46: error: unknown identifier 'num' | |
~/projects/lean/library/init/reserved_notation.lean:46:44: error: unknown identifier 'num' | |
~/projects/lean/library/init/reserved_notation.lean:49:48: error: unknown identifier 'pos_num' | |
~/projects/lean/library/init/reserved_notation.lean:53:7: error: invalid namespace name 'bool' | |
~/projects/lean/library/init/reserved_notation.lean:54:25: error: unknown identifier 'pos_num' | |
~/projects/lean/library/init/reserved_notation.lean:57:23: error: unknown identifier 'pos_num' | |
~/projects/lean/library/init/reserved_notation.lean:60:23: error: unknown identifier 'pos_num' | |
~/projects/lean/library/init/reserved_notation.lean:63:24: error: unknown identifier 'pos_num' | |
~/projects/lean/library/init/reserved_notation.lean:77:48: error: unknown identifier 'pos_num' | |
~/projects/lean/library/init/reserved_notation.lean:83:24: error: unknown identifier 'num' | |
~/projects/lean/library/init/reserved_notation.lean:87:44: error: unknown identifier 'num' | |
~/projects/lean/library/init/reserved_notation.lean:90:34: error: unknown identifier 'num' | |
~/projects/lean/library/init/reserved_notation.lean:91:34: error: unknown identifier 'num' | |
~/projects/lean/library/init/reserved_notation.lean:94:31: error: unknown identifier 'num.add' | |
~/projects/lean/library/init/reserved_notation.lean:96:34: error: unknown identifier 'nat' | |
~/projects/lean/library/init/reserved_notation.lean:99:25: error: unknown identifier 'num' | |
~/projects/lean/library/init/reserved_notation.lean:104:10: error: unknown identifier 'pos_num_has_add' | |
~/projects/lean/library/init/reserved_notation.lean:105:10: error: unknown command '[priority' | |
~/projects/lean/library/init/reserved_notation.lean:105:21: error: unknown command '[priority' | |
~/projects/lean/library/init/reserved_notation.lean:107:45: error: unknown identifier 'nat.prio' | |
~/projects/lean/library/init/reserved_notation.lean:110:44: error: unknown identifier 'nat.prio' | |
~/projects/lean/library/init/reserved_notation.lean:113:44: error: unknown identifier 'nat.prio' | |
~/projects/lean/library/init/reserved_notation.lean:124:28: error: unknown identifier 'num' | |
~/projects/lean/library/init/reserved_notation.lean:125:28: error: unknown identifier 'num' | |
~/projects/lean/library/init/reserved_notation.lean:133:0: error: unknown identifier 'num.succ' | |
~/projects/lean/library/init/reserved_notation.lean:153:21: error: unknown identifier 'std.prec.max_plus' | |
~/projects/lean/library/init/reserved_notation.lean:207:14: error: unknown identifier 'dvd' | |
~/projects/lean/library/init/reserved_notation.lean:210:8: error: unexpected token | |
~/projects/lean/library/init/reserved_notation.lean:210:14: error: invalid notation declaration, ':=' expected | |
~/projects/lean/library/init/reserved_notation.lean:211:14: error: unknown identifier 'le' | |
~/projects/lean/library/init/reserved_notation.lean:212:14: error: unknown identifier 'ge' | |
~/projects/lean/library/init/reserved_notation.lean:213:14: error: unknown identifier 'lt' | |
~/projects/lean/library/init/reserved_notation.lean:214:14: error: unknown identifier 'gt' | |
~/projects/lean/library/init/reserved_notation.lean:220:55: error: unknown identifier 'dvd' | |
~/projects/lean/library/init/reserved_notation.lean:222:55: error: unknown identifier 'le' | |
~/projects/lean/library/init/reserved_notation.lean:223:55: error: unknown identifier 'ge' | |
~/projects/lean/library/init/reserved_notation.lean:224:55: error: unknown identifier 'lt' | |
~/projects/lean/library/init/reserved_notation.lean:225:55: error: unknown identifier 'gt' | |
ninja: build stopped: subcommand failed. | |
[481/481] cd ~/projects/lean/hott && /usr/bin/python ~/projects/lean/src/../bin/linja all tags | |
[166/166] generating dep... ~/projects/lean/hott/types/eq.d upoid.d | |
[1/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/datatypes.hlean -o "~/projects/lean/hott/init/datatypes.olean" -c "~/projects/lean/hott/init/datatypes.clean" -i "~/projects/lean/hott/init/datatypes.ilean" | |
[2/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/reserved_notation.hlean -o "~/projects/lean/hott/init/reserved_notation.olean" -c "~/projects/lean/hott/init/reserved_notation.clean" -i "~/projects/lean/hott/init/reserved_notation.ilean" | |
[3/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/bool.hlean -o "~/projects/lean/hott/init/bool.olean" -c "~/projects/lean/hott/init/bool.clean" -i "~/projects/lean/hott/init/bool.ilean" | |
[4/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/num.hlean -o "~/projects/lean/hott/init/num.olean" -c "~/projects/lean/hott/init/num.clean" -i "~/projects/lean/hott/init/num.ilean" | |
[5/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/tactic.hlean -o "~/projects/lean/hott/init/tactic.olean" -c "~/projects/lean/hott/init/tactic.clean" -i "~/projects/lean/hott/init/tactic.ilean" | |
[6/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/logic.hlean -o "~/projects/lean/hott/init/logic.olean" -c "~/projects/lean/hott/init/logic.clean" -i "~/projects/lean/hott/init/logic.ilean" | |
[7/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/relation.hlean -o "~/projects/lean/hott/init/relation.olean" -c "~/projects/lean/hott/init/relation.clean" -i "~/projects/lean/hott/init/relation.ilean" | |
[8/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/types.hlean -o "~/projects/lean/hott/init/types.olean" -c "~/projects/lean/hott/init/types.clean" -i "~/projects/lean/hott/init/types.ilean" | |
[9/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/function.hlean -o "~/projects/lean/hott/init/function.olean" -c "~/projects/lean/hott/init/function.clean" -i "~/projects/lean/hott/init/function.ilean" | |
[10/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/connectives.hlean -o "~/projects/lean/hott/init/connectives.olean" -c "~/projects/lean/hott/init/connectives.clean" -i "~/projects/lean/hott/init/connectives.ilean" | |
[11/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/path.hlean -o "~/projects/lean/hott/init/path.olean" -c "~/projects/lean/hott/init/path.clean" -i "~/projects/lean/hott/init/path.ilean" | |
[12/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/nat.hlean -o "~/projects/lean/hott/init/nat.olean" -c "~/projects/lean/hott/init/nat.clean" -i "~/projects/lean/hott/init/nat.ilean" | |
[13/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/equiv.hlean -o "~/projects/lean/hott/init/equiv.olean" -c "~/projects/lean/hott/init/equiv.clean" -i "~/projects/lean/hott/init/equiv.ilean" | |
[14/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/ua.hlean -o "~/projects/lean/hott/init/ua.olean" -c "~/projects/lean/hott/init/ua.clean" -i "~/projects/lean/hott/init/ua.ilean" | |
[15/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/pathover.hlean -o "~/projects/lean/hott/init/pathover.olean" -c "~/projects/lean/hott/init/pathover.clean" -i "~/projects/lean/hott/init/pathover.ilean" | |
[16/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/trunc.hlean -o "~/projects/lean/hott/init/trunc.olean" -c "~/projects/lean/hott/init/trunc.clean" -i "~/projects/lean/hott/init/trunc.ilean" | |
[17/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/util.hlean -o "~/projects/lean/hott/init/util.olean" -c "~/projects/lean/hott/init/util.clean" -i "~/projects/lean/hott/init/util.ilean" | |
[18/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/hit.hlean -o "~/projects/lean/hott/init/hit.olean" -c "~/projects/lean/hott/init/hit.clean" -i "~/projects/lean/hott/init/hit.ilean" | |
[19/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/pointed.hlean -o "~/projects/lean/hott/init/pointed.olean" -c "~/projects/lean/hott/init/pointed.clean" -i "~/projects/lean/hott/init/pointed.ilean" | |
[20/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/hedberg.hlean -o "~/projects/lean/hott/init/hedberg.olean" -c "~/projects/lean/hott/init/hedberg.clean" -i "~/projects/lean/hott/init/hedberg.ilean" | |
[21/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/funext.hlean -o "~/projects/lean/hott/init/funext.olean" -c "~/projects/lean/hott/init/funext.clean" -i "~/projects/lean/hott/init/funext.ilean" | |
[22/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/wf.hlean -o "~/projects/lean/hott/init/wf.olean" -c "~/projects/lean/hott/init/wf.clean" -i "~/projects/lean/hott/init/wf.ilean" | |
[23/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/init/default.hlean -o "~/projects/lean/hott/init/default.olean" -c "~/projects/lean/hott/init/default.clean" -i "~/projects/lean/hott/init/default.ilean" | |
[24/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/tools/helper_tactics.hlean -o "~/projects/lean/hott/tools/helper_tactics.olean" -c "~/projects/lean/hott/tools/helper_tactics.clean" -i "~/projects/lean/hott/tools/helper_tactics.ilean" | |
[25/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/priority.hlean -o "~/projects/lean/hott/algebra/priority.olean" -c "~/projects/lean/hott/algebra/priority.clean" -i "~/projects/lean/hott/algebra/priority.ilean" | |
[26/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/unit.hlean -o "~/projects/lean/hott/types/unit.olean" -c "~/projects/lean/hott/types/unit.clean" -i "~/projects/lean/hott/types/unit.ilean" | |
[27/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/bool.hlean -o "~/projects/lean/hott/types/bool.olean" -c "~/projects/lean/hott/types/bool.clean" -i "~/projects/lean/hott/types/bool.ilean" | |
[28/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/binary.hlean -o "~/projects/lean/hott/algebra/binary.olean" -c "~/projects/lean/hott/algebra/binary.clean" -i "~/projects/lean/hott/algebra/binary.ilean" | |
[29/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/relation.hlean -o "~/projects/lean/hott/algebra/relation.olean" -c "~/projects/lean/hott/algebra/relation.clean" -i "~/projects/lean/hott/algebra/relation.ilean" | |
[30/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/hit/colimit.hlean -o "~/projects/lean/hott/hit/colimit.olean" -c "~/projects/lean/hott/hit/colimit.clean" -i "~/projects/lean/hott/hit/colimit.ilean" | |
[31/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/prod.hlean -o "~/projects/lean/hott/types/prod.olean" -c "~/projects/lean/hott/types/prod.clean" -i "~/projects/lean/hott/types/prod.ilean" | |
[32/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/cubical/pathover2.hlean -o "~/projects/lean/hott/cubical/pathover2.olean" -c "~/projects/lean/hott/cubical/pathover2.clean" -i "~/projects/lean/hott/cubical/pathover2.ilean" | |
[33/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/num.hlean -o "~/projects/lean/hott/types/num.olean" -c "~/projects/lean/hott/types/num.clean" -i "~/projects/lean/hott/types/num.ilean" | |
[34/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/order.hlean -o "~/projects/lean/hott/algebra/order.olean" -c "~/projects/lean/hott/algebra/order.clean" -i "~/projects/lean/hott/algebra/order.ilean" | |
[35/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/lattice.hlean -o "~/projects/lean/hott/algebra/lattice.olean" -c "~/projects/lean/hott/algebra/lattice.clean" -i "~/projects/lean/hott/algebra/lattice.ilean" | |
[36/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/graph.hlean -o "~/projects/lean/hott/algebra/graph.olean" -c "~/projects/lean/hott/algebra/graph.clean" -i "~/projects/lean/hott/algebra/graph.ilean" | |
[37/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/group.hlean -o "~/projects/lean/hott/algebra/group.olean" -c "~/projects/lean/hott/algebra/group.clean" -i "~/projects/lean/hott/algebra/group.ilean" | |
[38/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/bundled.hlean -o "~/projects/lean/hott/algebra/bundled.olean" -c "~/projects/lean/hott/algebra/bundled.clean" -i "~/projects/lean/hott/algebra/bundled.ilean" | |
[39/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/sigma.hlean -o "~/projects/lean/hott/types/sigma.olean" -c "~/projects/lean/hott/types/sigma.clean" -i "~/projects/lean/hott/types/sigma.ilean" | |
[40/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/arity.hlean -o "~/projects/lean/hott/arity.olean" -c "~/projects/lean/hott/arity.clean" -i "~/projects/lean/hott/arity.ilean" | |
[41/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/eq.hlean -o "~/projects/lean/hott/types/eq.olean" -c "~/projects/lean/hott/types/eq.clean" -i "~/projects/lean/hott/types/eq.ilean" | |
[42/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/ring.hlean -o "~/projects/lean/hott/algebra/ring.olean" -c "~/projects/lean/hott/algebra/ring.clean" -i "~/projects/lean/hott/algebra/ring.ilean" | |
[43/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/ordered_group.hlean -o "~/projects/lean/hott/algebra/ordered_group.olean" -c "~/projects/lean/hott/algebra/ordered_group.clean" -i "~/projects/lean/hott/algebra/ordered_group.ilean" | |
[44/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/nat/basic.hlean -o "~/projects/lean/hott/types/nat/basic.olean" -c "~/projects/lean/hott/types/nat/basic.clean" -i "~/projects/lean/hott/types/nat/basic.ilean" | |
[45/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/cubical/square.hlean -o "~/projects/lean/hott/cubical/square.olean" -c "~/projects/lean/hott/cubical/square.clean" -i "~/projects/lean/hott/cubical/square.ilean" | |
[46/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/field.hlean -o "~/projects/lean/hott/algebra/field.olean" -c "~/projects/lean/hott/algebra/field.clean" -i "~/projects/lean/hott/algebra/field.ilean" | |
[47/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/pullback.hlean -o "~/projects/lean/hott/types/pullback.olean" -c "~/projects/lean/hott/types/pullback.clean" -i "~/projects/lean/hott/types/pullback.ilean" | |
[48/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/cubical/square2.hlean -o "~/projects/lean/hott/cubical/square2.olean" -c "~/projects/lean/hott/cubical/square2.clean" -i "~/projects/lean/hott/cubical/square2.ilean" | |
[49/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/eq2.hlean -o "~/projects/lean/hott/eq2.olean" -c "~/projects/lean/hott/eq2.clean" -i "~/projects/lean/hott/eq2.ilean" | |
[50/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/pi.hlean -o "~/projects/lean/hott/types/pi.olean" -c "~/projects/lean/hott/types/pi.clean" -i "~/projects/lean/hott/types/pi.ilean" | |
[51/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/logic.hlean -o "~/projects/lean/hott/logic.olean" -c "~/projects/lean/hott/logic.clean" -i "~/projects/lean/hott/logic.ilean" | |
[52/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/arrow.hlean -o "~/projects/lean/hott/types/arrow.olean" -c "~/projects/lean/hott/types/arrow.clean" -i "~/projects/lean/hott/types/arrow.ilean" | |
[53/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/prop_trunc.hlean -o "~/projects/lean/hott/prop_trunc.olean" -c "~/projects/lean/hott/prop_trunc.clean" -i "~/projects/lean/hott/prop_trunc.ilean" | |
[54/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/cubical/cube.hlean -o "~/projects/lean/hott/cubical/cube.olean" -c "~/projects/lean/hott/cubical/cube.clean" -i "~/projects/lean/hott/cubical/cube.ilean" | |
[55/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/hott.hlean -o "~/projects/lean/hott/algebra/hott.olean" -c "~/projects/lean/hott/algebra/hott.clean" -i "~/projects/lean/hott/algebra/hott.ilean" | |
[56/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/cubical/squareover.hlean -o "~/projects/lean/hott/cubical/squareover.olean" -c "~/projects/lean/hott/cubical/squareover.clean" -i "~/projects/lean/hott/cubical/squareover.ilean" | |
[57/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/ordered_ring.hlean -o "~/projects/lean/hott/algebra/ordered_ring.olean" -c "~/projects/lean/hott/algebra/ordered_ring.clean" -i "~/projects/lean/hott/algebra/ordered_ring.ilean" | |
[58/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/W.hlean -o "~/projects/lean/hott/types/W.olean" -c "~/projects/lean/hott/types/W.clean" -i "~/projects/lean/hott/types/W.ilean" | |
[59/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/fiber.hlean -o "~/projects/lean/hott/types/fiber.olean" -c "~/projects/lean/hott/types/fiber.clean" -i "~/projects/lean/hott/types/fiber.ilean" | |
[60/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/cubical/cubeover.hlean -o "~/projects/lean/hott/cubical/cubeover.olean" -c "~/projects/lean/hott/cubical/cubeover.clean" -i "~/projects/lean/hott/cubical/cubeover.ilean" | |
[61/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/cubical/default.hlean -o "~/projects/lean/hott/cubical/default.olean" -c "~/projects/lean/hott/cubical/default.clean" -i "~/projects/lean/hott/cubical/default.ilean" | |
[62/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/nat/order.hlean -o "~/projects/lean/hott/types/nat/order.olean" -c "~/projects/lean/hott/types/nat/order.clean" -i "~/projects/lean/hott/types/nat/order.ilean" | |
[63/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/e_closure.hlean -o "~/projects/lean/hott/algebra/e_closure.olean" -c "~/projects/lean/hott/algebra/e_closure.clean" -i "~/projects/lean/hott/algebra/e_closure.ilean" | |
[64/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/equiv.hlean -o "~/projects/lean/hott/types/equiv.olean" -c "~/projects/lean/hott/types/equiv.clean" -i "~/projects/lean/hott/types/equiv.ilean" | |
[65/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/nat/sub.hlean -o "~/projects/lean/hott/types/nat/sub.olean" -c "~/projects/lean/hott/types/nat/sub.clean" -i "~/projects/lean/hott/types/nat/sub.ilean" | |
[66/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/ordered_field.hlean -o "~/projects/lean/hott/algebra/ordered_field.olean" -c "~/projects/lean/hott/algebra/ordered_field.clean" -i "~/projects/lean/hott/algebra/ordered_field.ilean" | |
[67/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/nat/div.hlean -o "~/projects/lean/hott/types/nat/div.olean" -c "~/projects/lean/hott/types/nat/div.clean" -i "~/projects/lean/hott/types/nat/div.ilean" | |
[68/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/pointed.hlean -o "~/projects/lean/hott/types/pointed.olean" -c "~/projects/lean/hott/types/pointed.clean" -i "~/projects/lean/hott/types/pointed.ilean" | |
[69/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/type_functor.hlean -o "~/projects/lean/hott/types/type_functor.olean" -c "~/projects/lean/hott/types/type_functor.clean" -i "~/projects/lean/hott/types/type_functor.ilean" | |
[70/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/nat/hott.hlean -o "~/projects/lean/hott/types/nat/hott.olean" -c "~/projects/lean/hott/types/nat/hott.clean" -i "~/projects/lean/hott/types/nat/hott.ilean" | |
[71/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/hit/trunc.hlean -o "~/projects/lean/hott/hit/trunc.olean" -c "~/projects/lean/hott/hit/trunc.clean" -i "~/projects/lean/hott/hit/trunc.ilean" | |
[72/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/nat/default.hlean -o "~/projects/lean/hott/types/nat/default.olean" -c "~/projects/lean/hott/types/nat/default.clean" -i "~/projects/lean/hott/types/nat/default.ilean" | |
[73/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/trunc_group.hlean -o "~/projects/lean/hott/algebra/trunc_group.olean" -c "~/projects/lean/hott/algebra/trunc_group.clean" -i "~/projects/lean/hott/algebra/trunc_group.ilean" | |
[74/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/hit/quotient.hlean -o "~/projects/lean/hott/hit/quotient.olean" -c "~/projects/lean/hott/hit/quotient.clean" -i "~/projects/lean/hott/hit/quotient.ilean" | |
[75/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/cylinder.hlean -o "~/projects/lean/hott/homotopy/cylinder.olean" -c "~/projects/lean/hott/homotopy/cylinder.clean" -i "~/projects/lean/hott/homotopy/cylinder.ilean" | |
[76/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/function.hlean -o "~/projects/lean/hott/function.olean" -c "~/projects/lean/hott/function.clean" -i "~/projects/lean/hott/function.ilean" | |
[77/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/lift.hlean -o "~/projects/lean/hott/types/lift.olean" -c "~/projects/lean/hott/types/lift.clean" -i "~/projects/lean/hott/types/lift.ilean" | |
[78/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/arrow_2.hlean -o "~/projects/lean/hott/types/arrow_2.olean" -c "~/projects/lean/hott/types/arrow_2.clean" -i "~/projects/lean/hott/types/arrow_2.ilean" | |
[79/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/list.hlean -o "~/projects/lean/hott/types/list.olean" -c "~/projects/lean/hott/types/list.clean" -i "~/projects/lean/hott/types/list.ilean" | |
[80/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/hit/quotient_functor.hlean -o "~/projects/lean/hott/hit/quotient_functor.olean" -c "~/projects/lean/hott/hit/quotient_functor.clean" -i "~/projects/lean/hott/hit/quotient_functor.ilean" | |
[81/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/hit/coeq.hlean -o "~/projects/lean/hott/hit/coeq.olean" -c "~/projects/lean/hott/hit/coeq.clean" -i "~/projects/lean/hott/hit/coeq.ilean" | |
[82/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/int/basic.hlean -o "~/projects/lean/hott/types/int/basic.olean" -c "~/projects/lean/hott/types/int/basic.clean" -i "~/projects/lean/hott/types/int/basic.ilean" | |
[83/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/sum.hlean -o "~/projects/lean/hott/types/sum.olean" -c "~/projects/lean/hott/types/sum.clean" -i "~/projects/lean/hott/types/sum.ilean" | |
[84/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/hit/pushout.hlean -o "~/projects/lean/hott/hit/pushout.olean" -c "~/projects/lean/hott/hit/pushout.clean" -i "~/projects/lean/hott/hit/pushout.ilean" | |
[85/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/hit/pointed_pushout.hlean -o "~/projects/lean/hott/hit/pointed_pushout.olean" -c "~/projects/lean/hott/hit/pointed_pushout.clean" -i "~/projects/lean/hott/hit/pointed_pushout.ilean" | |
[86/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/int/hott.hlean -o "~/projects/lean/hott/types/int/hott.olean" -c "~/projects/lean/hott/types/int/hott.clean" -i "~/projects/lean/hott/types/int/hott.ilean" | |
[87/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/int/default.hlean -o "~/projects/lean/hott/types/int/default.olean" -c "~/projects/lean/hott/types/int/default.clean" -i "~/projects/lean/hott/types/int/default.ilean" | |
[88/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/trunc.hlean -o "~/projects/lean/hott/types/trunc.olean" -c "~/projects/lean/hott/types/trunc.clean" -i "~/projects/lean/hott/types/trunc.ilean" | |
[89/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/choice.hlean -o "~/projects/lean/hott/choice.olean" -c "~/projects/lean/hott/choice.clean" -i "~/projects/lean/hott/choice.ilean" | |
[90/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/connectedness.hlean -o "~/projects/lean/hott/homotopy/connectedness.olean" -c "~/projects/lean/hott/homotopy/connectedness.clean" -i "~/projects/lean/hott/homotopy/connectedness.ilean" | |
[91/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/univ.hlean -o "~/projects/lean/hott/types/univ.olean" -c "~/projects/lean/hott/types/univ.clean" -i "~/projects/lean/hott/types/univ.ilean" | |
[92/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/precategory.hlean -o "~/projects/lean/hott/algebra/category/precategory.olean" -c "~/projects/lean/hott/algebra/category/precategory.clean" -i "~/projects/lean/hott/algebra/category/precategory.ilean" | |
[93/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/default.hlean -o "~/projects/lean/hott/types/default.olean" -c "~/projects/lean/hott/types/default.clean" -i "~/projects/lean/hott/types/default.ilean" | |
[94/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/wedge.hlean -o "~/projects/lean/hott/homotopy/wedge.olean" -c "~/projects/lean/hott/homotopy/wedge.clean" -i "~/projects/lean/hott/homotopy/wedge.ilean" | |
[95/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/types/fin.hlean -o "~/projects/lean/hott/types/fin.olean" -c "~/projects/lean/hott/types/fin.clean" -i "~/projects/lean/hott/types/fin.ilean" | |
[96/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/hit/prop_trunc.hlean -o "~/projects/lean/hott/hit/prop_trunc.olean" -c "~/projects/lean/hott/hit/prop_trunc.clean" -i "~/projects/lean/hott/hit/prop_trunc.ilean" | |
[97/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/susp.hlean -o "~/projects/lean/hott/homotopy/susp.olean" -c "~/projects/lean/hott/homotopy/susp.clean" -i "~/projects/lean/hott/homotopy/susp.ilean" | |
[98/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/interval.hlean -o "~/projects/lean/hott/homotopy/interval.olean" -c "~/projects/lean/hott/homotopy/interval.clean" -i "~/projects/lean/hott/homotopy/interval.ilean" | |
[99/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/cofiber.hlean -o "~/projects/lean/hott/homotopy/cofiber.olean" -c "~/projects/lean/hott/homotopy/cofiber.clean" -i "~/projects/lean/hott/homotopy/cofiber.ilean" | |
[100/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/hit/set_quotient.hlean -o "~/projects/lean/hott/hit/set_quotient.olean" -c "~/projects/lean/hott/hit/set_quotient.clean" -i "~/projects/lean/hott/hit/set_quotient.ilean" | |
[101/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/sphere.hlean -o "~/projects/lean/hott/homotopy/sphere.olean" -c "~/projects/lean/hott/homotopy/sphere.clean" -i "~/projects/lean/hott/homotopy/sphere.ilean" | |
[102/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/cellcomplex.hlean -o "~/projects/lean/hott/homotopy/cellcomplex.olean" -c "~/projects/lean/hott/homotopy/cellcomplex.clean" -i "~/projects/lean/hott/homotopy/cellcomplex.ilean" | |
[103/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/iso.hlean -o "~/projects/lean/hott/algebra/category/iso.olean" -c "~/projects/lean/hott/algebra/category/iso.clean" -i "~/projects/lean/hott/algebra/category/iso.ilean" | |
[104/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/smash.hlean -o "~/projects/lean/hott/homotopy/smash.olean" -c "~/projects/lean/hott/homotopy/smash.clean" -i "~/projects/lean/hott/homotopy/smash.ilean" | |
[105/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/groupoid.hlean -o "~/projects/lean/hott/algebra/category/groupoid.olean" -c "~/projects/lean/hott/algebra/category/groupoid.clean" -i "~/projects/lean/hott/algebra/category/groupoid.ilean" | |
[106/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/category.hlean -o "~/projects/lean/hott/algebra/category/category.olean" -c "~/projects/lean/hott/algebra/category/category.clean" -i "~/projects/lean/hott/algebra/category/category.ilean" | |
[107/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/constructions/order.hlean -o "~/projects/lean/hott/algebra/category/constructions/order.olean" -c "~/projects/lean/hott/algebra/category/constructions/order.clean" -i "~/projects/lean/hott/algebra/category/constructions/order.ilean" | |
[108/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/group_theory.hlean -o "~/projects/lean/hott/algebra/group_theory.olean" -c "~/projects/lean/hott/algebra/group_theory.clean" -i "~/projects/lean/hott/algebra/group_theory.ilean" | |
[109/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/functor/basic.hlean -o "~/projects/lean/hott/algebra/category/functor/basic.olean" -c "~/projects/lean/hott/algebra/category/functor/basic.clean" -i "~/projects/lean/hott/algebra/category/functor/basic.ilean" | |
[110/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/constructions/fundamental_groupoid.hlean -o "~/projects/lean/hott/algebra/category/constructions/fundamental_groupoid.olean" -c "~/projects/lean/hott/algebra/category/constructions/fundamental_groupoid.clean" -i "~/projects/lean/hott/algebra/category/constructions/fundamental_groupoid.ilean" | |
[111/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/strict.hlean -o "~/projects/lean/hott/algebra/category/strict.olean" -c "~/projects/lean/hott/algebra/category/strict.clean" -i "~/projects/lean/hott/algebra/category/strict.ilean" | |
[112/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/chain_complex.hlean -o "~/projects/lean/hott/homotopy/chain_complex.olean" -c "~/projects/lean/hott/homotopy/chain_complex.clean" -i "~/projects/lean/hott/homotopy/chain_complex.ilean" | |
[113/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/constructions/set.hlean -o "~/projects/lean/hott/algebra/category/constructions/set.olean" -c "~/projects/lean/hott/algebra/category/constructions/set.clean" -i "~/projects/lean/hott/algebra/category/constructions/set.ilean" | |
[114/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/constructions/finite_cats.hlean -o "~/projects/lean/hott/algebra/category/constructions/finite_cats.olean" -c "~/projects/lean/hott/algebra/category/constructions/finite_cats.clean" -i "~/projects/lean/hott/algebra/category/constructions/finite_cats.ilean" | |
[115/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/homotopy_group.hlean -o "~/projects/lean/hott/algebra/homotopy_group.olean" -c "~/projects/lean/hott/algebra/homotopy_group.clean" -i "~/projects/lean/hott/algebra/homotopy_group.ilean" | |
[116/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/default.hlean -o "~/projects/lean/hott/algebra/default.olean" -c "~/projects/lean/hott/algebra/default.clean" -i "~/projects/lean/hott/algebra/default.ilean" | |
[117/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/nat_trans.hlean -o "~/projects/lean/hott/algebra/category/nat_trans.olean" -c "~/projects/lean/hott/algebra/category/nat_trans.clean" -i "~/projects/lean/hott/algebra/category/nat_trans.ilean" | |
[118/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/join.hlean -o "~/projects/lean/hott/homotopy/join.olean" -c "~/projects/lean/hott/homotopy/join.clean" -i "~/projects/lean/hott/homotopy/join.ilean" | |
[119/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/constructions/comma.hlean -o "~/projects/lean/hott/algebra/category/constructions/comma.olean" -c "~/projects/lean/hott/algebra/category/constructions/comma.clean" -i "~/projects/lean/hott/algebra/category/constructions/comma.ilean" | |
[120/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/constructions/opposite.hlean -o "~/projects/lean/hott/algebra/category/constructions/opposite.olean" -c "~/projects/lean/hott/algebra/category/constructions/opposite.clean" -i "~/projects/lean/hott/algebra/category/constructions/opposite.ilean" | |
[121/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/constructions/discrete.hlean -o "~/projects/lean/hott/algebra/category/constructions/discrete.olean" -c "~/projects/lean/hott/algebra/category/constructions/discrete.clean" -i "~/projects/lean/hott/algebra/category/constructions/discrete.ilean" | |
[122/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/constructions/indiscrete.hlean -o "~/projects/lean/hott/algebra/category/constructions/indiscrete.olean" -c "~/projects/lean/hott/algebra/category/constructions/indiscrete.clean" -i "~/projects/lean/hott/algebra/category/constructions/indiscrete.ilean" | |
[123/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/hopf.hlean -o "~/projects/lean/hott/homotopy/hopf.olean" -c "~/projects/lean/hott/homotopy/hopf.clean" -i "~/projects/lean/hott/homotopy/hopf.ilean" | |
[124/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/constructions/product.hlean -o "~/projects/lean/hott/algebra/category/constructions/product.olean" -c "~/projects/lean/hott/algebra/category/constructions/product.clean" -i "~/projects/lean/hott/algebra/category/constructions/product.ilean" | |
[125/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/constructions/initial.hlean -o "~/projects/lean/hott/algebra/category/constructions/initial.olean" -c "~/projects/lean/hott/algebra/category/constructions/initial.clean" -i "~/projects/lean/hott/algebra/category/constructions/initial.ilean" | |
[126/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/constructions/terminal.hlean -o "~/projects/lean/hott/algebra/category/constructions/terminal.olean" -c "~/projects/lean/hott/algebra/category/constructions/terminal.clean" -i "~/projects/lean/hott/algebra/category/constructions/terminal.ilean" | |
[127/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/constructions/sum.hlean -o "~/projects/lean/hott/algebra/category/constructions/sum.olean" -c "~/projects/lean/hott/algebra/category/constructions/sum.clean" -i "~/projects/lean/hott/algebra/category/constructions/sum.ilean" | |
[128/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/circle.hlean -o "~/projects/lean/hott/homotopy/circle.olean" -c "~/projects/lean/hott/homotopy/circle.clean" -i "~/projects/lean/hott/homotopy/circle.ilean" | |
[129/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/complex_hopf.hlean -o "~/projects/lean/hott/homotopy/complex_hopf.olean" -c "~/projects/lean/hott/homotopy/complex_hopf.clean" -i "~/projects/lean/hott/homotopy/complex_hopf.ilean" | |
[130/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/constructions/cone.hlean -o "~/projects/lean/hott/algebra/category/constructions/cone.olean" -c "~/projects/lean/hott/algebra/category/constructions/cone.clean" -i "~/projects/lean/hott/algebra/category/constructions/cone.ilean" | |
[131/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/imaginaroid.hlean -o "~/projects/lean/hott/homotopy/imaginaroid.olean" -c "~/projects/lean/hott/homotopy/imaginaroid.clean" -i "~/projects/lean/hott/homotopy/imaginaroid.ilean" | |
[132/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/constructions/functor.hlean -o "~/projects/lean/hott/algebra/category/constructions/functor.olean" -c "~/projects/lean/hott/algebra/category/constructions/functor.clean" -i "~/projects/lean/hott/algebra/category/constructions/functor.ilean" | |
[133/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/constructions/pushout.hlean -o "~/projects/lean/hott/algebra/category/constructions/pushout.olean" -c "~/projects/lean/hott/algebra/category/constructions/pushout.clean" -i "~/projects/lean/hott/algebra/category/constructions/pushout.ilean" | |
[134/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/freudenthal.hlean -o "~/projects/lean/hott/homotopy/freudenthal.olean" -c "~/projects/lean/hott/homotopy/freudenthal.clean" -i "~/projects/lean/hott/homotopy/freudenthal.ilean" | |
[135/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/constructions/default.hlean -o "~/projects/lean/hott/algebra/category/constructions/default.olean" -c "~/projects/lean/hott/algebra/category/constructions/default.clean" -i "~/projects/lean/hott/algebra/category/constructions/default.ilean" | |
[136/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/functor/attributes.hlean -o "~/projects/lean/hott/algebra/category/functor/attributes.olean" -c "~/projects/lean/hott/algebra/category/functor/attributes.clean" -i "~/projects/lean/hott/algebra/category/functor/attributes.ilean" | |
[137/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/quaternionic_hopf.hlean -o "~/projects/lean/hott/homotopy/quaternionic_hopf.olean" -c "~/projects/lean/hott/homotopy/quaternionic_hopf.clean" -i "~/projects/lean/hott/homotopy/quaternionic_hopf.ilean" | |
[138/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/functor/examples.hlean -o "~/projects/lean/hott/algebra/category/functor/examples.olean" -c "~/projects/lean/hott/algebra/category/functor/examples.clean" -i "~/projects/lean/hott/algebra/category/functor/examples.ilean" | |
[139/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/limits/limits.hlean -o "~/projects/lean/hott/algebra/category/limits/limits.olean" -c "~/projects/lean/hott/algebra/category/limits/limits.clean" -i "~/projects/lean/hott/algebra/category/limits/limits.ilean" | |
[140/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/LES_of_homotopy_groups.hlean -o "~/projects/lean/hott/homotopy/LES_of_homotopy_groups.olean" -c "~/projects/lean/hott/homotopy/LES_of_homotopy_groups.clean" -i "~/projects/lean/hott/homotopy/LES_of_homotopy_groups.ilean" | |
[141/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/limits/colimits.hlean -o "~/projects/lean/hott/algebra/category/limits/colimits.olean" -c "~/projects/lean/hott/algebra/category/limits/colimits.clean" -i "~/projects/lean/hott/algebra/category/limits/colimits.ilean" | |
[142/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/limits/set.hlean -o "~/projects/lean/hott/algebra/category/limits/set.olean" -c "~/projects/lean/hott/algebra/category/limits/set.clean" -i "~/projects/lean/hott/algebra/category/limits/set.ilean" | |
[143/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/functor/adjoint.hlean -o "~/projects/lean/hott/algebra/category/functor/adjoint.olean" -c "~/projects/lean/hott/algebra/category/functor/adjoint.clean" -i "~/projects/lean/hott/algebra/category/functor/adjoint.ilean" | |
[144/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/homotopy_group.hlean -o "~/projects/lean/hott/homotopy/homotopy_group.olean" -c "~/projects/lean/hott/homotopy/homotopy_group.clean" -i "~/projects/lean/hott/homotopy/homotopy_group.ilean" | |
[145/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/sphere2.hlean -o "~/projects/lean/hott/homotopy/sphere2.olean" -c "~/projects/lean/hott/homotopy/sphere2.clean" -i "~/projects/lean/hott/homotopy/sphere2.ilean" | |
[146/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/functor/equivalence.hlean -o "~/projects/lean/hott/algebra/category/functor/equivalence.olean" -c "~/projects/lean/hott/algebra/category/functor/equivalence.clean" -i "~/projects/lean/hott/algebra/category/functor/equivalence.ilean" | |
[147/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/functor/adjoint2.hlean -o "~/projects/lean/hott/algebra/category/functor/adjoint2.olean" -c "~/projects/lean/hott/algebra/category/functor/adjoint2.clean" -i "~/projects/lean/hott/algebra/category/functor/adjoint2.ilean" | |
[148/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/limits/adjoint.hlean -o "~/projects/lean/hott/algebra/category/limits/adjoint.olean" -c "~/projects/lean/hott/algebra/category/limits/adjoint.clean" -i "~/projects/lean/hott/algebra/category/limits/adjoint.ilean" | |
[149/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/functor/yoneda.hlean -o "~/projects/lean/hott/algebra/category/functor/yoneda.olean" -c "~/projects/lean/hott/algebra/category/functor/yoneda.clean" -i "~/projects/lean/hott/algebra/category/functor/yoneda.ilean" | |
[150/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/limits/functor.hlean -o "~/projects/lean/hott/algebra/category/limits/functor.olean" -c "~/projects/lean/hott/algebra/category/limits/functor.clean" -i "~/projects/lean/hott/algebra/category/limits/functor.ilean" | |
[151/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/limits/functor_preserve.hlean -o "~/projects/lean/hott/algebra/category/limits/functor_preserve.olean" -c "~/projects/lean/hott/algebra/category/limits/functor_preserve.clean" -i "~/projects/lean/hott/algebra/category/limits/functor_preserve.ilean" | |
[152/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/limits/default.hlean -o "~/projects/lean/hott/algebra/category/limits/default.olean" -c "~/projects/lean/hott/algebra/category/limits/default.clean" -i "~/projects/lean/hott/algebra/category/limits/default.ilean" | |
[153/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/hit/two_quotient.hlean -o "~/projects/lean/hott/hit/two_quotient.olean" -c "~/projects/lean/hott/hit/two_quotient.clean" -i "~/projects/lean/hott/hit/two_quotient.ilean" | |
[154/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/vankampen.hlean -o "~/projects/lean/hott/homotopy/vankampen.olean" -c "~/projects/lean/hott/homotopy/vankampen.clean" -i "~/projects/lean/hott/homotopy/vankampen.ilean" | |
[155/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/red_susp.hlean -o "~/projects/lean/hott/homotopy/red_susp.olean" -c "~/projects/lean/hott/homotopy/red_susp.clean" -i "~/projects/lean/hott/homotopy/red_susp.ilean" | |
[156/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/hit/refl_quotient.hlean -o "~/projects/lean/hott/hit/refl_quotient.olean" -c "~/projects/lean/hott/hit/refl_quotient.clean" -i "~/projects/lean/hott/hit/refl_quotient.ilean" | |
[157/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/torus.hlean -o "~/projects/lean/hott/homotopy/torus.olean" -c "~/projects/lean/hott/homotopy/torus.clean" -i "~/projects/lean/hott/homotopy/torus.ilean" | |
[158/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/hit/default.hlean -o "~/projects/lean/hott/hit/default.olean" -c "~/projects/lean/hott/hit/default.clean" -i "~/projects/lean/hott/hit/default.ilean" | |
[159/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/functor/exponential_laws.hlean -o "~/projects/lean/hott/algebra/category/functor/exponential_laws.olean" -c "~/projects/lean/hott/algebra/category/functor/exponential_laws.clean" -i "~/projects/lean/hott/algebra/category/functor/exponential_laws.ilean" | |
[160/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/functor/default.hlean -o "~/projects/lean/hott/algebra/category/functor/default.olean" -c "~/projects/lean/hott/algebra/category/functor/default.clean" -i "~/projects/lean/hott/algebra/category/functor/default.ilean" | |
[161/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/default.hlean -o "~/projects/lean/hott/algebra/category/default.olean" -c "~/projects/lean/hott/algebra/category/default.clean" -i "~/projects/lean/hott/algebra/category/default.ilean" | |
[162/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/hit/groupoid_quotient.hlean -o "~/projects/lean/hott/hit/groupoid_quotient.olean" -c "~/projects/lean/hott/hit/groupoid_quotient.clean" -i "~/projects/lean/hott/hit/groupoid_quotient.ilean" | |
[163/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/EM.hlean -o "~/projects/lean/hott/homotopy/EM.olean" -c "~/projects/lean/hott/homotopy/EM.clean" -i "~/projects/lean/hott/homotopy/EM.ilean" | |
[164/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/algebra/category/constructions/rezk.hlean -o "~/projects/lean/hott/algebra/category/constructions/rezk.olean" -c "~/projects/lean/hott/algebra/category/constructions/rezk.clean" -i "~/projects/lean/hott/algebra/category/constructions/rezk.ilean" | |
[165/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/homotopy/default.hlean -o "~/projects/lean/hott/homotopy/default.olean" -c "~/projects/lean/hott/homotopy/default.clean" -i "~/projects/lean/hott/homotopy/default.ilean" | |
[166/167] "~/projects/lean/bin/lean" ~/projects/lean/hott/core.hlean -o "~/projects/lean/hott/core.olean" -c "~/projects/lean/hott/core.clean" -i "~/projects/lean/hott/core.ilean" | |
[167/167] "~/projects/lean/bin/leantags" --relative -- ~/projects/lean/hott/algebra/category/iso.ilean ~/projects/lean/hott/algebra/category/functor/attributes.ilean ~/projects/lean/hott/homotopy/complex_hopf.ilean ~/projects/lean/hott/homotopy/cylinder.ilean ~/projects/lean/hott/homotopy/cofiber.ilean ~/projects/lean/hott/algebra/default.ilean ~/projects/lean/hott/types/int/default.ilean ~/projects/lean/hott/algebra/lattice.ilean ~/projects/lean/hott/tools/helper_tactics.ilean ~/projects/lean/hott/algebra/category/constructions/functor.ilean ~/projects/lean/hott/homotopy/vankampen.ilean ~/projects/lean/hott/cubical/squareover.ilean ~/projects/lean/hott/hit/default.ilean ~/projects/lean/hott/cubical/cube.ilean ~/projects/lean/hott/init/function.ilean ~/projects/lean/hott/algebra/category/functor/equivalence.ilean ~/projects/lean/hott/hit/coeq.ilean ~/projects/lean/hott/types/pointed.ilean ~/projects/lean/hott/prop_trunc.ilean ~/projects/lean/hott/types/num.ilean ~/projects/lean/hott/types/fin.ilean ~/projects/lean/hott/init/funext.ilean ~/projects/lean/hott/types/nat/default.ilean ~/projects/lean/hott/types/fiber.ilean ~/projects/lean/hott/types/default.ilean ~/projects/lean/hott/init/logic.ilean ~/projects/lean/hott/algebra/category/limits/functor.ilean ~/projects/lean/hott/algebra/relation.ilean ~/projects/lean/hott/algebra/category/functor/examples.ilean ~/projects/lean/hott/init/datatypes.ilean ~/projects/lean/hott/homotopy/homotopy_group.ilean ~/projects/lean/hott/algebra/category/constructions/set.ilean ~/projects/lean/hott/algebra/category/functor/default.ilean ~/projects/lean/hott/types/unit.ilean ~/projects/lean/hott/init/ua.ilean ~/projects/lean/hott/algebra/category/limits/adjoint.ilean ~/projects/lean/hott/algebra/category/constructions/opposite.ilean ~/projects/lean/hott/init/bool.ilean ~/projects/lean/hott/types/nat/sub.ilean ~/projects/lean/hott/homotopy/red_susp.ilean ~/projects/lean/hott/algebra/category/limits/default.ilean ~/projects/lean/hott/homotopy/cellcomplex.ilean ~/projects/lean/hott/hit/trunc.ilean ~/projects/lean/hott/hit/pushout.ilean ~/projects/lean/hott/algebra/category/strict.ilean ~/projects/lean/hott/homotopy/join.ilean ~/projects/lean/hott/algebra/ordered_ring.ilean ~/projects/lean/hott/algebra/category/constructions/finite_cats.ilean ~/projects/lean/hott/algebra/category/constructions/discrete.ilean ~/projects/lean/hott/homotopy/hopf.ilean ~/projects/lean/hott/types/list.ilean ~/projects/lean/hott/homotopy/susp.ilean ~/projects/lean/hott/algebra/ring.ilean ~/projects/lean/hott/core.ilean ~/projects/lean/hott/hit/set_quotient.ilean ~/projects/lean/hott/algebra/category/limits/set.ilean ~/projects/lean/hott/algebra/category/functor/basic.ilean ~/projects/lean/hott/homotopy/sphere.ilean ~/projects/lean/hott/init/tactic.ilean ~/projects/lean/hott/init/hit.ilean ~/projects/lean/hott/init/num.ilean ~/projects/lean/hott/algebra/category/precategory.ilean ~/projects/lean/hott/algebra/trunc_group.ilean ~/projects/lean/hott/init/relation.ilean ~/projects/lean/hott/init/hedberg.ilean ~/projects/lean/hott/algebra/field.ilean ~/projects/lean/hott/algebra/category/constructions/product.ilean ~/projects/lean/hott/types/equiv.ilean ~/projects/lean/hott/hit/pointed_pushout.ilean ~/projects/lean/hott/types/W.ilean ~/projects/lean/hott/homotopy/interval.ilean ~/projects/lean/hott/hit/refl_quotient.ilean ~/projects/lean/hott/init/pointed.ilean ~/projects/lean/hott/algebra/category/constructions/sum.ilean ~/projects/lean/hott/algebra/ordered_group.ilean ~/projects/lean/hott/types/univ.ilean ~/projects/lean/hott/init/nat.ilean ~/projects/lean/hott/types/sigma.ilean ~/projects/lean/hott/homotopy/smash.ilean ~/projects/lean/hott/types/pullback.ilean ~/projects/lean/hott/homotopy/LES_of_homotopy_groups.ilean ~/projects/lean/hott/algebra/category/functor/adjoint2.ilean ~/projects/lean/hott/algebra/category/default.ilean ~/projects/lean/hott/algebra/category/constructions/rezk.ilean ~/projects/lean/hott/eq2.ilean ~/projects/lean/hott/homotopy/quaternionic_hopf.ilean ~/projects/lean/hott/algebra/category/constructions/default.ilean ~/projects/lean/hott/hit/quotient.ilean ~/projects/lean/hott/homotopy/circle.ilean ~/projects/lean/hott/homotopy/torus.ilean ~/projects/lean/hott/types/lift.ilean ~/projects/lean/hott/init/util.ilean ~/projects/lean/hott/algebra/ordered_field.ilean ~/projects/lean/hott/cubical/square.ilean ~/projects/lean/hott/hit/colimit.ilean ~/projects/lean/hott/homotopy/freudenthal.ilean ~/projects/lean/hott/types/arrow.ilean ~/projects/lean/hott/init/pathover.ilean ~/projects/lean/hott/algebra/category/constructions/order.ilean ~/projects/lean/hott/homotopy/imaginaroid.ilean ~/projects/lean/hott/types/arrow_2.ilean ~/projects/lean/hott/algebra/category/groupoid.ilean ~/projects/lean/hott/init/path.ilean ~/projects/lean/hott/algebra/category/category.ilean ~/projects/lean/hott/algebra/category/constructions/comma.ilean ~/projects/lean/hott/homotopy/connectedness.ilean ~/projects/lean/hott/algebra/priority.ilean ~/projects/lean/hott/types/pi.ilean ~/projects/lean/hott/cubical/cubeover.ilean ~/projects/lean/hott/arity.ilean ~/projects/lean/hott/init/connectives.ilean ~/projects/lean/hott/types/prod.ilean ~/projects/lean/hott/types/sum.ilean ~/projects/lean/hott/algebra/category/limits/limits.ilean ~/projects/lean/hott/choice.ilean ~/projects/lean/hott/algebra/hott.ilean ~/projects/lean/hott/types/nat/basic.ilean ~/projects/lean/hott/types/nat/div.ilean ~/projects/lean/hott/init/default.ilean ~/projects/lean/hott/algebra/category/functor/yoneda.ilean ~/projects/lean/hott/algebra/category/functor/exponential_laws.ilean ~/projects/lean/hott/init/wf.ilean ~/projects/lean/hott/algebra/category/constructions/initial.ilean ~/projects/lean/hott/cubical/default.ilean ~/projects/lean/hott/types/int/hott.ilean ~/projects/lean/hott/algebra/homotopy_group.ilean ~/projects/lean/hott/types/trunc.ilean ~/projects/lean/hott/algebra/category/functor/adjoint.ilean ~/projects/lean/hott/init/trunc.ilean ~/projects/lean/hott/types/int/basic.ilean ~/projects/lean/hott/algebra/graph.ilean ~/projects/lean/hott/types/nat/order.ilean ~/projects/lean/hott/algebra/bundled.ilean ~/projects/lean/hott/types/bool.ilean ~/projects/lean/hott/init/reserved_notation.ilean ~/projects/lean/hott/algebra/group_theory.ilean ~/projects/lean/hott/init/types.ilean ~/projects/lean/hott/function.ilean ~/projects/lean/hott/homotopy/sphere2.ilean ~/projects/lean/hott/algebra/category/constructions/fundamental_groupoid.ilean ~/projects/lean/hott/algebra/category/limits/functor_preserve.ilean ~/projects/lean/hott/algebra/binary.ilean ~/projects/lean/hott/algebra/category/constructions/terminal.ilean ~/projects/lean/hott/homotopy/default.ilean ~/projects/lean/hott/algebra/category/constructions/pushout.ilean ~/projects/lean/hott/cubical/pathover2.ilean ~/projects/lean/hott/types/type_functor.ilean ~/projects/lean/hott/types/nat/hott.ilean ~/projects/lean/hott/algebra/category/constructions/indiscrete.ilean ~/projects/lean/hott/homotopy/EM.ilean ~/projects/lean/hott/algebra/group.ilean ~/projects/lean/hott/cubical/square2.ilean ~/projects/lean/hott/homotopy/wedge.ilean ~/projects/lean/hott/algebra/category/limits/colimits.ilean ~/projects/lean/hott/algebra/category/constructions/cone.ilean ~/projects/lean/hott/hit/quotient_functor.ilean ~/projects/lean/hott/hit/two_quotient.ilean ~/projects/lean/hott/algebra/e_closure.ilean ~/projects/lean/hott/algebra/category/nat_trans.ilean ~/projects/lean/hott/homotopy/chain_complex.ilean ~/projects/lean/hott/algebra/order.ilean ~/projects/lean/hott/init/equiv.ilean ~/projects/lean/hott/logic.ilean ~/projects/lean/hott/hit/prop_trunc.ilean ~/projects/lean/hott/hit/groupoid_quotient.ilean ~/projects/lean/hott/types/eq.ilean | |
ninja: build stopped: subcommand failed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment