A problem with building the raylib-test executable (Windows)

[noncom]

Hello! I'm trying to experiment with Raylib in Lean under Windows, and it seems to work out-of-the-box until the last step of building the example exe. Here's the error I'm getting:

PS D:\work\my\_lean\lean-test-project\raylib-try-2> lake exe raylib-test
тЬЦ [13/113] Building ┬лraylib-lean┬╗.static:shared
trace: .> c:\Users\user\.elan\toolchains\leanprover--lean4---v4.13.0\bin\leanc.exe -shared -o .\.\.lake/packages\raylib\.lake\build\lib\raylib-lean.dll -Wl,--whole-archive .\.\.lake/packages\raylib\.lake\build\lib\raylib-lean.a -Wl,--no-whole-archive
info: stderr:
ld.lld: error: undefined symbol: UnloadImage
>>> referenced by raylib-lean.a(structures.o):(lean_raylib_Image_finalize)
>>> referenced by raylib-lean.a(functions.o):(lean_raylib__GenTextureMipmaps)

ld.lld: error: undefined symbol: rlGetTextureIdDefault
>>> referenced by raylib-lean.a(structures.o):(lean_raylib_Texture_finalize)
>>> referenced by raylib-lean.a(structures.o):(lean_raylib__Texture_getDefault)
>>> referenced by raylib-lean.a(functions.o):(lean_raylib__GetShapesTexture)

ld.lld: error: undefined symbol: UnloadTexture
>>> referenced by raylib-lean.a(structures.o):(lean_raylib_Texture_finalize)

ld.lld: error: undefined symbol: UnloadRenderTexture
>>> referenced by raylib-lean.a(structures.o):(lean_raylib_RenderTexture_finalize)

ld.lld: error: undefined symbol: UnloadFont
>>> referenced by raylib-lean.a(structures.o):(lean_raylib_Font_finalize)

ld.lld: error: undefined symbol: UnloadMesh
>>> referenced by raylib-lean.a(structures.o):(lean_raylib_Mesh_finalize)

ld.lld: error: undefined symbol: UnloadShader
>>> referenced by raylib-lean.a(structures.o):(lean_raylib_Shader_finalize)

ld.lld: error: undefined symbol: UnloadModelAnimation
>>> referenced by raylib-lean.a(structures.o):(lean_raylib_ModelAnimation_finalize)

ld.lld: error: undefined symbol: UnloadWave
>>> referenced by raylib-lean.a(structures.o):(lean_raylib_Wave_finalize)

ld.lld: error: undefined symbol: UnloadAudioStream
>>> referenced by raylib-lean.a(structures.o):(lean_raylib_AudioStream_finalize)

ld.lld: error: undefined symbol: UnloadSound
>>> referenced by raylib-lean.a(structures.o):(lean_raylib_Sound_finalize)

ld.lld: error: undefined symbol: UnloadMusicStream
>>> referenced by raylib-lean.a(structures.o):(lean_raylib_Music_finalize)

ld.lld: error: undefined symbol: UnloadAutomationEventList
>>> referenced by raylib-lean.a(structures.o):(lean_raylib_AutomationEventList_finalize)

ld.lld: error: undefined symbol: rlGetShaderIdDefault
>>> referenced by raylib-lean.a(structures.o):(lean_raylib__Shader_getDefault)

ld.lld: error: undefined symbol: rlGetShaderLocsDefault
>>> referenced by raylib-lean.a(structures.o):(lean_raylib__Shader_getDefault)

ld.lld: error: undefined symbol: lean_pod_BytesView_class
>>> referenced by raylib-lean.a(structures.o):(.refptr.lean_pod_BytesView_class)

ld.lld: error: undefined symbol: ImageCopy
>>> referenced by raylib-lean.a(functions.o):(lean_raylib_Image_exclusive)
>>> referenced by raylib-lean.a(functions.o):(lean_raylib__ImageCopy)
>>> referenced by raylib-lean.a(functions.o):(lean_raylib__GetGlyphInfo)

ld.lld: error: undefined symbol: IsWindowReady
>>> referenced by raylib-lean.a(functions.o):(lean_raylib__InitWindow)
>>> referenced by raylib-lean.a(functions.o):(lean_raylib__IsWindowReady)

ld.lld: error: undefined symbol: InitWindow
>>> referenced by raylib-lean.a(functions.o):(lean_raylib__InitWindow)

