build prerequisites and reservoir

Stream: lean4

[Tomas Skrivan]

My library LeanBLAS requires development files for BLAS to be installed. This is clearly not the case when reservoir tries to build the library. How am I supposed to ensure that BLAS is installed?

[Henrik Böving]

CC @Mac Malone sounds potentially relevant to the FFI goals for this quarter as well maybe?

[Tomas Skrivan]

LeanCopilot has a custom lake target which manually downloads OpenBLAS from github and builds it. I doubt that this is the way it is supposed to be done.

[Mac Malone]

Tomas Skrivan said:

LeanCopilot has a custom lake target which manually downloads OpenBLAS from github and builds it. I doubt that this is the way it is supposed to be done.

No, that is the standard solution. The FFI improvements coming this quarter will make this simpler, less finicky, and more declarative, but the underlying idea is more-or-less the same.

[Tomas Skrivan]

Ok sounds reasonable and I have adopted the approach from LeanCopilot. I'm still having issues using LeanBLAS as a dependency but I need to investigate more carefully what is going wrong.

[Tomas Skrivan]

Mac Malone said:

Tomas Skrivan said:

LeanCopilot has a custom lake target which manually downloads OpenBLAS from github and builds it. I doubt that this is the way it is supposed to be done.

No, that is the standard solution. The FFI improvements coming this quarter will make this simpler, less finicky, and more declarative, but the underlying idea is more-or-less the same.

I'm having really hard time using such library as dependency. I'm trying to use LeanBLAS in SciLean but I'm constantly getting

libopenblas.so: cannot open shared object file: No such file or directory

In LeanBLAS I have a custom target target libopenblas pkg : FilePath := ... that creates libopenblas.so. How am I supposed to say that this should be linked to libLeanBLAS.so? Also I want this to be somehow transitive. If another project depends on LeanBLAS it should not be forced to add explicit linking flat for libopenblas.so.

[Tomas Skrivan]

The only way I can successfully build SciLean with the depedency I have to run lake build leanblas to build explicitly build the dependency and set up scilean package as

def linkArgs := #["-L./.lake/packages/leanblas/.lake/build/lib/", "-lopenblas"]
def moreLeanArgs := #["--load-dynlib=./.lake/packages/leanblas/.lake/build/lib/libopenblas.so"]

package scilean {
  moreLinkArgs := linkArgs
  moreLeanArgs := moreLeanArgs
}

[Tomas Skrivan]

And if I compile binary HelloWorld I can run it only with

LD_LIBRARY_PATH=.lake/packages/leanblas/.lake/build/lib/ .lake/build/bin/HelloWorld