Skip to content

Instantly share code, notes, and snippets.

@spl
Created August 25, 2016 16:06
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save spl/417fb18d876200a87199033707f52211 to your computer and use it in GitHub Desktop.
Save spl/417fb18d876200a87199033707f52211 to your computer and use it in GitHub Desktop.
Errors compiling lean on Mac
$ 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