file encoding

Stream: new members

[Michael Beeson]

If I open one of my .lean files in TextMate (a text editor, which one probably not relevant), then I see some Japanese-looking characters
where in Lean I see some nice mathematical characters (which I typed in by \N or \F, etc.) TextMate offers me to "re-open with encoding..." and offers numerous options; e.g. UTF-8, and several more. But none of them make it appear as it does in Lean. I would like to be able to see it in TextMate as I see it in Lean. So the actual question is, what encoding is VSCode using to display my Lean files?

[Patrick Massot]

It sounds more like a font issue than an encoding issue.

[Michael Beeson]

well, since it displays fine in VSCode, the necessary fonts are present on my machine. So your suggestion is that TextMate and VSCode choose different fonts to render a certain byte in UTF-8?

[Patrick Massot]

I don't know what is TextMate but I don't see why any editor would feel the need to use the same font as what you asked VSCode to use.

[Eric Wieser]

Mathlib files are UTF-8, and I assume lean itself requires that.

[Eric Wieser]

TextMate is the common ancestor of the syntax highlighter used by sublime / atom / vscode.

[Eric Wieser]

At least in terms of the grammar of the grammar files

[Michael Beeson]

OK, here is a different but related question. I copy a few lines of Lean from my Lean file. It contains some Unicode characters. I paste it into a LaTeX file between \begin{verbatim} and \end{verbatim}. What package and package options will enable this to work? I tried
\usepackage[latin9, utf8]{inputenc} and some variations on that without success. I'm using TeXShop on the mac.
Surely I'm not the first person to try this.

[Michael Beeson]

Oh. All you have to do is choose "XeLateX" from the TeXShop "Typeset with" menu. Well, not quite. Quantifiers do not render.

[Anne Baanen]

In the Lean repository we have a lstlean.tex file for typesetting Lean code. See lstlean.md for more instructions.