Zulip Chat Archive

Stream: lean4

Topic: lakefile dependencies

Jesse Vogel (Jul 15 2022 at 14:34):

It has been a few months since I updated my lean version, but something has changed so that my lakefile.lean doesn't work anymore. I get the following error: 'dependencies' is not a field of structure 'Lake.PackageConfig'. How should I add dependencies now? My lakefile.lean is as follows:

import Lake
open Lake DSL

package MyPackage {
  dependencies := #[{
    name := `name
    src := Source.git "<url>" "<commit>"
  }]
}

Julian Berman (Jul 15 2022 at 14:36):

The DSL syntax changed. The Lake readme has an example, basically change it to:

import Lake
open Lake DSL

package MyPackage

require name from git
  "<url>"

Sebastian Ullrich (Jul 15 2022 at 14:37):

You usually want to drop @"<commit>", it is persisted in the manifest.json

Julian Berman (Jul 15 2022 at 14:37):

Ah interesting, good to know.

Julian Berman (Jul 15 2022 at 14:38):

(Obviously what Sebastian said, though if you have lean_packages/ in your gitignore remember to un-ignore lean_packages/manifest.json then)

Tomas Skrivan (Jul 15 2022 at 14:56):

Another thing I have encountered recently. My build fails if I'm offline as dependencies can't be updated. How can I ignore this?

Mac (Jul 15 2022 at 17:07):

@Tomas Skrivan Lake should not be trying to update dependencies if you are running a regular lake build instead of a lake update (and you have already download an initial set of dependencies). Can you elaborate more on the problem you are experiencing?

Tomas Skrivan (Jul 15 2022 at 17:19):

@Mac When I disconnect from the internet and run lake build I get the following error:

error: stderr:
fatal: unable to access 'https://github.com/leanprover-community/mathlib4.git/': Could not resolve host: github.com
error: git exited with code 128

My lakefile is:

import Lake
open Lake DSL System

package scilean

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"@"8f609e0ed826dde127c8bc322cb6f91c5369d37a"

@[defaultTarget]
lean_lib SciLean {
  roots := #[`SciLean]
}

Lean version is: leanprover/lean4:nightly-2022-07-11

Mac (Jul 15 2022 at 17:42):

@Tomas Skrivan do you think you could make that an issue on the Lake repo? Or, if you'd rather I can do it myself.

Tomas Skrivan (Jul 15 2022 at 17:44):

@Mac Sure, I make an issue and try to reproduce it on a clean repo.

Mac (Jul 15 2022 at 17:45):

Thanks! I do believe I already have a fix. The issue is mostly for posterity sake (and it give a number to the test :wink:)

Tomas Skrivan (Jul 15 2022 at 17:52):

Github issue #104

z battleman (Jul 28 2022 at 17:46):

In trying to do this it's telling me it's expecting a command at the line where I call the require. I suspect its because my syntax for the package is different, but I'm not sure. Does anyone know how to do this? Here is my Lakefile

import Lake
open System Lake DSL

def cDir : FilePath := "c"
def ffiSrc := cDir / "bindings.c"
def buildDir := defaultBuildDir
def packagesDir := "third_party"

def ffiOTarget (pkgDir : FilePath) : FileTarget :=
  let oFile := pkgDir / buildDir / cDir / "bindings.o"
  let srcTarget := inputFileTarget <| pkgDir / ffiSrc
  fileTargetWithDep oFile srcTarget fun srcFile => do
    compileO oFile srcFile #["-I", (← getLeanIncludeDir).toString,
                             "-I", "third_party/OpenBLASLib/include"]


def cLibTarget (pkgDir : FilePath) : FileTarget :=
  let libFile := pkgDir / buildDir / cDir / "libffi.a"
  staticLibTarget libFile #[ffiOTarget pkgDir]