ld.lld: error: undefined symbol: WindowShouldClose
>>> referenced by raylib-lean.a(functions.o):(lean_raylib__WindowShouldClose)

ld.lld: error: too many errors emitted, stopping now (use /errorlimit:0 to see all errors)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command 'c:\Users\user\.elan\toolchains\leanprover--lean4---v4.13.0\bin\leanc.exe' exited with code 1
Some required builds logged failures:
- ┬лraylib-lean┬╗.static:shared
error: build failed

As I understand, the line it passes to leanc.exe indeed only mentions the bindings, and completely misses the parameters for linking the Raylib library itself. I can't however, find any way to influence what's being passed there, whatever I do the command remains the same.

I tried even switching the whole build to gcc, partly borrowing some advise from #3, in hopes that gcc will be used for everything, and it seemed to work, but again only up to this same point of building the exe since lean_exe still uses leanc.exe despite anything.

What is the actual expected behavior of the build system at that point? It doesn't seem to me like that command would succeed, but I might be wrong. How would I go about fixing that?

[KislyjKisel]

Did you add #["-Llake-packages/raylib/raylib/build/raylib", "-lraylib"] to moreLinkArgs in lakefile? Nvm, you're using raylib-test exe, I'll look into it.

[KislyjKisel]

To swap leanc.exe for linking set LEAN_CC environment variable.

Following #3:

• Check files in .lake\packages\raylib\raylib\build\raylib, there should be a library libraylib.a or libraylib.lib.
• If .lake\packages\raylib\raylib directory is empty or doesn't exist, cd .lake\packages\raylib and run git submodule update --init --recursive.
• If library files or the .lake\packages\raylib\raylib\build folder don't exist then try running lake run raylib/buildSubmodule. If it fails paste here its output. Note that if either git or cmake are not in PATH buildSubmodule will fail. You can pass their paths to lake command with -Kgit=path/to/git and -Kcmake=path/to/cmake (or disable them using -Kgit="" -Kcmake="" and build raylib submodule manually) (don't forget to pass -R to update lakefile configuration).
• If you don't have system-wide git and cmake, you can try using w64devkit. In Raylib.lean's lakefile.lean add "-G Unix Makefiles" to cmakeBuildArgs and to package add (replacing UserName and leanprover--lean4---stable with what's on your system):

moreLinkArgs := #[
  "-LC:/Users/UserName/.elan/toolchains/leanprover--lean4---stable/lib"
  ,s!"-L{__dir__}/raylib/build/raylib"
  , "-lraylib"
  , s!"-L{__dir__}/raylib/build/raylib/external/glfw/src"
  , "-LC:/Windows/System32"
  ,"-lglfw3"
  , "-lgdi32"
  , "-lwinmm"
  , "-lopengl32"
  , "-lmsvcrt"
]

Setting LEAN_CC to gcc may allow removing link flags for system libraries ("-LC:/Windows/System32", "-lgdi32" and others below it).

Another option would be to use manually built or system-wide raylib. See raylib's Working on Windows or Working with CMake. To use it add -R -Kraylib=custom -Klflags=... to lake command (replace ... with flags that will be passed to raylib-test's linker, probably -lraylib but may also require -Lpath/to/library/directory).

[noncom]

Well, I'm still working on this. Thanks for the points, they gave me some ideas, but there are still problems. For now all I'm getting are the usual kinds of unimaginable C/C++ errors that break linking at one stage or another because why not. Tried 3 dfirrerent toolchains: MinGW-w64, w64devkit, and just gcc installed from scoop, on 2 different machines. All that this gives is just different errors. And of course I tried what worked in issue #3, but it also gave errors.

I'll post an update when I've got something.

[noncom]

Ok, so I got back to it, and finally figured out the remaining points. There were some differences to #3.
It's worth noting that unlike #3 that wants to setup the dependency for the users own project, I tried to run the bundled demo test.

I wrote all my steps in the form of instruction for myself, I'll just post it here. If you have any comments or think that I missed something, it would be great ot know. Otherwise I think the issue is solved, since the demo now runs for me.

The Process

0 - Pre-requesites

Make sure a Lean toolchain is installed in a known location, for example:

C:/Users/user/.elan/toolchains/leanprover--lean4---v4.13.0

Have gcc, make and cmake available in PATH.

I used x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0 as the gcc compiler distribution.

