Fails to compile stage2 on msys2/mingw64

Kreijstal commented 1 month ago

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

do

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

cd build
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 commented 1 month ago

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

semorrison commented 1 month ago

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

semorrison commented 1 month ago

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

Kreijstal commented 1 month ago

@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 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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

Kreijstal commented 1 month ago

@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 commented 1 month ago

@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 commented 1 month ago

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

leanprover / lean4