Warn or fail when creating packages with invalid names

[thorimur]

Although an experienced Lean user will know to simply not name packages incorrectly, a new one might choose to name a package e.g. "meta" with lake init meta, then be surprised when the lakefile produces errors like "expected identifier" upon building.

Of course, this is not the most pressing issue, but eventually it would be nice to make sure that all runs of lake init that do not warn or fail do produce valid packages.