Note: If at any moment of following these steps an error comes up that the cc program was not found, just duplicate gcc.exe and rename the copy to cc.exe.

1 - Create new project

lake new raylib-try std.lean

2 - Add the Lean Raylib dependency

In the project lakefile.lean add:

def raylibConfig : NameMap String := Id.run $ do
  let mut cfg := NameMap.empty
  cfg := cfg.insert `cc "gcc"
  cfg := cfg.insert `raygui "raygui"
  cfg

require raylib from git
  "https://github.com/KislyjKisel/Raylib.lean" @ "main" with raylibConfig

The config sets gcc as the compiler for the library. It also enables Raygui since it's needed for the test demo project.

Run

lake update

in the project directory to fetch the dependencies. This should create the <project-folder>/.lake/packages directory, with all the dependencies in it.

---

Optional?

Go to <project-folder>/.lake/packages/raylib and run

git submodule update --init --recursive

The raylib/buildSubmodule task should automatically take care of that?

---

3 - Edit the Lean Raylib lakefile

Open <project-folder>/.lake/packages/raylib/lakefile.lean.

3.1 - Additional linker args

To package raylib add

  moreLinkArgs := #[
    "-LC:/Users/user/.elan/toolchains/leanprover--lean4---v4.13.0/lib" -- should point to the `lib` folder of your current toolchain
    , s!"-L{__dir__}/../pod/.lake/build/lib"
    , "-llean-pod"
    , s!"-L{__dir__}/raylib/build/raylib"
    , "-lraylib"
    , s!"-L{__dir__}/raylib/build/raylib/external/glfw/src"
    , "-LC:/Windows/System32"
    -- ,"-lglfw3" -- only add if linking fails otherwise
    , "-lgdi32"
    , "-lwinmm"
    , "-lopengl32"
    , "-lmsvcrt"
  ]

3.2 - CMake generator setup

To the cmakeBuildArgs array add:

  "-G Unix Makefiles"

Explanation: this is needed to prevent the possibility of cmake generating the project for msvc, as that might likely be the default behavior on a Windows system.

4 - Generate CMake projects

Run

lake run raylib/buildSubmodule

This should generate all makefiles for the future build.

5 - Build the Raylib Lean example exe

Run

lake exe raylib-test

This should build the test and run it.

[KislyjKisel]

The raylib/buildSubmodule task should automatically take care of that?

Running raylib/buildSubmodule is optional too. Running the commands manually allows you to see their output. To me the long wait during lake's "Computing build jobs" seemed like a bug, but what takes so much time is actually cloning raylib. Similarly with errors like git's "RPC failed" (seeing subprocess error text is at least some info about why the build fails) .

You can use getLeanSystemLibDir in lakefile to get C:/Users/user/.elan/toolchains/leanprover--lean4---v4.13.0/lib (given Lake.findLeanInstall? works: LEAN_SYSROOT is set, LEAN is set or lean is in PATH):

run_io do
  let leanInstall ← Lake.findLeanInstall?
  match leanInstall with
  | some li => pure li.systemLibDir
  | none => panic! "Could not find lean installation"

"-llean-pod" is included by lake automatically.

Maybe it would be better to change this repo's lakefile to include the additional link args when System.Platform.isWindows. The reason I leave it as is is because the args depend on the toolchain used (not msvc) and are fixed by defining lake_exe in the target project.

Can you test if building the project with LEAN_CC set to gcc makes "-LC:/Windows/System32" or any of -l... unnecessary?

[noncom]

I was trying to find out what you asked about LEAN_CC, and there are two puzzles.

The first is: I realized that if I was not specifying LEAN_CC, it would have meant that:

• lake exe raylib-test was using clang all the way. The problem is that it only prints the commands it uses if there was an error. So when it builds successfully there is no error, it doesn't say explicitly if it was using clang or not. I guess it must have been clang all along because I'm sure I wasn't specifying LEAN_CC.
• lake run raylib/buildSubmodule was using gcc because it was taking the compiler from the cc param of the NameMap passed in params to the dependency. It prints this each time explicitly in the cmake generator printout, so I'm sure it was using gcc all the way.

So I have no idea how it worked, because combining gcc and clang object files during linking is not possbile, as far as I know, because of different layouts used by the compilers.

The second puzzle is that after the updates from 2025.01.04 I couldn't manage to build it again, even following the instruction -- the linking errors have returned. Since prior to that I managed to build and run the demo in fresh projects on 2 different machines, that was quite surprising. I tried changing some stuff back and forth, but no luck, either way it can't either link some libraries or find some symbols, depending on settings.

