Lake/Alloy pkg-config libraries

Stream: lean4

[Joe Hendrix]

I am trying to figure out how to have lake use pkg-config to use include path and library path for a library using pkg-config. e.g., in Bash, I'd make the include path moreLeancArgs := #[$(pkg-config --cflags libuv)] and also update moreLinkArgs.

I've tried a few routes but all the routes I've seen so far look like they would involve a fair bit of code duplication. Is there a recommended way to do that?

[Notification Bot]

This topic was moved here from #lean4 > Lake/Ally pkg-config libraries by Joe Hendrix.

[Utensil Song]

Something like

def getPkgCflags (pkgName : String) : IO (Array FilePath) := do
  let output ← IO.Process.output {
    cmd := "pkg-config", args := #["--cflags", pkgName]
  }
  let mut paths := #[]
  for s in output.stdout.splitOn do
    paths := paths.push (s : FilePath).normalize
  return paths

in lakefile.lean?

Tested with

script cflags := do
  for path in (<- getPkgCflags "libuv") do
    println! path

  return 0

where it will return an array of -I... or an empty array if not found.

[Daniil Kisel]

You also need to somehow put IO inside the target definition (moreLinkArgs), how to do that?

[Schrodinger ZHU Yifan]

I think such lake configs are wrapped in SchedulerM which is on top of BaseIO

[Schrodinger ZHU Yifan]

I do not recall if SchedulerM can lift EIO or not. but you can obtain BaseIO from EIO by handling exceptions on your own

[Mac Malone]

On the latest nightly, the easiest way to do this is via the new run_io Lake utility.

[Mac Malone]

(previously, this could be done by a custom elaborator, but that is currently causing some problems)

[Joe Hendrix]

@Mac Malone Thanks! run_io solved the problem.