lake build not building dependency binary

Stream: lean4

[Arthur Paulino]

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]

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]

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]

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

[Mac]

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]

So I need to do lake build lspec instead?

[Arthur Paulino]

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]

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]

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]

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