doc-gen4 package name & lakefile parsing

Stream: lean4

[Henrik Böving]

The package name was mainly chosen like this to reflect the doc-gen naming from Lean 3, also the french brackets are general lean sytnax for making stuff that can usually not be an identifier an identifier so that's the reason lake generated the project this way. If you have an alternative idea feel free, I don't think we have really agreed upon a naming scheme for packages though? So we should probably do that.

Did you actually build this with lake build or just in the server? For me when I try to build software with lake build it will actually inform me that I imported a package as xy but it found yz in the directory, at least when I last made this mistake.

this also answers question 3 i guess? At least there is a check for this right now

[Henrik Böving]

Also doc-gen4 is not really meant to be used as a dependency in this way, my hope was that it would eventually be shipped with a lean install and maybe even as a lake subcommand.

[Arthur Paulino]

I didn't build it with lake build. I just cloned the repo, opened it with VS Code and every Lean file had a red bar with that error message.

If doc-gen4 won't be meant to be used as a dependency like that, then the package name doesn't matter much.

The error message from lake build indeed helps (and it has helped me in the past), but the error message that I got without building, just from opening the project, ended up getting me confused.

Question 3 wasn't fully answered because I was thinking about not needing to provide the name attribute at all. You'd just provide the src attribute because the package name can be inferred from its respective lakefile.lean.

[Mario Carneiro]

As a point of comparison, Rust uses crates which are often named with hyphens, but the hyphens are transposed to underscore when referencing them in code so that the french quotes aren't necessary