Add explanation on how to cross compile for windows

[ValorZard]

I've been writing down my research here: #new members > Cross Compiling Lean executabel for windows from linux

TL;DR - I've been able to do this

sraya@Penelope:~/Lean4-FFI-Programming-Tutorial-GLFW$ LEAN_CC=x86_64-w64-mingw32-gcc lake build
Build completed successfully.
sraya@Penelope:~/Lean4-FFI-Programming-Tutorial-GLFW$

but it doesn't seem to result in a proper .exe
Any ideas @DSLstandard ?

[DSLstandard]

sup
I am looking into this and I believe I have a solid idea on how to fix this and properly cross-compile Lean4 applications
I will reply again very soon once I come up with a sane solution

[DSLstandard]

I skemmed through Lean4's implementation of the lake build command (Source Link). Sadly, I think currently there is no way to do cross-compilation without modifying Lean4's source code (See REF 1).

My current recommendation for building a Windows Lean4 application on Linux is
to:

1. begin with a Windows environment (maybe with wine on your WSL/Linux host machine; or use your actual Windows host machine),
2. get a Lean4 build for Windows from https://github.com/leanprover/lean4/releases (and download one of those lean-X.YY.Z-windows.zip files and unzip it),
3. and finally just build your Lean4 project with lake.exe build (lake.exe is in located under bin/ within the lean-X.YY.Z-windows.zip file). Make sure to set the PATH/LD_LIBRARY_PATH envvar and other funky Windows-specific things to make sure lake.exe could find its shared library dependencies and not die on launch.

Here is what I found & learnt when investigating the problem -

When you call $ lake build in this project, the following things happen:

1. Lean "compiles" each of your .lean into a .olean.

2. Lean then "compiles" each of the produced .olean into a .c.

