compilation failed in MacOS

[arademaker]

% lake build
info: downloading component 'lean'
Total: 170.0 MiB Speed:  10.2 MiB/s
info: installing component 'lean'
[22/22] Linking test
trace: .> /Users/ar/.elan/toolchains/leanprover--lean4---v4.8.0-rc1/bin/leanc -o ././.lake/build/bin/test ././.lake/build/ir/Test.c.o.export ././.lake/build/ir/Curl/Errors.c.o.export ././.lake/build/ir/Curl/CurlM.c.o.export ././.lake/build/ir/Curl/Options.c.o.export ././.lake/build/ir/Curl/Extern.c.o.export ././.lake/build/ir/Curl/Easy.c.o.export ././.lake/build/ir/Curl/HeaderData.c.o.export ././.lake/build/ir/Curl.c.o.export ././.lake/build/lib/libleancurl.a -lcurl
info: stderr:
ld64.lld: error: library not found for -lcurl
ld64.lld: error: undefined symbol: _curl_version_info
>>> referenced by ././.lake/build/lib/libleancurl.a(leancurl.o):(symbol _lean_curl_version+0x10)

ld64.lld: error: undefined symbol: _curl_easy_init
>>> referenced by ././.lake/build/lib/libleancurl.a(leancurl.o):(symbol _lean_curl_easy_init+0x4c)

ld64.lld: error: undefined symbol: _curl_global_init
>>> referenced by ././.lake/build/lib/libleancurl.a(leancurl.o):(symbol _lean_curl_easy_init+0x28)

ld64.lld: error: undefined symbol: _curl_easy_cleanup
>>> referenced by ././.lake/build/lib/libleancurl.a(leancurl.o):(symbol curl_handle_finalizer(void*)+0x20)

ld64.lld: error: undefined symbol: _curl_slist_free_all
>>> referenced by ././.lake/build/lib/libleancurl.a(leancurl.o):(symbol _lean_curl_easy_perform+0xf4)

ld64.lld: error: undefined symbol: _curl_easy_perform
>>> referenced by ././.lake/build/lib/libleancurl.a(leancurl.o):(symbol _lean_curl_easy_perform+0x24)

ld64.lld: error: undefined symbol: _curl_easy_setopt
>>> referenced by ././.lake/build/lib/libleancurl.a(leancurl.o):(symbol _lean_curl_easy_setopt_long+0x40)
>>> referenced by ././.lake/build/lib/libleancurl.a(leancurl.o):(symbol _lean_curl_easy_setopt_string+0x48)
>>> referenced by ././.lake/build/lib/libleancurl.a(leancurl.o):(symbol _lean_curl_easy_setopt_strings+0xb8)
>>> referenced 2 more times

ld64.lld: error: undefined symbol: _curl_slist_append
>>> referenced by ././.lake/build/lib/libleancurl.a(leancurl.o):(symbol _lean_curl_easy_setopt_strings+0x84)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command '/Users/ar/.elan/toolchains/leanprover--lean4---v4.8.0-rc1/bin/leanc' exited with code 1
Some build steps logged failures:
- Linking test
error: build failed
(venv) ar@tranco leanCurl %

But notice that I do have libcurl installed

% gcc -lcurl fetch.c

The fetch.c files is

#include <stdio.h>
#include <curl/curl.h>

// Write callback function to write the data to a file
size_t write_data(void *ptr, size_t size, size_t nmemb, FILE *stream) {
    size_t written = fwrite(ptr, size, nmemb, stream);
    return written;
}

int main(void) {
    CURL *curl;
    FILE *fp;
    CURLcode res;
    char *url = "https://example.com"; // URL to fetch
    char outfilename[FILENAME_MAX] = "output.html"; // Output file name

    curl = curl_easy_init(); // Initialize curl
    if (curl) {
        fp = fopen(outfilename, "wb"); // Open the file for writing
        if (fp == NULL) {
            perror("Failed to open file");
            return 1;
        }

        // Set curl options
        curl_easy_setopt(curl, CURLOPT_URL, url);
        curl_easy_setopt(curl, CURLOPT_WRITEFUNCTION, write_data);
        curl_easy_setopt(curl, CURLOPT_WRITEDATA, fp);

        // Perform the request
        res = curl_easy_perform(curl);
        if (res != CURLE_OK) {
            fprintf(stderr, "curl_easy_perform() failed: %s\n", curl_easy_strerror(res));
        }

        // Clean up
        fclose(fp);
        curl_easy_cleanup(curl);
    }

    return 0;
}

Can you provide more instructions about how to use this library? Say I have another project that wants to use our library as a Python project would normally use the requests library... Maybe basic instruction in the README would be helpful.

[bergmannjg]

@arademaker Can you please try to build the package with the configuration option libcurlSharedLib.

It should contain the path to the libcurl shared library as in the following example:

lake -R -KlibcurlSharedLib=/lib/x86_64-linux-gnu/libcurl.so.4 test

Can you provide more instructions about how to use this library?

Please have a look at the example projects.

[bergmannjg]

@arademaker I dont't know why leanc doesn't use -lcurl. A possible ad hoc solution is to reinstall curl, i added a fix to use this approach.

[arademaker]

% lake -R -KlibcurlSharedLib=/opt/homebrew/Cellar/curl/8.9.1/lib/libcurl.dylib build
Build completed successfully.

It also worked with libcurl.a. But I got the error below when I tried #eval main in the HttpGet example.

Lean server printed an error: libc++abi: terminating due to uncaught exception of type lean::exception: Could not find native implementation of external declaration 'Curl.Extern.curl_version' (symbols 'l_Curl_Extern_curl__version___boxed' or 'l_Curl_Extern_curl__version'). For declarations from `Init`, `Std`, or `Lean`, you need to set `supportInterpreter := true` in the relevant `lean_exe` statement in your `lakefile.lean`.

[arademaker]

Do we need the native folder? Is it possible to rely on the library being already available in the system?

[bergmannjg]

Do we need the native folder?

The native folder contains

• the lean bindings to libcurl, this is necessary
• the curl include files, this can be changed with the configuration option libcurlIncludeDir.

Is it possible to rely on the library being already available in the system?

The pre installed library is /usr/lib/libcurl.4.dylib according to otool. The library seems to exist in a cache. I don't know how to access it. So i came up with the reinstall solution.

I added the httpget example to the workflow file.

[arademaker]

I was able to compile and run the example!

cd examples/httpget/
lake -R -KlibCurl=/opt/homebrew/Cellar/curl/8.9.1/lib/libcurl.dylib build
.lake/build/bin/httpget

Still, I would like to understand how to import the library in another project and use the library from any #eval command... I know nothing about the lake file; I need to read spend some time reading about it to undersstand the compilation process.

[arademaker]

My attempt to run #eval main

[bergmannjg]

I would like to understand how to import the library in another project

All example projects show how to import the library (see httpget). The full documentation is here.

use the library from any #eval command

eval doesn't seem to work with shared libraries.