Compiling to C

Stream: lean4

[Calvin Lee]

I'd like to compile my program on a host that does not have lean. Is there any way to compile to a C file that I can then compile on that machine?

[Sebastian Ullrich]

Is this for cross-compiling? Anyway, when you run leanmake bin on your package, it should tell you exactly what commands the build pipeline is running and which files it's putting where. After that, you probably need to take a closer look at the leanc script and its dependencies (Lean headers, gmp, ...).

[Calvin Lee]

Ah I see, so I would have to make sure the lean libraries lib*.a work as well
Unfortunately I'm not doing something so interesting as cross-compiling... For an assignment I am entering a "competition" with my lean program against other people in my class. Unfortunately for this it has to work on a machine with a very old gcc and glibc, so my lean executable and elan cannot run. I think I'll try bootstrapping lean from scratch and see if that works

[Alcides Fonseca]

I wonder whether it would be possible to build lean binaries using Cosmopolitan: https://github.com/jart/cosmopolitan
Then the generated binary could be used in your "old" machine.