doc-gen4 package name

Stream: lean4

[Arthur Paulino]

I was helping @Joseph O with his Hangman package and Lean was complaining about a badly formatted lakefile.lean:

`/home/arthur/.elan/toolchains/leanprover--lean4---nightly-2022-03-06/bin/lake print-paths Init` failed:

stderr:
Error parsing './lakefile.lean'.  Please restart the lean server after fixing the Lake configuration file.

Turns out the error was because he added the doc-gen4 dependency named as docgen4. Changing it to «doc-gen4» solved the issue. However, I thought about three things:

• The current doc-gen4 package name with french brackets and a dash isn't very straightforward (just my opinion)
• The error message was pretty misleading, making me think there was something wrong with the formatting when the error was just a misspelled package name
• Would it be nice if the package name were inferred instead of inputted manually?