leanprover
`lake init` should not write imports with French quotes unnecessarily.
lake init foo creates Foo.lean containing import «Foo».Basic, which is quite confusing, and unnecessary.
Could we avoid confusing new users and teaching them unhelpful habits by not using French quotes unless necessary.
Relatedly, lakefile.lean is populated with unnecessary French quotes in package and lean_lib.
@semorrison The French quotes in the imports can probably be removed because Lean does not parse keywords in import statements. In the Lake configuration file, however, it is not possible to know whether the names are keywords. This was the source of a previous bug (lake#128) which was the reason for introducing the French quotes.
What is the origin of this impossibility? Can't we just use a fixed blacklist? Or do a "practice run" without the French quotes and check dynamically?
@semorrison Lean/Lake does add new keywords as time progresses and those new keywords would then break packages with those names. A possibly better solution (which was part of #3174) is to allow the specification of these names as strings. This way we do not have to worry about keywords at all.