I'm still figuring this out. But I see that now it's updated to v4.15.0, so I'll retry with the latest version now. I'll post an update when I get something.

To me the long wait during lake's "Computing build jobs" seemed like a bug, but what takes so much time is actually cloning raylib

There is some slight delay, but not really a big lag. Maybe 10-15 seconds or so. Yeah, it's visible in the VSCode explorer that it clones and/or builds Raylib, so no big problem there. Never got any git errors or issues.

You can use getLeanSystemLibDir in lakefile to get C:/Users/user/.elan/toolchains/leanprover--lean4---v4.13.0/lib (given Lake.findLeanInstall? works: LEAN_SYSROOT is set, LEAN is set or lean is in PATH):

I'll try experimenting with that.

"-llean-pod" is included by lake automatically.

That's the interesting part, actually. I figured that it should've been somehow included automatically, but it wasn't! Literally, lake exe raylib-test was failing without that, on both machines. That's why I included it into the instruction as well.

Maybe it would be better to change this repo's lakefile to include the additional link args when System.Platform.isWindows

Yeah, maybe. I wish we really figure out how to write the lakefile in a way that it just works on Windows.

Sorry for longer reply times, I try when I can, so far this experimentation is taking a lot of time, I don't understand why something so simple should be so hard. But it's often the case when dealing with building C/C++ stuff, especially when using some intermediate tools like lake that uses another intermediate tool like leanc.exe, somehow along the way implicitly requiring cc to be a program in the path as well, which should be gcc, I guess, and so all the setup, configuration, and passing the variables becomes a nightmare.

[noncom]

Ok, so, it's amazing, but with the new version the instruction works again. I don't think that the toolchain verison should influence something like that, and I think that I might've messed something up the last time, but not sure what.

Anyway, it works again now. I think it was good before that the example of using Raygui was in, kinda straight to business. Using something like Lean with something like Raylib is not the most popular usecase, so that was very instructive. Maybe it's worth having it, or a separate example with Raygui usage.

Regarding your question, I checked that. Specifying LEAN_CC=gcc produces linking errors by itself, even without removing the additional dependencies from the list:

PS D:\work\my\_lean\lean-test-project\raylib-try-v15> $env:LEAN_CC="gcc"
PS D:\work\my\_lean\lean-test-project\raylib-try-v15> lake exe raylib-test
warning: raylib: repository '.\.\.lake/packages\raylib' has local changes
тЬЦ [5/111] Building ┬лlean-pod┬╗.static:shared
trace: .> c:\Users\user\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe -shared -o .\.\.lake/packages\pod\.lake\build\lib\lean-pod.dll -Wl,--whole-archive .\.\.lake/packages\pod\.lake\build\lib\lean-pod.a -Wl,--no-whole-archive
info: stderr:
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: cannot find -lc++: No such file or directory
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: cannot find -lc++abi: No such file or directory
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: cannot find -lgmp: No such file or directory
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: cannot find -luv: No such file or directory
collect2.exe: error: ld returned 1 exit status
error: external command 'c:\Users\user\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe' exited with code 1
тЬЦ [108/111] Building ┬лraylib-lean┬╗.static:shared
trace: .> c:\Users\user\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe -shared -o .\.\.lake/packages\raylib\.lake\build\lib\raylib-lean.dll -Wl,--whole-archive .\.\.lake/packages\raylib\.lake\build\lib\raylib-lean.a -Wl,--no-whole-archive -LC:/Users/user/.elan/toolchains/leanprover--lean4---v4.15.0/lib -L.\.\.lake/packages\raylib/../pod/.lake/build/lib -llean-pod -L.\.\.lake/packages\raylib/raylib/build/raylib -lraylib -L.\.\.lake/packages\raylib/raylib/build/raylib/external/glfw/src
info: stderr:
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: cannot find -llean-pod: No such file or directory
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: note to link with .\.\.lake/packages\raylib/../pod/.lake/build/lib\lean-pod.a use -l:lean-pod.a or rename it to liblean-pod.a
collect2.exe: error: ld returned 1 exit status
error: external command 'c:\Users\user\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe' exited with code 1
Some required builds logged failures:
- ┬лlean-pod┬╗.static:shared
- ┬лraylib-lean┬╗.static:shared
error: build failed

