Rendering of `\varphi` and `\phi` in Lean files

I raised a question to @kim-em today about why \varphi renders like ϕ and \phi renders like φ in Lean files opened in vscode, which was the opposite of what I was anticipating. After a web search, apparently this is or was valid Greek, but it is inconsistent with the way LaTeX renders $\varphi$ like φ and renders $\phi$ like ϕ. According to this StackOverflow answer, Knuth made that decision, so I guess it is a question of whether Lean should adhere to LaTeX conventions? It would change the way some existing Lean files look, so I would understand if there was reluctance to change it at this point. The symbols that vscode uses with Lean files are defined here .

Start with lean4-unicode-input/src/abbreviations.json and inspect the entries for \varphi and \phi. Review how the VS Code extension consumes these abbreviations and consider the compatibility impact described in the issue; done means an agreed mapping is reflected and its behavior is verified.