error when building lean from source

Stream: lean4

[Frederick Pu]

When I try to build lean from source I get the following error

1 warning generated.
Build completed successfully (5811 jobs).
[ 45%] Built target make_stdlib
make[3]: *** [Makefile:146: all] Error 2
make[2]: *** [CMakeFiles/stage1.dir/build.make:86: stage1-prefix/src/stage1-stamp/stage1-build] Error 2
make[1]: *** [CMakeFiles/Makefile2:167: CMakeFiles/stage1.dir/all] Error 2
make: *** [Makefile:136: all] Error 2
make: Leaving directory '/c/Users/pufre/Downloads/CodingProjects/lean4/build/release'

it seems stage1 is successfull but some sort of issue trying to link it together.
I'm using MSYS2 on windows

[Sebastian Ullrich]

My guess is that the actual error message is somewhere above the part you showed

[Frederick Pu]

ning: Lean/Elab/Do.lean:428:14: unused variable x Note: This linter can be disabled with set_option linter.unusedVariables false ℹ [3841/5335] Replayed Lean.Meta.WHNF:c.o info: stderr: C:\Users\pufre\Downloads\CodingProjects\lean4\build\release\stage1\lib\temp\Lean\Meta\WHNF.c:95:26: warning: redeclaration of 'lean_whnf' should not add 'dllexport' attribute [-Wdll-attribute-on-redeclaration] 95 | LEAN_EXPORT lean_object* lean_whnf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); | ^ C:\Users\pufre\Downloads\CodingProjects\lean4\build\release\stage1\lib\temp\Lean\Meta\WHNF.c:77:14: note: previous declaration is here 77 | lean_object* lean_whnf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); | ^ 1 warning generated. ℹ [4278/5335] Replayed Lean.Meta.LevelDefEq:c.o info: stderr: C:\Users\pufre\Downloads\CodingProjects\lean4\build\release\stage1\lib\temp\Lean\Meta\LevelDefEq.c:113:26: warning: redeclaration of 'lean_is_level_def_eq' should not add 'dllexport' attribute [-Wdll-attribute-on-redeclaration] 113 | LEAN_EXPORT lean_object* lean_is_level_def_eq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); | ^ C:\Users\pufre\Downloads\CodingProjects\lean4\build\release\stage1\lib\temp\Lean\Meta\LevelDefEq.c:29:14: note: previous declaration is here 29 | lean_object* lean_is_level_def_eq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); | ^ 1 warning generated. ℹ [4280/5335] Replayed Lean.Meta.ExprDefEq:c.o info: stderr: C:\Users\pufre\Downloads\CodingProjects\lean4\build\release\stage1\lib\temp\Lean\Meta\ExprDefEq.c:952:26: warning: redeclaration of 'lean_is_expr_def_eq' should not add 'dllexport' attribute [-Wdll-attribute-on-redeclaration] 952 | LEAN_EXPORT lean_object* lean_is_expr_def_eq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); | ^ C:\Users\pufre\Downloads\CodingProjects\lean4\build\release\stage1\lib\temp\Lean\Meta\ExprDefEq.c:446:14: note: previous declaration is here 446 | lean_object* lean_is_expr_def_eq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); | ^ 1 warning generated. ℹ [5286/5811] Replayed Lean.Elab.Tactic.Try:c.o info: stderr: C:\Users\pufre\Downloads\CodingProjects\lean4\build\release\stage1\lib\temp\Lean\Elab\Tactic\Try.c:816:26: warning: redeclaration of 'lean_eval_suggest_tactic' should not add 'dllexport' attribute [-Wdll-attribute-on-redeclaration] 816 | LEAN_EXPORT lean_object* lean_eval_suggest_tactic(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); | ^ C:\Users\pufre\Downloads\CodingProjects\lean4\build\release\stage1\lib\temp\Lean\Elab\Tactic\Try.c:338:14: note: previous declaration is here 338 | lean_object* lean_eval_suggest_tactic(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); | ^ 1 warning generated. ℹ [5289/5811] Replayed Lean.Meta.Tactic.Grind.Arith.Cutsat.Var:c.o info: stderr: C:\Users\pufre\Downloads\CodingProjects\lean4\build\release\stage1\lib\temp\Lean\Meta\Tactic\Grind\Arith\Cutsat\Var.c:120:26: warning: redeclaration of 'lean_grind_cutsat_mk_var' should not add 'dllexport' attribute [-Wdll-attribute-on-redeclaration] 120 | LEAN_EXPORT lean_object* lean_grind_cutsat_mk_var(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); | ^ C:\Users\pufre\Downloads\CodingProjects\lean4\build\release\stage1\lib\temp\Lean\Meta\Tactic\Grind\Arith\Cutsat\Var.c:50:14: note: previous declaration is here 50 | lean_object* lean_grind_cutsat_mk_var(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); | ^ 1 warning generated. ℹ [5294/5811] Replayed Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr:c.o info: stderr: C:\Users\pufre\Downloads\CodingProjects\lean4\build\release\stage1\lib\temp\Lean\Meta\Tactic\Grind\Arith\Cutsat\LeCnstr.c:295:26: warning: redeclaration of 'lean_grind_cutsat_assert_le' should not add 'dllexport' attribute [-Wdll-attribute-on-redeclaration] 295 | LEAN_EXPORT lean_object* lean_grind_cutsat_assert_le(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); | ^ C:\Users\pufre\Downloads\CodingProjects\lean4\build\release\stage1\lib\temp\Lean\Meta\Tactic\Grind\Arith\Cutsat\LeCnstr.c:272:14: note: previous declaration is here 272 | lean_object* lean_grind_cutsat_assert_le(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); | ^ 1 warning generated. ℹ [5296/5811] Replayed Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr:c.o info: stderr: C:\Users\pufre\Downloads\CodingProjects\lean4\build\release\stage1\lib\temp\Lean\Meta\Tactic\Grind\Arith\Cutsat\EqCnstr.c:476:26: warning: redeclaration of 'lean_grind_cutsat_assert_eq' should not add 'dllexport' attribute [-Wdll-attribute-on-redeclaration] 476 | LEAN_EXPORT lean_object* lean_grind_cutsat_assert_eq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); | ^ C:\Users\pufre\Downloads\CodingProjects\lean4\build\release\stage1\lib\temp\Lean\Meta\Tactic\Grind\Arith\Cutsat\EqCnstr.c:382:14: note: previous declaration is here 382 | lean_object* lean_grind_cutsat_assert_eq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); | ^ 1 warning generated. Build completed successfully (5811 jobs). [ 45%] Built target make_stdlib make[3]: *** [Makefile:146: all] Error 2 make[2]: *** [CMakeFiles/stage1.dir/build.make:86: stage1-prefix/src/stage1-stamp/stage1-build] Error 2 make[1]: *** [CMakeFiles/Makefile2:167: CMakeFiles/stage1.dir/all] Error 2 make: *** [Makefile:136: all] Error 2