Removing these dependencies produces even more errors. Here's the log with these libraries, and -llean-pod removed, notice that the initial errors from the long list are about the missing -llean-pod:

PS D:\work\my\_lean\lean-test-project\raylib-try-v15> lake exe raylib-test
warning: raylib: repository '.\.\.lake/packages\raylib' has local changes
тЬЦ [5/111] Building ┬лlean-pod┬╗.static:shared
trace: .> c:\Users\user\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe -shared -o .\.\.lake/packages\pod\.lake\build\lib\lean-pod.dll -Wl,--whole-archive .\.\.lake/packages\pod\.lake\build\lib\lean-pod.a -Wl,--no-whole-archive
info: stderr:
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: cannot find -lc++: No such file or directory
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: cannot find -lc++abi: No such file or directory
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: cannot find -lgmp: No such file or directory
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: cannot find -luv: No such file or directory
collect2.exe: error: ld returned 1 exit status
error: external command 'c:\Users\user\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe' exited with code 1
тЬЦ [108/111] Building ┬лraylib-lean┬╗.static:shared
trace: .> c:\Users\user\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe -shared -o .\.\.lake/packages\raylib\.lake\build\lib\raylib-lean.dll -Wl,--whole-archive .\.\.lake/packages\raylib\.lake\build\lib\raylib-lean.a -Wl,--no-whole-archive -LC:/Users/user/.elan/toolchains/leanprover--lean4---v4.15.0/lib -L.\.\.lake/packages\raylib/raylib/build/raylib -lraylib -L.\.\.lake/packages\raylib/raylib/build/raylib/external/glfw/src  
info: stderr:
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: .\.\.lake/packages\raylib\.lake\build\lib\raylib-lean.a(structures.o):structures.c:(.rdata$.refptr.lean_pod_BytesView_class[.refptr.lean_pod_BytesView_class]+0x0): undefined reference to `lean_pod_BytesView_class'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: .\.\.lake/packages\raylib\.lake\build\lib\raylib-lean.a(functions.o):functions.c:(.rdata$.refptr.lean_pod_Buffer_class[.refptr.lean_pod_Buffer_class]+0x0): undefined reference to `lean_pod_Buffer_class'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: .\.\.lake/packages\raylib\.lake\build\lib\raylib-lean.a(functions.o):functions.c:(.rdata$.refptr.lean_pod_Ptr_class[.refptr.lean_pod_Ptr_class]+0x0): undefined reference to `lean_pod_Ptr_class'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: .\.\.lake/packages\raylib/raylib/build/raylib/libraylib.a(rcore.c.obj): in function `ClosePlatform':
D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/platforms/rcore_desktop_glfw.c:1697:(.text+0x2b2f8): undefined reference to `__imp_timeEndPeriod'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: .\.\.lake/packages\raylib/raylib/build/raylib/libraylib.a(rcore.c.obj): in function `InitTimer':
D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/rcore.c:3520:(.text+0x32ec3): undefined reference to `__imp_timeBeginPeriod'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: .\.\.lake/packages\raylib/raylib/build/raylib/libraylib.a(win32_monitor.c.obj): in function `createMonitor':
D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_monitor.c:82:(.text+0x175): undefined reference to `__imp_CreateDCW'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_monitor.c:86:(.text+0x1ad): undefined reference to `__imp_GetDeviceCaps'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_monitor.c:87:(.text+0x1cb): undefined reference to `__imp_GetDeviceCaps'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_monitor.c:91:(.text+0x22b): undefined reference to `__imp_GetDeviceCaps'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_monitor.c:92:(.text+0x29c): undefined reference to `__imp_GetDeviceCaps'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_monitor.c:95:(.text+0x2c8): undefined reference to `__imp_DeleteDC'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: .\.\.lake/packages\raylib/raylib/build/raylib/libraylib.a(win32_monitor.c.obj): in function `_glfwGetHMONITORContentScaleWin32':
D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_monitor.c:336:(.text+0xc75): undefined reference to `__imp_GetDeviceCaps'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_monitor.c:337:(.text+0xc8d): undefined reference to `__imp_GetDeviceCaps'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: .\.\.lake/packages\raylib/raylib/build/raylib/libraylib.a(win32_monitor.c.obj): in function `_glfwGetGammaRampWin32':
D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_monitor.c:501:(.text+0x12e4): undefined reference to `__imp_CreateDCW'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_monitor.c:502:(.text+0x1302): undefined reference to `__imp_GetDeviceGammaRamp'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_monitor.c:503:(.text+0x1315): undefined reference to `__imp_DeleteDC'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: .\.\.lake/packages\raylib/raylib/build/raylib/libraylib.a(win32_monitor.c.obj): in function `_glfwSetGammaRampWin32':
D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_monitor.c:530:(.text+0x1474): undefined reference to `__imp_CreateDCW'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_monitor.c:531:(.text+0x1492): undefined reference to `__imp_SetDeviceGammaRamp'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_monitor.c:532:(.text+0x14a5): undefined reference to `__imp_DeleteDC'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: .\.\.lake/packages\raylib/raylib/build/raylib/libraylib.a(win32_window.c.obj): in function `createIcon':
D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_window.c:125:(.text+0x232): undefined reference to `__imp_CreateDIBSection'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_window.c:140:(.text+0x2a3): undefined reference to `__imp_CreateBitmap'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_window.c:145:(.text+0x2d2): undefined reference to `__imp_DeleteObject'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_window.c:168:(.text+0x3da): undefined reference to `__imp_DeleteObject'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_window.c:169:(.text+0x3ea): undefined reference to `__imp_DeleteObject'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: .\.\.lake/packages\raylib/raylib/build/raylib/libraylib.a(win32_window.c.obj): in function `updateFramebufferTransparency':
D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_window.c:386:(.text+0xc76): undefined reference to `__imp_CreateRectRgn'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/win32_window.c:393:(.text+0xcdb): undefined reference to `__imp_DeleteObject'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: .\.\.lake/packages\raylib/raylib/build/raylib/libraylib.a(wgl_context.c.obj): in function `choosePixelFormatWGL':
D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/wgl_context.c:75:(.text+0xdc): undefined reference to `__imp_DescribePixelFormat'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/wgl_context.c:220:(.text+0xe32): undefined reference to `__imp_DescribePixelFormat'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: .\.\.lake/packages\raylib/raylib/build/raylib/libraylib.a(wgl_context.c.obj): in function `swapBuffersWGL':
D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/wgl_context.c:344:(.text+0x123d): undefined reference to `__imp_SwapBuffers'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: .\.\.lake/packages\raylib/raylib/build/raylib/libraylib.a(wgl_context.c.obj): in function `_glfwInitWGL':
D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/wgl_context.c:452:(.text+0x1683): undefined reference to `__imp_ChoosePixelFormat'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/wgl_context.c:452:(.text+0x169c): undefined reference to `__imp_SetPixelFormat'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: .\.\.lake/packages\raylib/raylib/build/raylib/libraylib.a(wgl_context.c.obj): in function `_glfwCreateContextWGL':
D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/wgl_context.c:565:(.text+0x1b34): undefined reference to `__imp_DescribePixelFormat'
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/bin/ld.exe: D:/work/my/_lean/lean-test-project/raylib-try-v15/.lake/packages/raylib/raylib/src/external/glfw/src/wgl_context.c:573:(.text+0x1b7a): undefined reference to `__imp_SetPixelFormat'
collect2.exe: error: ld returned 1 exit status
error: external command 'c:\Users\user\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe' exited with code 1
Some required builds logged failures:
- ┬лlean-pod┬╗.static:shared
- ┬лraylib-lean┬╗.static:shared
error: build failed