3. Lean then compiles each of the produced .c into a .o with the internal function buildLeanO (source link)

   • Important detail: buildLeanO calls compileO oFile srcFile args lean.cc. The variable lean.cc sets the C compiler used. By default, the value of lean.cc follows the "default compiler option" displayed by running the command $ leanc, which in my case (boring detail: I am using NixOS and I am using the Lean4 package provided by the flake.nix in this repository) outputs:

       Lean C compiler
     
       A simple wrapper around a C compiler. Defaults to `/nix/store/67x7pknz0qa2j16x02idf0x98lpcspah-gcc-wrapper-14.3.0/bin/gcc`,
       which can be overridden with the environment variable `LEAN_CC`. All parameters are passed
       as-is to the wrapped compiler.
     
       Interesting options:
       * `--print-cflags`: print C compiler flags necessary for building against the Lean runtime and exit
       * `--print-ldflags`: print C compiler flags necessary for statically linking against the Lean library and exit
     

   • As hinted in the output of $ leanc, setting LEAN_CC can overwrite the compiler option. This means that setting LEAN_CC=x86_64-w64-mingw32-gcc helps to compile the .c files generated from your .lean source code into proper .o object files for your cross-compilation target.

   • For debugging purposes, you may see the actual C compilation command Lean used for compiling the .c files by looking into one of those *.trace files within the directory ./.lake/build/ir/, which is created when you run $ lake build.

   • For example, if you have Main.lean, Lean turns Main.lean into Main.olean, then into Main.c, then finally into Main.c.o.export (I don't know why the object file is suffixed with .export). You can find the trace file named Main.c.o.export.traced and see the exact command Lean used to compile Main.c. The extra C compilation flags Lean uses follows what is printed by $ leanc --print-cflags.

   • For me, $ leanc --print-cflags looks something like:

       $ leanc --print-cflags -I /nix/store/qhkwwlwv0ffl5nhipdy47mcwrfah15nz-lean4-4.21.0/include -fstack-clash-protection -fwrapv -fPIC -fvisibility=hidden
     

   • /nix/store/qhkwwlwv0ffl5nhipdy47mcwrfah15nz-lean4-4.21.0/include contains Lean4 headers like <lean/lean.h>, and fun fact (I learnt this by tracing code starting from src/Leanc.lean (source code)): you can set the environment variable LEAN_SYSROOT to change the parent of the include directory Lean4 will use during compilation of *.c files, i.e.,

       $ leanc --print-cflags
       -I /nix/store/qhkwwlwv0ffl5nhipdy47mcwrfah15nz-lean4-4.21.0/include -fstack-clash-protection -fwrapv -fPIC -fvisibility=hidden
     
       $ LEAN_SYSROOT=/another-location leanc --print-cflags
       -I /another-location/include -fstack-clash-protection -fwrapv -fPIC -fvisibility=hidden
     

4. Lean then compiles the native.c of this project into native.o through this line of code in lakefile.lean here:

    target native.o (pkg : NPackage _package.name) : FilePath := do
        let native_src := "native.c"
        let native_c := pkg.dir / native_src
        let native_o := pkg.buildDir / "native.o"
   
        buildFileAfterDep native_o (<- inputFile native_c True) fun native_src => do
            let lean_dir := (<- getLeanIncludeDir).toString
            compileO native_o native_src #["-I", lean_dir, "-fPIC"] <<<<<< HERE
   

   • If you run $ lake build with that compileO native_o native_src #["-I", lean_dir, "-fPIC"] line in lakefile.lean, native.c is actually compiled with the command cc (as defined by the implementation of compileO (source link)), which usually just points to your host system's default compiler, which typically just compiles the .c files into .o files targetting your host platform, and we don't want that. We want it to be x86_64-w64-mingw32-gcc, and we can do that by changing that line in lakefile.lean like so:

       --- compileO native_o native_src #["-I", lean_dir, "-fPIC"]
       +++ compileO native_o native_src #["-I", lean_dir, "-fPIC"] (compiler := "x86_64-w64-mingw32-gcc")
     

5. Finally, and here is likely the problematic part for you ---

   • In the last step, with native.c and all your .lean files compiled into .o files, Lean4 will try to link them together to form your final executable.

   • When Lean4 is running commands to link your executable (you may find the exact command from a .trace file, or stdout/stderr when $ lake build crashes and dumps trace logs into the console), Lean4 includes a bunch of extra link flags. These extra link flags can be obtained by the running command $ leanc --print-ldflags, which for me displays:

       -I /nix/store/qhkwwlwv0ffl5nhipdy47mcwrfah15nz-lean4-4.21.0/include -fstack-clash-protection -fwrapv -fPIC -fvisibility=hidden -L /nix/store/qhkwwlwv0ffl5nhipdy47mcwrfah15nz-lean4-4.21.0/lib/lean -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group -lstdc++ -lLake /nix/store/f6yc9mbdp17kh3p70lhlix1w21jlj5kp-gmp-with-cxx-6.3.0/lib/libgmp.so -L/nix/store/6r9fwvh9ansv5ddm9kal1w2l18gc1f72-libuv-1.51.0/lib -luv -lm -ldl -pthread
     

   • Your output is likely very different from mine. The exact output depends on how your entire Lean4 toolchain was built in the first place.

   • Anyway, the crucial part is that in these extra link flags, you can see Lean4 is trying to link a bunch of shared/static libraries from, in my case, /nix/store/qhkwwlwv0ffl5nhipdy47mcwrfah15nz-lean4-4.21.0/lib/lean, which includes shared/static libraries like libleancpp.a, libleanrt.a, libleanshared.a (they implement what is declared in <lean/lean.h>, among other extremely important things for Lean4 executables to function properly), and other shared/static libraries like libLean.a, libInit.a, and friends (they are just built versions of Lean4's prelude).

     • For cross-compilation, we should switch out these libraries to those to built for Windows/MinGW (Hypothetically, we would like to switch to the libraries in https://github.com/leanprover/lean4/releases/download/v4.22.0/lean-4.22.0-windows.zip, which are compiled with MinGW I think). Unfortunately, this is impossible... I will explain why soon.

   • Additionally, in my case, the link flags indicate that Lean4 tries to link the final executable with my system's libuv, libgmp, and other things that are meant for use on my host system (I think these 3rd dependencies are there because Lean4's runtime needs them to function properly). We don't want that. To do cross-compilation, we would like to swap out these libraries with variants meant for the cross-compilation target so the linked executable can execute properly on the cross-compilation target's platform.

   • ...The big problem is that there is no way to change these link flags. These link flags are embedded into the lean/lake toolchain program binaries, and there is no logic/lakefile.lean parameters/lake CLI options implemented by Lean4's developers to let us tweak the link flags for cross-compilation purposes.

     • In detail: The exact Lean4 implementation to link your final executable is in the function buildLeanExe (source code), and this part of the function controls the actual link flags used:

         let lean ← getLeanInstall
         let libs ← mkLinkOrder libs
         let args := mkLinkObjArgs objs libs ++ weakArgs ++ traceArgs ++
             #["-L", lean.leanLibDir.toString] ++ lean.ccLinkFlags sharedLean
         compileExe exeFile args lean.cc
       

     • lean.ccLinkFlags sharedLean contains the aforementioned "extra" link flags added by Lean4 to create the final executable. Tracing the source code, I found that lean.ccLinkFlags <arg> ALWAYS contains values read from src/util/ffi.cpp (source file), which contains:

         namespace lean {
         LEAN_EXPORT extern "C" object * lean_get_leanc_extra_flags(object *) {
             return lean_mk_string("@LEANC_EXTRA_CC_FLAGS@");
         }
       
         LEAN_EXPORT extern "C" object * lean_get_leanc_internal_flags(object *) {
             return lean_mk_string("@LEANC_INTERNAL_FLAGS@");
         }
       
         LEAN_EXPORT extern "C" object * lean_get_linker_flags(uint8 link_static) {
             return lean_mk_string(link_static ? "@LEANC_STATIC_LINKER_FLAGS@ @LEAN_EXTRA_LINKER_FLAGS@" : "@LEANC_SHARED_LINKER_FLAGS@ @LEAN_EXTRA_LINKER_FLAGS@");
         }
       
         LEAN_EXPORT extern "C" object * lean_get_internal_linker_flags(object *) {
             return lean_mk_string("@LEANC_INTERNAL_LINKER_FLAGS@");
         }
         }
       

     • The strings "@LEANC_***_FLAGS@" are actually replaced during the build process of the Lean4 project itself. They are replaced by this CMake line in src/util/CMakeLists.txt (source code).

         configure_file(ffi.cpp "${CMAKE_BINARY_DIR}/util/ffi.cpp" @ONLY) <<<< THIS
       
         add_library(util OBJECT name.cpp name_set.cpp
         escaped.cpp bit_tricks.cpp ascii.cpp
         path.cpp lbool.cpp init_module.cpp list_fn.cpp
         timeit.cpp timer.cpp
         name_generator.cpp kvmap.cpp map_foreach.cpp
         options.cpp option_declarations.cpp
         "${CMAKE_BINARY_DIR}/util/ffi.cpp")
       

     • From CMake's docs, CMake's configure_file() replaces each of those strings with the value of the CMake variable of the same name. The corresponding LEANC_***_FLAGS CMake variables are all set in src/CMakeLists.txt (source link), which heavily depends on how Lean4 was built.

tl;dr, it is impossible to use the Lean4/Lake built for your host platform to do
cross-compilation because Lean4 tries to link your Lean4 application executable
with link flags meant to build an executable targetted to your host platform and currently there is no way
offered by the Lean4 developers for you to manually tweak those link flags so the linked Lean4 application executable is targetted to your desired cross-compilation target (by, e.g., switching out the libraries to those
targetted for your cross-compilation target).

Therefore, there are three solutions I can currently think of:

1. The recommendation I wrote at the beginning.

2. (REF 1): Alter the source code of Lean4 to allow the customization of those link flags. This is very annoying and might be too overkill for your purpose. You might want to instead raise a GitHub issue for Lean4's developers. Maybe the Lean4 developers will propose a more-informed/more appropriate solution for doing cross-compilation in Lean4.

3. Actually I am just completely wrong and there is a way to change the flags / to do cross-compilation in Lean4 with methods I do not know about.

[ValorZard]

Hm... okay so I now need to figure out how to build this project on windows natively, which I was avoiding to do since I really hate using MSYS2.
ughhhhhhhh thanks for all the help @DSLstandard ill leave the issue open in case we find a solution

[ValorZard]

So I talked to the lean devs at the office hours today and I got links to two projects to check out for more info
https://github.com/T-Brick/c0deine - this cross compiles lean to webassembly using emscripten
I feel like this could be a good place to start @DSLstandard ? Especially this file here: https://github.com/T-Brick/c0deine/blob/main/BuildWasm.lean
(EDIT: Nevermind, seems like it uses a webassembly build for Lean that only existed for older lean versions?? no idea why they stopped doing that)
https://github.com/acmepjz/md4lean - this is an "idomatic" lean FFI project (shows you how to compile a Lean FFI thing on Windows as well using hacks)

[DSLstandard]

nice! I am having a 2nd look at this now

[DSLstandard]

Good news:

3. Actually I am just completely wrong and there is a way to change the flags / to do cross-compilation in Lean4 with methods I do not know about.

is true.

I was too fixated on the need to change the link flags...... when one could just roll their own custom Lean4 target.

I have cooked up a solution as follows --

First, do the following to install GLFW for Windows and Lean4 for Windows and place them under ./vendor (relative to the root of this Git project):

1. mkdir ./vendor/ (From this Git project's root directory)

2. Download https://github.com/glfw/glfw/releases/download/3.4/glfw-3.4.bin.WIN64.zip

3. Unzip it under ./vendor/.

4. Download https://github.com/leanprover/lean4/releases/download/v4.22.0/lean-4.22.0-windows.zip

5. Also unzip it under ./vendor/.

6. Ensure that your directory structure of ./vendor looks like this:

    ./vendor
      - glfw-3.4.bin.WIN64/
        - docs/
        - include/
        - lib-mingw-w64/
          - libglfw3.a (Important file)
          - glfw3.dll
          - libglfw3dll.a
        - (...)
        - LICENSE.md
        - README.md
      - lean-4.22.0-windows/
        - bin/
        - include/
          - lean/
            - lean.h
            - (...)
          - (...)
        - lib/ (Important directory)
          - clang/(...)
          - lean/(...)
          - crt2.o
          - crtbegin.o
          - crtend.o
          - dllcrt2.o
          - libadvapi32.a
          - ...
          - libuv.a
          - libws2_32.a
   

Then, replace the lakefile.lean of this project with:

import Lake
import Lake.Build.Fetch
import Lake.Config.LeanLib
import Lake.Util.JsonObject

open System Lake DSL

-- TIP: To learn about writing a `lakefile.lean` (or `lakefile.toml`), see
-- https://github.com/leanprover/lean4/blob/master/src/lake/README.md and the
-- directory `examples/` in there.

package «GlfwTest» where
  -- add package configuration options here

target native.o (pkg : NPackage _package.name) : FilePath := do
  let native_src := "native.c"
  let native_c := pkg.dir / native_src
  let native_o := pkg.buildDir / "native.o"

  -- TIP: About 'buildFileAfterDep', see
  -- https://github.com/leanprover/lean4/blob/dfdd682c017a96896d8cfa683f510dd2e0491752/src/lake/Lake/Build/Common.lean#L538.

  -- TIP: About 'inputFile', see
  -- https://github.com/leanprover/lean4/blob/dfdd682c017a96896d8cfa683f510dd2e0491752/src/lake/Lake/Build/Common.lean#L573.

  -- TIP: About 'compileO', see
  -- https://github.com/leanprover/lean4/blob/dfdd682c017a96896d8cfa683f510dd2e0491752/src/lake/Lake/Build/Actions.lean#L79

  buildFileAfterDep native_o (<- inputFile native_c True) fun native_src => do
    let lean_dir := (<- getLeanIncludeDir).toString
    compileO native_o native_src #["-I", lean_dir, "-fPIC"] (compiler := "x86_64-w64-mingw32-gcc")

extern_lib native (pkg : NPackage _package.name) := do
  let name := nameToStaticLib "native"
  let native_o <- fetch <| pkg.target ``native.o
  buildStaticLib (pkg.buildDir / "lib" / name) #[native_o]

/--
Code from https://github.com/leanprover/lean4/blob/ba2cbbf09d4978f416e0ebd1fceeebc2c4138c05/src/lake/Lake/Build/Common.lean#L671
-/
private def mkLinkObjArgs
  (objs : Array FilePath) (libs : Array Dynlib) : Array String
:= Id.run do
  let mut args := #[]
  for obj in objs do
    args := args.push obj.toString
  for lib in libs do
    if let some dir := lib.dir? then
      args := args.push s!"-L{dir}"
    args := args.push s!"-l{lib.name}"
  return args

/--
Code from https://github.com/leanprover/lean4/blob/ba2cbbf09d4978f416e0ebd1fceeebc2c4138c05/src/lake/Lake/Build/Common.lean#L687

Topologically sorts the library dependency tree by name.
Libraries come *before* their dependencies.
-/
private partial def mkLinkOrder (libs : Array Dynlib) : JobM (Array Dynlib) := do
  let r := libs.foldlM (m := Except (Cycle String)) (init := ({}, #[])) fun (v, o) lib =>
    go lib [] v o
  match r with
  | .ok (_, order) => pure order
  | .error cycle => error s!"library dependency cycle:\n{formatCycle cycle}"
where
  go lib (ps : List String) (v : Lean.RBMap String Unit compare) (o : Array Dynlib) := do
    let o := o.push lib
    if v.contains lib.name then
      return (v, o)
    if ps.contains lib.name then
      throw (lib.name :: ps)
    let ps := lib.name :: ps
    let v := v.insert lib.name ()
    let (v, o) ← lib.deps.foldlM (init := (v, o)) fun (v, o) lib =>
      go lib ps v o
    return (v, o)


/--
This part of the code is ripped from
https://github.com/leanprover/lean4/blob/ba2cbbf09d4978f416e0ebd1fceeebc2c4138c05/src/lake/Lake/Build/Common.lean#L759

Build an executable by linking the results of `linkJobs`
using the Lean toolchain's linker.
-/
def buildLeanExeCustom
  (exeFile : FilePath)
  (linkObjs : Array (Job FilePath)) (linkLibs : Array (Job Dynlib))
  (weakArgs traceArgs : Array String := #[]) (_sharedLean : Bool := false)
: SpawnM (Job FilePath) :=
  (Job.collectArray linkObjs "linkObjs").bindM (sync := true) fun objs => do
  (Job.collectArray linkLibs "linkLibs").mapM fun libs => do
    addLeanTrace
    addPureTrace traceArgs "traceArgs"
    addPlatformTrace -- executables are platform-dependent artifacts
    buildArtifactUnlessUpToDate exeFile (ext := FilePath.exeExtension) (exe := true) do
      let libs ← mkLinkOrder libs

      -- ORIGINAL CODE FROM LEAN:
      -- > let args := mkLinkObjArgs objs libs ++ weakArgs ++ traceArgs ++ #["-L", lean.leanLibDir.toString] ++ lean.ccLinkFlags sharedLean
      -- > compileExe exeFile args

      let fakeCCLinkFlags := #[
        -- For debugging while I was coming up with a solution. This prints out
        -- the absolute paths of all static & shared libraries the linker used.
        "-Wl,-trace",

        -- Use static libgcc and libstdc++ for convenience. It also helps to
        -- eliminate random runtime linking errors when the program is run on
        -- Windows.
        "-static-libgcc",
        "-static-libstdc++",

        -- HACK: For some reason "vendor/lean-4.22.0-windows/lib/libc++.a" and
        -- "vendor/lean-4.22.0-windows/lib/libc++abi.a" have duplicate symbols.
        -- Turning on "-Wl,--allow-multiple-definition" to make the linker stop
        -- complaining. Fortunately, the final executable created seems to run
        -- just fine.
        "-Wl,--allow-multiple-definition",

        -- Start from the flags outputted by running
        -- './vendor/lean-4.22.0-windows/leanc.exe --print-ldflags' in Windows,
        -- then adjust the flags to use the libraries under
        -- './vendor/lean-4.22.0-windows'
        --
        -- In my case, 'leanc.exe --print-ldflags' gives:
        --
        -- -I c:\Users\User\Desktop\lean-4.22.0-windows\include
        -- -fstack-clash-protection -fwrapv -L
        -- c:\Users\User\Desktop\lean-4.22.0-windows\lib\lean -Wl,--start-group
        -- -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit
        -- -lleanrt -Wl,--end-group -lc++ -lc++abi -lLake -lgmp -luv -lpsapi
        -- -luser32 -ladvapi32 -liphlpapi -luserenv -lws2_32 -ldbghelp -lole32
        -- -lshell32 -lucrtbase -Wl,--stack,104857600 -licu -lm -lbcrypt
        -- -pthread
        "-I", "vendor/lean-4.22.0-windows/include",
        "-fstack-clash-protection",
        "-fwrapv",
        "-Wl,--start-group",
        "vendor/lean-4.22.0-windows/lib/lean/libleancpp.a",
        "vendor/lean-4.22.0-windows/lib/lean/libLean.a",
        "-Wl,--end-group",
        "vendor/lean-4.22.0-windows/lib/lean/libStd.a",
        "-Wl,--start-group",
        "vendor/lean-4.22.0-windows/lib/lean/libInit.a",
        "vendor/lean-4.22.0-windows/lib/lean/libleanrt.a",
        "-Wl,--end-group",
        "vendor/lean-4.22.0-windows/lib/libc++.a",
        "vendor/lean-4.22.0-windows/lib/libc++abi.a",
        "vendor/lean-4.22.0-windows/lib/libgmp.a",
        "vendor/lean-4.22.0-windows/lib/libuv.a",
        "vendor/lean-4.22.0-windows/lib/libpsapi.a",
        "vendor/lean-4.22.0-windows/lib/libuser32.a",
        "vendor/lean-4.22.0-windows/lib/libadvapi32.a",
        "vendor/lean-4.22.0-windows/lib/libiphlpapi.a",
        "vendor/lean-4.22.0-windows/lib/libuserenv.a",
        "vendor/lean-4.22.0-windows/lib/libws2_32.a",
        "vendor/lean-4.22.0-windows/lib/libdbghelp.a",
        "vendor/lean-4.22.0-windows/lib/libole32.a",
        "vendor/lean-4.22.0-windows/lib/libshell32.a",
        "vendor/lean-4.22.0-windows/lib/libucrtbase.a",
        "vendor/lean-4.22.0-windows/lib/libicu.a",
        "vendor/lean-4.22.0-windows/lib/libbcrypt.a"
      ]

      -- Flags for
      let moreLinkFlagsForGLFW := #[
        "vendor/glfw-3.4.bin.WIN64/lib-mingw-w64/libglfw3.a",
        "-lgdi32", -- Required. See https://www.glfw.org/docs/latest/build_guide.html#build_link_mingw.
      ]

      let args := mkLinkObjArgs objs libs ++ weakArgs ++ traceArgs ++ fakeCCLinkFlags ++ moreLinkFlagsForGLFW

      -- N.B. This is g++, NOT gcc. If you use `gcc`, you will get a bunch of
      -- C++-related undefined reference errors.
      let linker := "x86_64-w64-mingw32-g++"

      compileExe exeFile args linker

-- Dummy `lean_exe` target. We actually just want the 'LeanExeDecl' object this
-- declaration makes.
lean_exe «glfw_test.exe» where
  root := `Main

@[default_target]
target glfw_test_exe_from_linux_to_windows (pkg : NPackage _package.name) : FilePath := do
  -- Code ripped from
  -- https://github.com/leanprover/lean4/blob/ba2cbbf09d4978f416e0ebd1fceeebc2c4138c05/src/lake/Lake/Build/Executable.lean#L16
  withRegisterJob "glfw_test_exe_from_linux_to_windows" <| withCurrPackage pkg do
    let self <- «glfw_test.exe».get
    let mut objJobs := #[]
    let mut libJobs := #[]
    let shouldExport := self.supportInterpreter
    for facet in self.root.nativeFacets shouldExport do
      objJobs := objJobs.push <| ← facet.fetch self.root
    let .ok imports _ ← (← self.root.transImports.fetch).wait
      | error s!"bad imports (see the '{self.root.name.toString}' job for details)"
    for mod in imports do
      for facet in mod.nativeFacets shouldExport do
        objJobs := objJobs.push <| ← facet.fetch mod
    let libs := imports.foldl (·.insert ·.lib) OrdHashSet.empty |>.toArray
    for lib in libs do
      for link in lib.moreLinkObjs do
        objJobs := objJobs.push <| ← link.fetchIn lib.pkg
      for link in lib.moreLinkLibs do
        libJobs := libJobs.push <| ← link.fetchIn lib.pkg
    let deps := (← (← self.pkg.transDeps.fetch).await).push self.pkg
    for dep in deps do
      for lib in dep.externLibs do
        objJobs := objJobs.push <| ← lib.static.fetch
    buildLeanExeCustom self.file objJobs libJobs self.weakLinkArgs self.linkArgs self.sharedLean

After that, remove the printf(...) line from lean_glfwCreateWindow in ./native.c:

@@ -34,7 +34,19 @@ lean_obj_res lean_glfwTerminate(lean_obj_arg world) {
 }
 
 lean_obj_res lean_glfwCreateWindow(uint32_t width, uint32_t height, b_lean_obj_arg title, lean_obj_arg world) {
-       printf("lean_glfwCreateWindow %dx%d\n", width, height);
+       // FIXME: printf() makes your Windows executable crash with exit code
+       // -1073741819 (Hex: 0xC0000005. Apparently it means memory access
+       // violation/null-pointer access/or whatever) for some reason. Comment
+       // this out for now...
+       //
+       // printf("lean_glfwCreateWindow %dx%d\n", width, height);
+
+       // RANDOM TIP: I was testing the Windows executable on a Windows 11 instance running
+       // within virt-manager with no GPU setup. Without setting this window
+       // hint, GLFW complains (You need to setup a glfwSetErrorCallback handle to
+       // see the error) that "WGL: The driver does not appear to support OpenGL."
+       glfwWindowHint(GLFW_CLIENT_API, GLFW_NO_API);
+
        char const *title_cstr = lean_string_cstr(title);
        GLFWwindow *win = glfwCreateWindow(width, height, title_cstr, NULL, NULL);
        return lean_io_result_mk_ok(lean_alloc_external(get_glfw_window_class(), win));

Finally, run:

$ rm -r .lake/   # Optional. This ensures a clean setup
$ LEAN_CC=x86_64-w64-mingw32-gcc lake build

and Lean4 should build the executable ./.lake/build/bin/glfw_test.exe.

You may then simply copy ./.lake/build/bin/glfw_test.exe to a Windows host,
directly run the executable, and a GLFW window should pop up. You should not have to install any shared libraries, since the
executable is almost entirely built by static linking.

[DSLstandard]

Some notes:

• Make sure your Lake & Lean versions are Lake version 5.0.0-src+v4.22.0 (Lean version 4.22.0) (NB.: NOT 4.21.X), otherwise you may run into errors about having undefined symbols in the lakefile.lean file.
• (REF 1) For whatever reason, if ./native.c calls printf(), your Windows executable will crash with exit code -1073741819 (Hex: 0xC0000005. Apparently it means memory access violation/null-pointer access/or whatever) for some reason. I could not figure out why exactly.
• I am confident that the fakeCCLinkFlags I used in buildLeanExeCustom is not proper (and this might be the reason why the error in (REF 1) exists). I have little experience with doing cross-compilation and working with linkers to handle non-trivial tasks. Basically, I spent hours just tweaking the link flags to try to eliminate all linking errors through trial and error.
• I have looked through https://github.com/T-Brick/c0deine/blob/main/BuildWasm.lean and https://github.com/acmepjz/md4lean but sadly they did not directly help much. However, after having looked through those projects only then did I realize that a simple solution can be created using Lean4 custom targets.

[ValorZard]

Gotcha! this should all be a big help. Thanks!