package LeanAlg (pkgDir) (args) {

  -- customize layout
  --srcDir := "LeanAlg"
  --libRoots := #[`mathVec, `mathMatrix]
  -- specify the lib as an additional target
  moreLibTargets := #[cLibTarget pkgDir]
  moreLinkArgs := #["-L", "./third_party/OpenBLASLib/lib",
                    "-lopenblas",
                    "-Wl,-R./third_party/OpenBLASLib/lib"]
}

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

Sebastian Ullrich (Jul 28 2022 at 18:35):

What version of Lean is this?

z battleman (Jul 28 2022 at 19:31):

it's the nightly version of lean4 (version 4.0.0-nightly-2022-04-28)

Mac (Jul 28 2022 at 19:33):

@z battleman that version is older than the addition of the require command. You may wish to update to the latest nightly mathlib4 supports (i.e., 07-24)

z battleman (Jul 28 2022 at 19:34):

ah that makes sense. I just updated. But now its upset at the syntax of the package LeanAlg line so I'll try to fix that. Thank you :)

z battleman (Jul 28 2022 at 19:59):

oh that broke a lot of things... in all my files I'm getting error loading library: libleanffi.a.so and when I try to build I'm just getting exit with status 139 does anyone recognize these?

z battleman (Jul 28 2022 at 20:12):

here's my attempt to port my lakefile

import Lake
open System Lake DSL

lean_lib LeanAlg

def cDir : FilePath := "c"
def ffiSrc := cDir / "bindings.c"
def buildDir := defaultBuildDir
def packagesDir := "third_party"
def pkgDir := __dir__

def ffiOTarget : FileTarget :=
  let oFile := pkgDir / buildDir / cDir / "bindings.o"
  let srcTarget := inputFileTarget <| pkgDir / ffiSrc
  fileTargetWithDep oFile srcTarget fun srcFile => do
    compileO oFile srcFile #["-I", (← getLeanIncludeDir).toString, "-fPIC",
                             "-I", "third_party/OpenBLASLib/include"]

def cLibTarget (pkgDir : FilePath) : FileTarget :=
  let libFile := pkgDir / buildDir / cDir / "libffi.a"
  staticLibTarget libFile #[ffiOTarget]

extern_lib cLib :=
  let libFile := buildDir / nameToStaticLib "libffi"
  staticLibTarget libFile #[ffiOTarget]


package LeanAlg {
  -- customize layout
  --srcDir := "LeanAlg"
  --libRoots := #[`mathVec, `mathMatrix]
  -- specify the lib as an additional target
  moreLibTargets := #[cLibTarget __dir__]
  moreLinkArgs := #["-L", "./third_party/OpenBLASLib/lib",
                    "-lopenblas",
                    "-Wl,-R./third_party/OpenBLASLib/lib"]
  precompileModules := true
}

--require mathlib from git
--  "https://github.com/leanprover-community/mathlib4.git"

z battleman (Jul 28 2022 at 20:20):

ah well I got it to build at least by removing precompileModules and changing around some other things. Now its segfaulting of course, but that's progress :)

z battleman (Jul 28 2022 at 20:48):

Is there anything obvious that would cause it to segault like ordering of arguments or whatnot?

import Lake
open System Lake DSL

lean_lib LeanAlg

package LeanAlg {
  -- customize layout
  --srcDir := "LeanAlg"
  --libRoots := #[`mathVec, `mathMatrix]
  -- specify the lib as an additional target
  --moreLibTargets := #[cLibTarget __dir__]
  srcDir := "LeanAlg"
  moreLinkArgs := #["-L", "./third_party/OpenBLASLib/lib",
                    "-lopenblas",
                    "-Wl,-R./third_party/OpenBLASLib/lib"]
  --precompileModules := true
}