So specifying LEAN_CC=gcc results in errors. I'm not sure, would that mean that it uses clang then?
Also, I verified that omitting

    , s!"-L{__dir__}/../pod/.lake/build/lib"
    , "-llean-pod"

results in linking errors. Not sure what to do with that. So I just add it to fix the errors.

[KislyjKisel]

So I have no idea how it worked, because combining gcc and clang object files during linking is not possbile, as far as I know, because of different layouts used by the compilers.

After googling a bit I think they are compatible, at least in some cases.

There is some slight delay, but not really a big lag. Maybe 10-15 seconds or so.

For me clean git clone of raylib takes like 5-10 minutes :). And last time I checked it failed to clone at all with HTTP2 in git config.

Maybe it's worth having it, or a separate example with Raygui usage.

Then I'll make some more examples related to bindings' features like raygui soon.

Regarding your question

Thanks for checking! I hoped that the system compiler will have these libraries available by default. I guess it is fixable, but probably not worth it. On Linux it did help when Luau was failing to link due to something with c++ std lib.

Regarding -llean-pod - it may be a lake bug, because IIUC extern_libs from dependencies are always linked automatically. The problem here is probably with compiling Raylib.lean's C code which uses symbols from lean-pod's C code. Maybe the order of -l flags matters and lake doesn't set it so that downstream extern_libs can use upstream ones. Or maybe it is something with the extern_lib compilation code. It certainly works for me, so must be non-deterministic, Windows specific or related to custom toolchain (e.g. -Kcc=..). I'll try to reproduce it minimally later.

