Zulip Chat Archive

Stream: lean4

Topic: Compiling to C


view this post on Zulip Calvin Lee (Feb 26 2021 at 06:38):

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?

view this post on Zulip Sebastian Ullrich (Feb 26 2021 at 09:08):

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, ...).

view this post on Zulip Calvin Lee (Feb 26 2021 at 16:45):

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

view this post on Zulip Alcides Fonseca (Mar 02 2021 at 16:33):

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.


Last updated: May 18 2021 at 23:14 UTC