@[defaultTarget] lean_exe test {
  root := `Main
}
def packagesDir := "third_party"
def pkgDir := __dir__
def cSrcDir := pkgDir / "c"
def cBuildDir := pkgDir / _package.buildDir / "c"

def ffiOTarget : FileTarget :=
  let oFile := cBuildDir / "bindings.o"
  let srcTarget := inputFileTarget <| cSrcDir / "bindings.c"
  fileTargetWithDep oFile srcTarget fun srcFile => do
    compileO oFile srcFile #["-I", (← getLeanIncludeDir).toString,
                             "-I", "third_party/OpenBLASLib/include"]

--def cLibTarget (pkgDir : FilePath) : FileTarget :=
--  let libFile := pkgDir / buildDir / cDir / "libffi.a"
--  staticLibTarget libFile #[ffiOTarget]

extern_lib cLib :=
  let libFile := cBuildDir / nameToStaticLib "libffi"
  staticLibTarget libFile #[ffiOTarget]

The only thing that changed on the Lean end is that this is no longer accepted

@[extern "mathMatrix_initialize"]
private constant mathMatrix_initializer : IO Unit

builtin_initialize mathMatrix_initializer

so I rmeoved them, but I'm not sure if they need to be replaced

z battleman (Jul 28 2022 at 20:56):

oh... those being gone would definitely cause a segfault, but I'm not sure how to replace them with the current Lean4 syntax

z battleman (Jul 28 2022 at 21:06):

ah, this did it

@[extern "mathMatrix_initialize"]
opaque mathMatrix_initializer : IO Unit

builtin_initialize mathMatrix_initializer

Thanks for the help!!

Mac (Jul 29 2022 at 03:44):

z battleman said:

ah well I got it to build at least by removing precompileModules and changing around some other things. Now its segfaulting of course, but that's progress :)

You should be able to add this back (I believe the problem was the existence of the moreLibTargets setting).

z battleman (Jul 29 2022 at 03:53):

I've been trying to add it back to some luck. It is compiling, but Lean is unable to find the .so file associated with it. It's in the build/c/ directory though so I'm not sure why its failing to find it

Mac (Jul 29 2022 at 03:54):

@z battleman what OS are you on?

z battleman (Jul 29 2022 at 03:55):

I'm on Arch Kernel version 5.18.9-arch1-1

Mac (Jul 29 2022 at 03:55):

And what is the specific error you are getting from Lean?

z battleman (Jul 29 2022 at 03:56):

error loading library, libleanffi.so: cannot open shared object file. No such file or directory

z battleman (Jul 29 2022 at 03:57):

the file definitely is in ./build/c/

Mac (Jul 29 2022 at 03:57):

Oh wait, one problem (hopefully that one) is that you have name the library you passed to nameToStaticLib "libffi", it should just be "ffi", the definition will add the lib prefix (on non-Windows).

z battleman (Jul 29 2022 at 03:58):

ah sorry that's an old version with that typo, its currently "leanffi". Here is the most recent version

import Lake
open System Lake DSL


package LeanAlg {
  -- customize layout
  --srcDir := "LeanAlg"
  --libRoots := #[`mathVec, `mathMatrix]
  -- specify the lib as an additional target
  --moreLibTargets := #[cLibTarget __dir__]
  moreLinkArgs := #["-L", "./third_party/OpenBLASLib/lib",
                    "-lopenblas",
                    "-Wl,-R./third_party/OpenBLASLib/lib"]

  precompileModules := true
  packagesDir := "third_party"
}

@[defaultTarget] lean_exe test {
  root := `Main
}

def pkgDir := __dir__
def cSrcDir := pkgDir / "c"
def cBuildDir := pkgDir / _package.buildDir / "c"

def ffiOTarget : FileTarget :=
  let oFile := cBuildDir / "bindings.o"
  let srcTarget := inputFileTarget <| cSrcDir / "bindings.c"
  fileTargetWithDep oFile srcTarget fun srcFile => do
    compileO oFile srcFile #["-I", (← getLeanIncludeDir).toString,
                             "-I", "third_party/OpenBLASLib/include"]

--def cLibTarget (pkgDir : FilePath) : FileTarget :=
--  let libFile := pkgDir / buildDir / cDir / "libffi.a"
--  staticLibTarget libFile #[ffiOTarget]

