Zulip Chat Archive

Stream: lean4

Topic: lake build not building dependency binary


Arthur Paulino (Jul 11 2022 at 22:38):

Hello!

I'm trying to build a dependency (LSpec) with lake build LSpec and almost everything seems to work nicely.

The problem I'm facing is that the lspec binary is not being generated and the next step is failing, as you can see here.

Both repos use today's toolchain (2022-07-11)

Is there something else I need to do on the LSpec repo for this to work? Thanks in advance!!

Mac (Jul 12 2022 at 03:25):

According to the yatima-inc/LSpec repository , the executable is name lspec while the library is named LSpec so it is building the library rather than the executable.

Mac (Jul 12 2022 at 03:29):

Or were you trying to build the package LSpec? If so, then you need and @ to disambiguate it (i.e., lake build @LSpec). Lake resolves targets in the order of custom target, executable, external library, lean library, package, and them module (see here). Package and modules are last because they can be disambiguated with @ and +, respectively (as mentioned in lake help build).

Mac (Jul 12 2022 at 03:31):

Actually, now that I think about it a bit more, pkg/ would be alternative, potentially more intuitive way to disambiguate package names.

Mac (Jul 12 2022 at 03:33):

That way I could use @ for modules and remove + which I personally have never liked (it was only non-special character left in shell that I could think of at the time).

Arthur Paulino (Jul 12 2022 at 03:39):

So I need to do lake build lspec instead?

Arthur Paulino (Jul 12 2022 at 03:41):

A honest piece of feedback: I don't understand the difference between "package" and "library" according to Lake. I've seen a message saying that Package is deprecated, but then I tried removing it and the code no longer compiled.

I don't think Lake's readme is didactic enough

Mac (Jul 12 2022 at 03:50):

Arthur Paulino said:

A honest piece of feedback: I don't understand the difference between "package" and "library" according to Lake. I've seen a message saying that Package is deprecated, but then I tried removing it and the code no longer compiled

Ah, this Lake's package vs lean_lib vs lean_exe thread by Yuri de Wit may help. I explained that deprecation message here and discussed the package and workspace terminology of Lake here and connected the concept of Lake library to its parallel in Racket here. I really do need to add a glossary to Lake's README.

Arthur Paulino (Jul 12 2022 at 04:05):

Thank you!
I will read that thread tomorrow. If I find the opportunity, I might also PR some pieces of information I find important (it you don't cover them first)

Mac (Jul 12 2022 at 05:44):

Added a Glossary of Terms to Lake's README. Feel free to suggest improvements!


Last updated: Dec 20 2023 at 11:08 UTC