[noncom]

After googling a bit I think they are compatible, at least in some cases.

There's an interesting thing. Sorry for the off-topic, it's mostly a note-in-context for my future reference, feel free to skip.

It always amazes me how doing such basic things always feels like navigating in the dark, while in reality these things are invented by us, to help us, are just mere service tools, and have a very well defined behavior. There's always a clear reason why something does or doesn't work, and always a clear and well-defined set of possible options and actions from each point of the process. The complexity is times lower than that of a large business application. There's no RNG involved, no surprises, no divine intervention, no side effects. Parameters, programs and source files in, generated files out, that's it.

Problems of this level, if projected outside of IT feel just idiculous. It's like not being able to walk out of home for a week because you can't figure out how to tie your laces because they just keep raining errors. How did we get outselves into this? I would think that I'm just stupid, ok no problem, but when I search for answers in google, there are countless forums where even C/C++ pros are unable to help in many situations other people have the same problems, and they keep repeating.

I hope that one day all this is just as verified and checked, as a Lean program. At any point it should be able to verify the build script and propose solutions. It should never be more complex than the menu of a McDonald's kiosks where you build a hamburger, figuratively speaking. There were similar attempts like the Nix, and then Guix package managers, but the fundamental flaw was always that they were mathematically incomplete, not even talking about that they did not manage to cover the Windows algebra. There's Maven/Gradle, but that's a different story. There's also Unison, with the groundbreakingly new promising paradigm for all this, but it's too early to say something yet.

Let's see, I just wonder, who's going to be the first to solve the "compilation problem" -- will it be a human-built tool based on mathematical rigor, understanding, and intelligent design, or will it be an AI-based tool? And if it's going to be the latter, then that's gonna be really funny news, we're just unable to.

For me clean git clone of raylib takes like 5-10 minutes :). And last time I checked it failed to clone at all with HTTP2 in git config.

Wow, strange. For me it's like always, cloning goes fast like of any other repo on github. Just letting you know. Maybe it's an internet problem where you are or something like that.

Then I'll make some more examples related to bindings' features like raygui soon.

Thanks! I think that'll be great!

[noncom]

@KislyjKisel well, not surprisingly, the new update broke it again 😄

I'm trying to figure out how to fix it. Currently this is here it breaks:

PS D:\work\my\_lean\lean-test-project\raylib-try-v03\.lake\packages\raylib> lake -d=examples exe Minimal
тЬЦ [19/100] Building raylib/┬лraylib-lean┬╗.static
trace: .> c:\Users\user\.elan\toolchains\leanprover--lean4---v4.15.0\bin\clang.exe -c -o examples\.\./..\.lake\build\ir\native\structures.o examples\.\./..\src\native\structures.c -I c:\Users\user\.elan\toolchains\leanprover--lean4---v4.15.0\include -I examples\.\.lake/packages\pod\src\native\include -I examples\.\./..\raygui\src -I c:\Users\user\.elan\toolchains\leanprover--lean4---v4.15.0\include\clang -fPIC -I examples\.\./..\raylibFork\build\raylib\include -I examples\.\./..\raylibFork\src\external\glfw\include -DLEAN_RAYLIB_FORK
info: stderr:
In file included from examples\.\./..\src\native\structures.c:3:
In file included from examples\.\.lake/packages\pod\src\native\include/lean_pod.h:4:
In file included from D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/x86_64-w64-mingw32/include/stdlib.h:770:
D:/storage/distribs/programming/____mingw64/x86_64-14.2.0-release-posix-seh-ucrt-rt_v12-rev0/mingw64/x86_64-w64-mingw32/include/malloc.h:84:10: fatal error: 'mm_malloc.h' file not found
#include <mm_malloc.h>
         ^~~~~~~~~~~~~