extern_lib cLib :=
  let libFile := cBuildDir / nameToStaticLib "leanffi"
  staticLibTarget libFile #[ffiOTarget]

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

Although I plan to change it from an executable to a library tomorrow

Mac (Jul 29 2022 at 04:02):

Do you have the command line invocation that is erroring (i.e., the part starting with > .../lean...)?

z battleman (Jul 29 2022 at 04:03):

its occuring in the info window. The executables run correctly. Admittedly I don't know enough about running lean from the command line to reproduce it... sorry

Mac (Jul 29 2022 at 04:10):

@z battleman No worries, the info part helps. I didn't mean run lean directly from the command line. When you run lake build it should spit out a lot of logging which includes a the invocations of lean used to builds files (in the form > [env-vars] [cmd] [args])

z battleman (Jul 29 2022 at 04:13):

I'm not entirely sure what you're looking for in particular so here's the output

> cc -c -o ./build/c/bindings.o ./c/bindings.c -I /home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/include -I third_party/OpenBLASLib/include
> /home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/bin/llvm-ar rcs ./build/c/libleanffi.a ./build/c/bindings.o
> /home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/bin/leanc -shared -o ./build/c/libleanffi.so -Wl,--whole-archive ./build/c/libleanffi.a -Wl,--no-whole-archive
> LEAN_PATH=./third_party/mathlib/build/lib:./build/lib LD_LIBRARY_PATH=/home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/lib:./build/lib:./build/c /home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/bin/lean ./././LeanAlg/genVec.lean -R ././. -o ./build/lib/LeanAlg/genVec.olean -i ./build/lib/LeanAlg/genVec.ilean -c ./build/ir/LeanAlg/genVec.c --load-dynlib=libleanffi.so
> LEAN_PATH=./third_party/mathlib/build/lib:./build/lib LD_LIBRARY_PATH=/home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/lib:./build/lib:./build/c /home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/bin/lean ./././LeanAlg/utils/FloatUtils.lean -R ././. -o ./build/lib/LeanAlg/utils/FloatUtils.olean -i ./build/lib/LeanAlg/utils/FloatUtils.ilean -c ./build/ir/LeanAlg/utils/FloatUtils.c --load-dynlib=libleanffi.so
> /home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/bin/leanc -c -o ./build/ir/LeanAlg/utils/FloatUtils.o ./build/ir/LeanAlg/utils/FloatUtils.c -O3 -DNDEBUG
> LEAN_PATH=./third_party/mathlib/build/lib:./build/lib LD_LIBRARY_PATH=/home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/lib:./build/lib:./build/c /home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/bin/lean ./././LeanAlg/mathVec.lean -R ././. -o ./build/lib/LeanAlg/mathVec.olean -i ./build/lib/LeanAlg/mathVec.ilean -c ./build/ir/LeanAlg/mathVec.c --load-dynlib=libleanffi.so
> /home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/bin/leanc -c -o ./build/ir/LeanAlg/genVec.o ./build/ir/LeanAlg/genVec.c -O3 -DNDEBUG

> /home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/bin/leanc -c -o ./build/ir/LeanAlg/mathVec.o ./build/ir/LeanAlg/mathVec.c -O3 -DNDEBUG
> LEAN_PATH=./third_party/mathlib/build/lib:./build/lib LD_LIBRARY_PATH=/home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/lib:./build/lib:./build/c /home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/bin/lean ./././LeanAlg/mathMatrix.lean -R ././. -o ./build/lib/LeanAlg/mathMatrix.olean -i ./build/lib/LeanAlg/mathMatrix.ilean -c ./build/ir/LeanAlg/mathMatrix.c --load-dynlib=libleanffi.so
> LEAN_PATH=./third_party/mathlib/build/lib:./build/lib LD_LIBRARY_PATH=/home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/lib:./build/lib:./build/c /home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/bin/lean ./././LeanAlg/tests/mathVecTest.lean -R ././. -o ./build/lib/LeanAlg/tests/mathVecTest.olean -i ./build/lib/LeanAlg/tests/mathVecTest.ilean -c ./build/ir/LeanAlg/tests/mathVecTest.c --load-dynlib=libleanffi.so

