Compiling lean 4 code with a C compiler

Stream: lean4

[Oscar Matemb ⚛️]

Any ideas or opinions on how to compile a lean file in C?

[Eric Wieser]

When you declare a lean_exe in your lakefile.lean, you get this automatically

[Oscar Matemb ⚛️]

Thank you. Could you show a working example?

[Eric Wieser]

I think the template package that lake creates has one

[Eric Wieser]

But also, your question is a little unclear (unless you really meant "why doesn't gcc my_file.lean work"), and the gaps I'm filling in might not be what you meant to ask.

[Oscar Matemb ⚛️]

Yes, I am not sure on how to get it to compile with GCC, if you have some documentation or instructions on how I could get it done

[Henrik Böving]

Use the lake build system, everything apart from lake has zero stability guarantees in the future. If you really want to you can run lake build --verbose to see the commands that it runs to compile a Lean file.

[Oscar Matemb ⚛️]

It doesn't seem to work for some reason on my end

[Eric Wieser]

You'll need to tell us exactly what you did on your end and exactly what error it produced for us to help

[Oscar Matemb ⚛️]

#include <stdio.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif

#include "lean/lean.h"  // Include Lean's C API

static bool _G_initialized = false;

LEAN_EXPORT lean_object* initialize_Untitled(uint8_t builtin, lean_object* w) {
    lean_object * res;
    if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
    _G_initialized = true;

    res = initialize_Init(builtin, lean_io_mk_world());
    if (lean_io_result_is_error(res)) return res;
    lean_dec_ref(res);  // Decrement reference to avoid memory leak

    res = initialize_Untitled_Basic(builtin, lean_io_mk_world());
    if (lean_io_result_is_error(res)) return res;
    lean_dec_ref(res);  // Decrement reference to avoid memory leak

    return lean_io_result_mk_ok(lean_box(0));
}

#ifdef __cplusplus
}
#endif

[Oscar Matemb ⚛️]

I am not sure if it is a configuration issue, ' #include "lean/lean.h' throws an error

[Quinn]

I messed around with this, I think you mean compiling files from .lake/build/ir with a c compiler. You need to pass in -I for includes and a path to lean.h, for one. But even that doesn't go all the way thru--- I lost interest before finalizing

[Oscar Matemb ⚛️]

Yes, thanks for insight. I’m still trying to configure the path. I’ll keep this chat updated if any one else comes up with a solution. So far no avail.

[Kim Morrison]

Oscar, you still haven't said what it is that you are doing.

[François G. Dorais]

Use lake env to configure the path automatically.