1 error generated.
error: external command 'c:\Users\user\.elan\toolchains\leanprover--lean4---v4.15.0\bin\clang.exe' exited with code 1

... many more instances of the same error ...

So the problem is that it can't find the mm_malloc.h header.
Of this I can say two things:

• It is a part of the gcc installation, and I know what folder this file is, but I don't know how to pass it here. Do you maybe know where from does lake take that command string, and if it's possible to add custom parameters to it, like some "-I<folder>"?
• It's using clang, and it might be that if it uses the include from gcc, there'll be an error of redefinition of some struct, or something like that -- I used to keep getting them when I was mixing clang and gcc. So I'm not sure if specifying the include here would actually help while it's using clang. But if I set it to gcc, other errors will come.

Ultimately, a part of the problem is that it's not clear how does the toolchain coin each of the strings it uses during the process, where from do the parameters come, and where do I specify them. So do you know if there's maybe some good manual on lake which explains all this? Because the only documentation I found explains only the barest minimum of options, and there's nothing like configuring what params does it pass to the C compiler, etc.

[KislyjKisel]

Where the strings come from (not relevant - I forgot a thing, see below):

raylib-lean.static is created by extern_lib in lakefile, which ends in buildStaticLib that takes an array of object file build jobs. Object files are build using buildO, that takes weakArgs and traceArgs that are passed to the compiler. cflags lake option (what you pass in raylibConfig, similar to cc) is added to traceArgs. And cc is the compiler used.

buildO has a docstring showing how the executed command is created.

---

Now I remember that when trying out an example on a different pc, I also had problems. They ignore -R -K.. flags set in the parent directory / main lakefile. To change cc (and cflags etc) for examples you need to modify their lakefile. I wonder if this behavior is a bug? And also I am passing flags using command line, if you are using a separate project with raylibConfig, then I guess there is no way to pass parameters to examples and they may only be run from this project's directory. Later I'll put examples in the main lakefile. Initially I made it this way to make their configuration isolated and easier to understand.

[noncom]

@KislyjKisel I keep mentioning you explicitly because idk if closed issues send any notifications, sorry :)

Now I remember that when trying out an example on a different pc, I also had problems. They ignore -R -K.. flags set in the parent directory / main lakefile. To change cc (and cflags etc) for examples you need to modify their lakefile. I wonder if this behavior is a bug?

Yeah, as I execute lake -d=examples exe Minimal inside <my-project>/.lake/packages/raylib it has no way to guess that there's some <my-project> with parameters, it only sees the raylib project. So yeah, as you have corrected, that's not actually a bug per se.

But it's still kinda weird because:

• There's no lakefile of the examples initially -- the link in your last post leads to a 404, I guess you used some auto-link-copy of an IDE to get that link. This file gets generated after I run for example lake -d=examples exe Minimal. But this means that from the start it is doomed to fail. And only after it fails the first time, I can maybe modify this file in the hope that the second time it will use it for configuring, instead of creating a new one. This loop feels like bad design of how lake exe without an existing lakefile works.
• I haven't found a way to make it create lakefile.lean, and not lakefile.toml. Do you know a way? I get it that .toml was introduced for simplicity, but it's actually quite the opposite because .lean files get typechecked and verified immediately by the IDE while .toml files are not. Idk why this was decided to be a good idea instead of creating a toml-like DSL in Lean.

Later I'll put examples in the main lakefile. Initially I made it this way to make their configuration isolated and easier to understand.

I think that the issue is in that lake doesn't have the concept of project modules, like in for example Gradle. It solves so many problems...

Yeah, maybe I should stop trying to build examples as the first step of verifying that I got a working Lean+Raylib setup, and just actually start the project I was thinking of, so that I don't deal with the build system troubles that much. But still, the fact that these problems come up is kinda worrysome, simply skipping such stuff doesn't feel right.

[KislyjKisel]

So yeah, as you have corrected, that's not actually a bug per se.

Actually, I meant that I tried to configure raylib using -K, but since in this case the main lakefile was from examples the options didn't get passed to raylib.

There's no lakefile of the examples initially

My bad, I didn't use a permalink. I have already deleted it and moved examples lean_exe back to the main lakefile. Now they should work as before: lake exe examples.Minimal without -d. And it means that thay now use raylib's configuration (cc, cflags, lflags etc).

I haven't found a way to make it create lakefile.lean, and not lakefile.toml

lake new <proj> .lean, also .lean can be used as a suffix for template name.