> /home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/bin/leanc -c -o ./build/ir/LeanAlg/mathMatrix.o ./build/ir/LeanAlg/mathMatrix.c -O3 -DNDEBUG
> LEAN_PATH=./third_party/mathlib/build/lib:./build/lib LD_LIBRARY_PATH=/home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/lib:./build/lib:./build/c /home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/bin/lean ./././LeanAlg/tests/mathMatrixTest.lean -R ././. -o ./build/lib/LeanAlg/tests/mathMatrixTest.olean -i ./build/lib/LeanAlg/tests/mathMatrixTest.ilean -c ./build/ir/LeanAlg/tests/mathMatrixTest.c --load-dynlib=libleanffi.so

> /home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/bin/leanc -c -o ./build/ir/LeanAlg/tests/mathVecTest.o ./build/ir/LeanAlg/tests/mathVecTest.c -O3 -DNDEBUG
> LEAN_PATH=./third_party/mathlib/build/lib:./build/lib LD_LIBRARY_PATH=/home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/lib:./build/lib:./build/c /home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/bin/lean ./././Main.lean -R ././. -o ./build/lib/Main.olean -i ./build/lib/Main.ilean -c ./build/ir/Main.c --load-dynlib=libleanffi.so
> /home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/bin/leanc -c -o ./build/ir/LeanAlg/tests/mathMatrixTest.o ./build/ir/LeanAlg/tests/mathMatrixTest.c -O3 -DNDEBUG
> /home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/bin/leanc -c -o ./build/ir/Main.o ./build/ir/Main.c -O3 -DNDEBUG
> /home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/bin/leanc -o ./build/bin/test ./build/ir/Main.o ./build/ir/LeanAlg/genVec.o ./build/ir/LeanAlg/mathVec.o ./build/ir/LeanAlg/utils/FloatUtils.o ./build/ir/LeanAlg/mathMatrix.o ./build/ir/LeanAlg/tests/mathMatrixTest.o ./build/ir/LeanAlg/tests/mathVecTest.o ./build/c/libleanffi.a -L ./third_party/OpenBLASLib/lib -lopenblas -Wl,-R./third_party/OpenBLASLib/lib

(if you can point out whats relevant I can delete the rest to avoid clogging the thread)

Mac (Jul 29 2022 at 05:20):

Looks good to me. You mentioned that error only appears in the infoview, right?

Mac (Jul 29 2022 at 05:22):

My two suggestions:

  • You have a lean-toolchain file in your project, correct? What nightly are using?
  • If you are using VSCode, you can run try running Developer: Reload Window from the command palette and seeing if that helps.

z battleman (Jul 29 2022 at 12:27):

