Alloy: How to pass C flags?

Stream: lean4

[David Garland]

Hello! I'm relatively new to Lean but I'm enjoying playing with it so far.

I'm curious how one might go about passing compiler flags to the C compiler Alloy (the library for C interop created by @Mac Malone) invokes.
The reason I ask this is because I've tried doing the following (minimized example):

import Alloy.C

open scoped Alloy.C

alloy c include <stdio.h> <lean/lean.h>

alloy c extern
def foo (x : UInt32) : IO PUnit := {
  fprintf(stderr, "oops!");
  return lean_io_result_mk_ok(lean_box(0));
}

When compiling this (importing it into Main), I get the following error:

error: > /home/david/.elan/toolchains/stable/bin/leanc -shared -o ./.lake/build/lib/libSlim-Basic-1.so ./.lake/build/ir/Slim/Basic.c.o ./.lake/build/ir/Slim/Basic.alloy.c.o -L./.lake/packages/alloy/.lake/build/lib -L./.lake/build/lib -lAlloy-Util-Parser-1 -lAlloy-C-Grammar-1 -lAlloy-C-Syntax-1 -lAlloy-Util-Shim-1 -lAlloy-Util-Extension-1 -lAlloy-Util-Command-1 -lAlloy-Util-Syntax-1 -lAlloy-Util-ShimElab-1 -lAlloy-C-Shim-1 -lAlloy-Util-Server-Capabilities-1 -lAlloy-Util-Server-Initialize-1 -lAlloy-Util-Server-Methods-1 -lAlloy-C-Server-Clangd-1 -lAlloy-Util-Server-Worker-1 -lAlloy-Util-Server-Extra-1 -lAlloy-Util-Server-1 -lAlloy-C-Server-Worker-1 -lAlloy-C-Server-Location-1 -lAlloy-C-Server-SemanticTokens-1 -lAlloy-C-Server-1 -lAlloy-C-ShimElab-1 -lAlloy-C-Translator-1 -lAlloy-C-Enum-1 -lAlloy-C-IR-1 -lAlloy-Util-Binder-1 -lAlloy-C-ExternImpl-1 -lAlloy-C-ExternDef-1 -lAlloy-Util-OpaqueType-1 -lAlloy-C-ExternType-1 -lAlloy-C-1 -lSlim-Alloy-1 -fPIC
error: stderr:
ld.lld: error: relocation R_X86_64_PC32 cannot be used against symbol 'stderr'; recompile with -fPIC
>>> defined in /home/david/.elan/toolchains/stable/lib/glibc/libc.so
>>> referenced by Basic.alloy.c
>>>               ./.lake/build/ir/Slim/Basic.alloy.c.o:(_alloy_c_l_Slim_foo)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `/home/david/.elan/toolchains/stable/bin/leanc` exited with code 1

As you can see by the first line showing the leanc invocation, I've added -fPIC to my moreLinkArgs in my lakefile.lean-- but this seems to have no effect on Alloy specifically.

I've also tried using addServerFlag (both via the #eval and initialize methods I found described in some code comments) and those don't seem to do what I want either.

Apologies if I've missed anything obvious-- thank you for reading my question (and thank you to Mac especially for the nifty library!)
I hope I've posted this in the right place and haven't broken any sort of etiquette, this is my first time using Zulip.

[Mac Malone]

@David Garland Welcome to the Lean Zulip! No worries about etiquette, your post is great! I believe the problem is that you need to pass -fPIC via moreLeancArgs rather than moreLinkArgs (as it a C compiler flag, not a linker flag).

[David Garland]

Thank you! That fixed it ^^