I can't build lean

Stream: general

[Kenny Lau]

ninja gives me error. here's an excerpt:

C:\lean\library\init\algebra\ordered_group.lean:342:7: error: _interaction: trying to evaluate sorry
C:\lean\library\init\algebra\ordered_group.lean:342:7: error: unknown identifier 'h'
C:\lean\library\init\algebra\ordered_group.lean:342:9: error: invalid 'begin-end' expression, ',' expected
C:\lean\library\init\algebra\ordered_group.lean:343:2: error: sync
C:\lean\library\init\algebra\ordered_group.lean:340:0: error: invalid reference to undefined universe level parameter 'u_1'
C:\lean\library\init\algebra\ring.lean:168:11: error: _interaction: trying to evaluate sorry
C:\lean\library\init\algebra\ordered_group.lean:340:0: error: invalid reference to undefined universe level parameter 'u_6'
C:\lean\library\init\algebra\ordered_group.lean:343:6: error: unknown identifier 'neg_add_cancel_left'
C:\lean\library\init\algebra\ordered_group.lean:343:26: error: invalid 'begin-end' expression, ',' expected
C:\lean\library\init\algebra\ordered_group.lean:344:0: error: sync
C:\lean\library\init\algebra\ring.lean:168:11: error: invalid reference to undefined universe level parameter 'u_2'
C:\lean\library\init\algebra\ring.lean:168:11: error: invalid reference to undefined universe level parameter 'u_4'
C:\lean\library\init\algebra\ring.lean:168:11: error: invalid reference to undefined universe level parameter 'u_11'
C:\lean\library\init\algebra\ring.lean:168:11: error: invalid reference to undefined universe level parameter 'u_16'
C:\lean\library\init\algebra\ring.lean:168:39: error: invalid reference to undefined universe level parameter 'u_1'
C:\lean\library\init\algebra\ring.lean:168:39: error: invalid reference to undefined universe level parameter 'u_6'
C:\lean\library\init\algebra\ring.lean:169:22: error: unknown identifier 'add_left_cancel'
C:\lean\library\init\algebra\ordered_group.lean:335:0: error: failed to synthesize type class instance for
α : Type u,
_inst_1 : ordered_comm_group α,
a b c : α,
h : b ≤ -a + c
⊢ has_bind tactic
C:\lean\library\init\algebra\ordered_group.lean:335:0: error: failed to synthesize type class instance for
α : Type u,
_inst_1 : ordered_comm_group α,
a b c : α,
h : b ≤ -a + c
⊢ has_bind tactic
C:\lean\library\init\algebra\ordered_group.lean:337:2: error: failed to synthesize type class instance for
α : Type u,
_inst_1 : ordered_comm_group α,
a b c : α,
h : b ≤ -a + c
⊢ has_bind tactic
C:\lean\library\init\algebra\ordered_group.lean:342:2: error: failed to synthesize type class instance for
α : Type u,
_inst_1 : ordered_comm_group α,
a b c : α,
h : a + b ≤ c
⊢ has_bind tactic
C:\lean\library\init\algebra\ring.lean:174:8: error: _interaction: trying to evaluate sorry
C:\lean\library\init\algebra\ring.lean:174:8: error: invalid reference to undefined universe level parameter 'u_2'
C:\lean\library\init\algebra\ring.lean:174:8: error: invalid reference to undefined universe level parameter 'u_4'
C:\lean\library\init\algebra\ring.lean:174:8: error: invalid reference to undefined universe level parameter 'u_11'
C:\lean\library\init\algebra\ordered_group.lean:336:2: error: don't know how to synthesize placeholder
context:
α : Type u,
_inst_1 : ordered_comm_group α,
a b c : α,
h : b ≤ -a + c
⊢ Type ?
C:\lean\library\init\algebra\ring.lean:174:8: error: invalid reference to undefined universe level parameter 'u_16'
C:\lean\library\init\algebra\ordered_group.lean:341:0: error: failed to synthesize type class instance for
α : Type u,
_inst_1 : ordered_comm_group α,
a b c : α,
h : a + b ≤ c
⊢ has_bind tactic
C:\lean\library\init\algebra\ring.lean:174:41: error: invalid reference to undefined universe level parameter 'u_1'
C:\lean\library\init\algebra\ring.lean:174:41: error: invalid reference to undefined universe level parameter 'u_6'
C:\lean\library\init\algebra\ring.lean:167:36: error: failed to synthesize type class instance for
α : Type u,
_inst_1 : ring α,
a : α
⊢ has_bind tactic
C:\lean\library\init\algebra\ring.lean:175:23: error: unknown identifier 'add_left_cancel'
C:\lean\library\init\algebra\ordered_group.lean:341:0: error: failed to synthesize type class instance for
α : Type u,
_inst_1 : ordered_comm_group α,
a b c : α,
h : a + b ≤ c
⊢ has_bind tactic
C:\lean\library\init\algebra\ordered_group.lean:344:0: error: failed to synthesize type class instance for
α : Type u,
_inst_1 : ordered_comm_group α,
a b c : α,
h : a + b ≤ c
⊢ has_bind tactic
C:\lean\library\init\algebra\ring.lean:168:36: error: failed to synthesize type class instance for
α : Type u,
_inst_1 : ring α,
a : α
⊢ has_bind tactic
C:\lean\library\init\algebra\ordered_group.lean:348:7: error: _interaction: trying to evaluate sorry
C:\lean\library\init\algebra\ordered_group.lean:348:7: error: _interaction: trying to evaluate sorry
C:\lean\library\init\algebra\ordered_group.lean:341:0: error: failed to synthesize type class instance for
α : Type u,