My lean-toolchain is nightly version 07-24-22. I use neovim with lean.nvim, but I could try vscode and see if that works. Also, to be a bit more specific, the error isnt occuring the infowindow itself, but rather my language server is detecting it and nothing is loading in the infowindow (which I think is just trying to load it into the info window, but I'm not sure if that distinction is important)

z battleman (Jul 29 2022 at 13:07):

I just checked, it's the same issue in VScode :(

(and this time officially in the info window haha)

Mac (Jul 29 2022 at 16:16):

@z battleman try running the following in your lean server environment:

#eval show IO _ from do
  let path := (← IO.getEnv "LD_LIBRARY_PATH").getD ""
  return System.SearchPath.parse path

If things are working correctly, you should see build/c in the list of paths the #eval prints.

z battleman (Jul 29 2022 at 17:41):

Its not there, I'm just getting 

[FilePath.mk "/home/zaxioms/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/lib",
 FilePath.mk "./third_party/mathlib/build/lib",
 FilePath.mk "./build/lib"]

in the ./build/lib directory are a bunch of .so files associated with the individual files, but I assume the one that its looking for "ties them all together" so to speak

Mac (Jul 29 2022 at 17:52):

@z battleman yep, that is a bug. A short term solution would be to output libleanffi to build/lib rather than build/c

z battleman (Jul 29 2022 at 17:53):

hopefully that'll work for now. Thanks!

z battleman (Jul 29 2022 at 18:10):

well it found the file, but now it says that 

libc++abi: terminating with uncaught exception of type lean::exception: could not find native implementation of external declaration 'mathMatrix.id' (symbols 'l_mathMatrix_id___boxed' or 'l_mathMatrix_id')

considering the files run at all, these defintely exist in my c code but it seems like they might not being detected by the compiler when it is compiling the so? Is this something that can happen?

Here it is in the ir directory generated

LEAN_EXPORT lean_object* l_mathMatrix_id___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = mathMatrix_new_id(x_1);
return x_2;
}

Mac (Jul 29 2022 at 18:17):

How are you calling your C code from Lean?

z battleman (Jul 29 2022 at 18:19):

just with #eval

Sebastian Ullrich (Jul 29 2022 at 18:28):

The #eval needs to be in a different file from the extern

z battleman (Jul 29 2022 at 18:35):

oh that works!! thank you so much!

Yakov Pechersky (Oct 21 2022 at 13:21):

I've hit the offline issue again, preventing offline porting, because the lakefile for mathlib4 won't parse. https://github.com/leanprover/lake/issues/104#issuecomment-1286953208

James Gallicchio (Nov 05 2022 at 20:38):

I'm having a slightly different issue from what @zbatt had; for some reason, an executable generated by lake build doesn't have libunwind.so linked correctly:

$ ldd ./build/bin/eternity2
        linux-vdso.so.1 (0x00007fffa8bd2000)
        libc++.so.1 => /usr/lib/x86_64-linux-gnu/libc++.so.1 (0x00007f4854a6b000)
        libc++abi.so.1 => /usr/lib/x86_64-linux-gnu/libc++abi.so.1 (0x00007f4854a33000)
        libunwind.so.1 => not found
        libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007f48548e4000)
        libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007f48548de000)
        libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007f48548bb000)
        libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007f48546c7000)
        librt.so.1 => /lib/x86_64-linux-gnu/librt.so.1 (0x00007f48546bd000)
        libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007f48546a2000)
        /lib64/ld-linux-x86-64.so.2 (0x00007f4857c13000)

but if I add the lean toolchain lib/ folder to the LD_LIBRARY_PATH environment variable it runs fine. i think this is also why i hadn't noticed it until now, cuz lake exe eternity2 has LD_LIBRARY_PATH set properly

James Gallicchio (Nov 05 2022 at 20:38):

obviously low priority since I can work around it right now but I'm not sure if I'm doing something weird or if this is a bug in lake

James Gallicchio (Nov 05 2022 at 20:41):

https://github.com/JamesGallicchio/eternity2/tree/8e7b7927d350467e281a674616ddb29c1578b89d leaving this commit here in case we want to debug at some point

Sebastian Ullrich (Nov 05 2022 at 22:40):

libunwind is supposed to be linked statically: https://github.com/leanprover/lean4/blob/8b9fe9b6c2714b51dc8b25c3f90304e488ec29a6/script/prepare-llvm-linux.sh#L60. But your additional linker flags may have affected that in some way

James Gallicchio (Nov 05 2022 at 23:39):

hrm, interesting

James Gallicchio (Nov 05 2022 at 23:41):

oh, wait, I had a lingering -lstdlib++ in my linker args, seems to work now

James Gallicchio (Nov 05 2022 at 23:41):

sorry for the noise!

Last updated: Dec 20 2023 at 11:08 UTC