Fails to compile stage2 on msys2/mingw64

[Kreijstal]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [x] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

I failed to reproduce build on msys2

Building stage2: it gets stuck on [ 0%] Built target make_stdlib

make[6]: *** No rule to make target 'runtime/libleanrt_initial-exec.a', needed by 'CMakeFiles/Init_shared'.  Stop.

I followed the steps on the website, downloaded the git code, and successfully compiled state0, and stage1, but it gets stuck on stage2

Context

I have installed all dependencies from msys2 as written in the tutorial

Steps to Reproduce

1. do

cmake -B build -G "Unix Makefiles"  -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++

2. cd build
3. make stage2

Expected behavior: [I expect stage2 to compile]

Actual behavior: [stage2 does not compile]

Versions

git master branch 1382e9fbc4877820570d99f8a1226081a4a41750

Using windows 11 with msys2 mingw enviroment, also latest version

Additional Information

[Kreijstal]

line 74 of stage1/stdlib.make

Lake:
# lake is in its own subdirectory, so must adjust relative paths...
	+"/E/lean4/stage1/bin/leanmake" -C lake bin lib PKG=Lake BIN_NAME=lake.exe $(LEANMAKE_OPTS) LINK_OPTS=' -lstdc++ -lInit_shared -lleanshared' OUT="../E:/lean4/stage1/lib" LIB_OUT="../E:/lean4/stage1/lib/lean" OLEAN_OUT="../E:/lean4/stage1/lib/lean"

we can see it tries to find relative paths.. but fails miserably on windows lmao

[kim-em]

@Kreijstal, could you say what you were expecting to see there?

[kim-em]

If it's a problem in lake then @tydeu may be able to help.

[Kreijstal]

@Kreijstal, could you say what you were expecting to see there?

my drive is E:\ So I dont expect E:\ to be in a relative path. Or ../E/my/path

[tydeu]

The CMake build specifically looks for a relative path for LIB (see here for Windows, so I am not sure were the absolute path is coming from. Maybe this is a by-product of running cmake -B instead of configuring CMake and then running Make directly?

[Kreijstal]

In windows there are sometimes where you can't have relative directories so when you have different drives, maybe it's better to use absolute, not relative? Or fall back

[tydeu]

@Kreijstal Oh, are you building Lean from a different drive than the source and/or build results?

[Kreijstal]

@Kreijstal Oh, are you building Lean from a different drive than the source and/or build results?

yeah I thougth I could, since one drive is faster than the other... but it seems it is not supported

[tydeu]

@Kreijstal Such a case seems like a reasonable feature request we can consider supporting (or better documenting the lack of support for) in the future. Could you update the issue description and title to clarify this is/was the source of problem (e.g., "Lean fails to compile from a different drive")?

[Kreijstal]

Well, now everything is on the same drive but the error is still the following:

make[6]: *** No rule to make target 'runtime/libleanrt_initial-exec.a', needed by 'CMakeFiles/Init_shared'.  Stop.

log.txt