[Kenny Lau]

The error is kinda long and I don't know where to copy it from

[Kenny Lau]

https://github.com/leanprover/lean

[Kenny Lau]

nvm lean is still building

[Simon Hudon]

When you install Lean, where does it put the library? Try deleting that

[Kenny Lau]

I've got a new error

[Kenny Lau]

[36/40] Building CXX object shell/CMakeFiles/lean.dir/server.cpp.obj
[37/40] Linking CXX executable shell\lean_js.exe
[38/40] Linking CXX executable shell\lean.exe
FAILED: shell/lean.exe
cmd.exe /C "cd . && C:\msys64\mingw64\bin\c++.exe  -Wall -Wextra -std=c++11  -D LEAN_WINDOWS -D LEAN_WIN_STACK_SIZE=104857600 -D LEAN_JSON -D_GLIBCXX_USE_CXX11_ABI=0 -D LEAN_MULTI_THREAD -D LEAN_AUTO_THREAD_FINALIZATION -DLEAN_BUILD_TYPE="RELEASE" -O3 -DNDEBUG  -Wl,--stack,104857600 -pthread shell/CMakeFiles/lean.dir/lean.cpp.obj shell/CMakeFiles/lean.dir/server.cpp.obj shell/CMakeFiles/lean.dir/leandoc.cpp.obj  -o shell\lean.exe -Wl,--major-image-version,0,--minor-image-version,0  libleanstatic.a -lgmp -lpsapi -lkernel32 -luser32 -lgdi32 -lwinspool -lshell32 -lole32 -loleaut32 -luuid -lcomdlg32 -ladvapi32 && cmd.exe /C "cd /D C:\lean\build\release\shell && C:\msys64\mingw64\bin\cmake.exe -E remove -f C:/lean/src/../bin/lean.exe && C:\msys64\mingw64\bin\cmake.exe -E copy C:/lean/build/release/shell/lean.exe C:/lean/src/../bin/""
Error copying file "C:/lean/build/release/shell/lean.exe" to "C:/lean/src/../bin/".
ninja: build stopped: subcommand failed.

[Kenny Lau]

I've reverted to an older version by git checkout

[Kenny Lau]

and then I tried to build it again

[Simon Hudon]

Did you pick a revision which builds on Travis and AppVeyor?

[Kenny Lau]

I used 832d235 because Kevin Buzzard is currently running on that

[Kenny Lau]

how do I check if it builds on Travis and AppVeyor?

[Simon Hudon]

You can go: https://github.com/leanprover/lean/commits/master

The commits that pass both have a green check mark

[Kenny Lau]

the last green check mark is March 2 :o

[Mario Carneiro]

@Kenny Lau The last error you posted usually indicates that lean.exeis locked (usually because it is running somewhere), so the copy command fails. I have had success with deleting lean.exe and then running ninja again

[Kenny Lau]

oh thanks, lemme try

[Kenny Lau]

but should I just go with the green check marks

[Mario Carneiro]

Sometimes this fails as well because ninja fails to detect that lean.exe has been deleted, and starts running the build script from after when the file should already exist. When this happens I just touch any cpp file and run ninja again to force recompilation

[Kenny Lau]

@Mario Carneiro I deleted lean.exe, now it's complaining that lean.exe isn't there

[Mario Carneiro]

see my last comment

[Mario Carneiro]

open any cpp file, add and delete a space somewhere, and save, then run ninja again

[Kenny Lau]

oh

[Kenny Lau]

nice

[Kenny Lau]

parabens por mim, it worked

[Kevin Buzzard]

I just built lean head on Ubuntu 16.04 -- hopefully no memory leaks any more!