Building Lean program from source

Stream: lean4

[Locria Cyber]

I bodged together something to build a lean program using Zig and lean's source repo.
lean need to be installed on $PATH.
Nim is used to compile all referenced lean files to C.

https://git.envs.net/iacore/lean-from-source

[Locria Cyber]

Lesson: if the installation ship with src/runtime and src/Init*, it can build any Lean program from source.

[Locria Cyber]

Anyone interested in making this a reality?

[Locria Cyber]

I hope Lake will use this for cross-compiling.

[Locria Cyber]

Is it possible to compile .ilean + .olean to C file? If that's the case, we don't need to ship src/Init/**.lean

[Andrés Goens]

@Locria Cyber could you explain the motivation for that? I'm curious but I don't really understand it

[Mario Carneiro]

Locria Cyber said:

Is it possible to compile .ilean + .olean to C file? If that's the case, we don't need to ship src/Init/**.lean

The lean files are important for enabling go-to-definition on declarations in those files

[Locria Cyber]

The motivation is to use Zig to cross-compile Lean code to many platforms.

[Locria Cyber]

One problem is still that src/runtime depends on too much POSIX stuff.

[Locria Cyber]

Even if I don't use mutex&threads, I can't compile the runtime to wasm32-wasi.