Zulip Chat Archive

Stream: new members

Topic: file encoding

Michael Beeson (Jul 11 2021 at 17:10):

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 (Jul 11 2021 at 17:11):

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

Michael Beeson (Jul 11 2021 at 17:21):

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 (Jul 11 2021 at 17:22):

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 (Jul 11 2021 at 17:32):

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

Eric Wieser (Jul 11 2021 at 17:33):

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

Eric Wieser (Jul 11 2021 at 17:33):

At least in terms of the grammar of the grammar files

Michael Beeson (Jul 13 2021 at 04:13):

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 (Jul 13 2021 at 04:43):

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

Anne Baanen (Jul 13 2021 at 09:17):

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

Last updated: Dec 20 2023 at 11:08 UTC