Lake target to run cmake

Stream: lean4

[Tomas Skrivan]

I have a c++ library that I know how to compile only with cmake and would like to create Lean wrappers for it

How do I set up lake project that compiles static library using cmake?

My idea is to create two FileTargets, one that would execute cmake and other to run make to compile static library with Lean compatible C API.

How do I properly set up a FileTarget to run cmake?
I have tried modifying the ffi example in lake repo i.e. using fileTargetWithDep makeFile cmakelistsTarget runCMake where

• makeFile is a path to makefile I'm want to generate
• cmakelistsTarget is input file target pointing to CMakeLists.txt
• runCMake is a function that spawns a process running cmake

When I run lake build, cmake gets executed correctly but I get an error from a linker. Lake seems to run a linker on the generated makefile for some reason.

I will post a mwe later today, but maybe there is an easy fix e.g. another function like fileTargetWithDep that doesn't do as much.

Also, how do I then set up a FileTarget that executes the resulting makefile?

[Arthur Paulino]

There is a thread I can't seem to find in which I ask about compiling C++ code and making it available from Lean 4

[Tomas Skrivan]

I am successfully compiling C++ code, even using lean_external_object to hold some precomputed objects, like matrix factorisation, that are used later on.

I'm mainly curious how to fuse cmake and lake workflow.

I should search those threads though to see if there is some info on cmake.

[Tomas Skrivan]

Right now, I compile the library by manually invoking cmake and make. I want it to be part of lake build command.

Alternatively, I wrote a lake script to do that https://github.com/lecopivo/HouLean/blob/ade9a0b8224b339f8c023897a85c1b993c972dac/lakefile.lean#L21 but it is a mess and it does not feel right.

[Christian Pehle]

This is not on-topic to your question, but I have been considering integrating Lean with Bazel for a while, because I wanted to easily integrate with larger C++ projects (and CMake isn't easily extensible to new languages).

I've managed to compile and link the C output of the lean compiler with Bazel and wrote some super minimal meta build system for lean which produces ninja files (https://github.com/cpehle/bn). The next step would be to integrate this or lake with Bazel and use then Bazel as the overall build system.