Zulip Chat Archive

Stream: lean4

Topic: lake linkArgs

Scott Morrison (Oct 13 2021 at 01:18):

@Mac, apparently lake no longer supports linkArgs:

./lakefile.lean:12:2: error: 'linkArgs' is not a field of structure 'Lake.PackageConfig'

Do you know what I should do to adapt? The current lakefile.lean (for mathport) says:

import Lake

open Lake DSL System

package mathport {
  dependencies := #[{
    name := "mathlib",
    src := Source.git "https://github.com/semorrison/mathlib4.git" "lake" none,
    dir := FilePath.mk "."
  }],
  binRoot := `MathportApp
  linkArgs := #["-rdynamic"]
}

Scott Morrison (Oct 13 2021 at 01:20):

Ah, renamed to moreLinkArgs. https://github.com/leanprover/lake/commit/211e1dc56c453675047f5ac8d1030eb8c8e3fa3e#diff-b335630551682c19a781afebcf4d07bf978fb1f8ac04c6bf87428ed5106870f5R110

Mac (Oct 13 2021 at 01:27):

@Scott Morrison ah, yeah, sorry about that, but I wanted to make the name more semantically correct (and consistent with things like moreLibTargets)

Scott Morrison (Oct 13 2021 at 01:27):

All good. Everything is moving fast at the moment. :-)

Mac (Oct 13 2021 at 01:29):

@Scott Morrison since we are on the topic of mathport's link args setting iit really should be:

moreLinkArgs :=
  if Platform.isWindows then
    #["-Wl,--export-all"]
  else
    #["-rdynamic"]

so that it also works on Windows (like Lake's own lakefile.lean)

Sebastian Ullrich (Oct 13 2021 at 07:24):

Could maybe be a convenience function like |>.enableInterpreter?

Sebastian Ullrich (Oct 13 2021 at 07:30):

The Nix setup for example has withSharedStdlib (which specifically might or might not be interesting for users as well) https://github.com/leanprover/lean4/blob/66fcfcce3716774dacbd35e1ea0f5c75356df311/nix/bootstrap.nix#L114

Sebastian Ullrich (Oct 13 2021 at 07:30):

(It's really enableInterpreterToCallFunctionsCompiledIntoThisExecutable)

Mac (Oct 13 2021 at 09:06):

@Sebastian Ullrich I think I will definitely need a shorter name than that if I am to implement this. :stuck_out_tongue_wink:

Mac (Oct 13 2021 at 09:07):

sadly, it is very true that what is does is not really easy to capture in a concise manner (a least I haven't thought of such a way yet)

Sebastian Ullrich (Oct 23 2021 at 13:26):

PSA: --export-all is not needed anymore since leanprover/lean4#670. Worse, it seems to be an undocumented, GNU ld-specific alias of --export-all-symbols, so packages specifying it will not work with leanprover/lean4#736. Please remove it from your packages!

Mac (Oct 23 2021 at 19:17):

@Sebastian Ullrich -rdynamic is still needed though on non-Windows systems, correct?

Sebastian Ullrich (Oct 23 2021 at 20:05):

Correct, populating the dynamic symbol table is independent from symbol visibility with ELF/MachO

Scott Morrison (Oct 25 2021 at 23:03):

I've removed --export-all from mathport at https://github.com/leanprover/mathport/pull/37.

Last updated: Dec 20 2023 at 11:08 UTC