Latex

Stream: general

[Billy Price]

I'm trying to format something in latex - but some unicode characters don't render and some are out of order. I'm rendering with xelatex like this xelatex --shell-escape file.tex.

\begin{adjustbox}{max width=\textwidth}
\begin{lstlisting}
inductive proof : context → term → term → Prop
| axm        {Γ} {φ}       : WF Γ Ω φ → proof Γ φ φ
| vac        {Γ} {φ}       : WF Γ Ω φ → proof Γ φ ⊤
| abs        {Γ} {φ}       : WF Γ Ω φ → proof Γ ⊥ φ
| and_intro  {Γ} {p q r}   : proof Γ p q → proof Γ p r → proof Γ p (q ⋀ r)
| and_left   {Γ} (p q r)   : proof Γ p (q ⋀ r) → proof Γ p q
| and_right  {Γ} (p q r)   : proof Γ p (q ⋀ r) → proof Γ p r
| or_intro   {Γ} {p q r}   : proof Γ p r → proof Γ q r → proof Γ (p ⋁ q) r
| or_left    {Γ} (p q r)   : proof Γ (p ⋁ q) r → proof Γ p r
| or_right   {Γ} (p q r)   : proof Γ (p ⋁ q) r → proof Γ q r
| imp_to_and {Γ} {p q r}   : proof Γ p (q ⟹ r) → proof Γ (p ⋀ q) r
| and_to_imp {Γ} {p q r}   : proof Γ (p ⋀ q) r → proof Γ p (q ⟹ r)
| weakening  {Γ} {φ ψ Δ}   : proof Γ φ ψ → proof (list.append Γ Δ) φ ψ
| cut        {Γ} (φ c ψ)   : proof Γ φ c → proof Γ c ψ → proof Γ φ ψ
| all_elim   {Γ} {p φ A}   : proof Γ p (∀' A φ) → proof (A::Γ) p φ
| all_intro  {Γ} {p φ} (A) : proof (A::Γ) p φ → proof Γ p (∀' A φ)
| ex_elim    {Γ} {p φ A}   : proof Γ p (∃' A φ) → proof (A::Γ) p φ
| ex_intro   {Γ} {p φ} (A) : proof (A::Γ) p φ → proof Γ p (∃' A φ)
| extensionality {A}       : proof [] ⊤ $ ∀' (𝒫 A) $ ∀' (𝒫 A) $ (∀' A ((𝟘 ∈ 𝟚) ⇔ (𝟘 ∈ 𝟙))) ⟹ (𝟚 ≃[A] 𝟙)
| prop_ext                 : proof [] ⊤ $ ∀' Ω $ ∀' Ω (𝟙 ⇔ 𝟘) ⟹ (𝟙 ≃[Ω] 𝟘)
| star_unique              : proof [] ⊤ $ ∀' Unit (𝟘 ≃[Unit] ⁎)
| pair_exists_rep {A B}    : proof [] ⊤ $ ∀' (A ×× B) $ ∃' A $ ∃' B $ 𝟚 ≃[A ×× B] ⟪𝟙,𝟘⟫
| pair_distinct_rep {A B}  : proof [] ⊤ $ ∀' A $ ∀' B $ ∀' A $ ∀' B $ (⟪𝟛,𝟙⟫ ≃[A××B] ⟪𝟚,𝟘⟫) ⟹ (𝟛 ≃[A] 𝟚 ⋀ 𝟙 ≃[B] 𝟘)
| sub      {Γ} (B) (φ ψ b) : WF Γ B b → proof (B::Γ) φ ψ → proof Γ (⁅φ // b⁆) (⁅ψ // b⁆)
| comp     {Γ} (A) (φ)     : WF (A::Γ) Ω φ → proof Γ ⊤ (∀' A (𝟘 ∈ ⟦A | φ⟧) ⇔ (⁅φ // 𝟘⁆))
\end{lstlisting}
\end{adjustbox}

image.png

[Chris Hughes]

Are you using the lstlean file?

[Chris Hughes]

There's a list of symbols in that file, if things don't display correctly after using lstlean, then you can add to the list of symbols.

[Billy Price]

Yes I am. phi is already in that file, and that's the first symbol to not show up

[Kevin Buzzard]

Those 's are not the best either

[Billy Price]

In fact I just went back to compiling the sample.tex file provided there and even that's missing unicode symbols. There seems to be no complaint in the log

[Billy Price]

Actually there is a warning "Package inputenc Warning: inputenc package ignored with utf8 based engines."

[Billy Price]

Is there a recommended way to compile tex files that use lstlean? I'm using XeLaTeX because I read it was necessary for unicode characters, but I'm realising this might be the problem.

[Sebastian Ullrich]

IIRC listings has some issues with Unicode even on other Latex engines(?). I always use minted with Luatex for my talks.

% https://tex.stackexchange.com/questions/343494/minted-red-box-around-greek-characters
\makeatletter
\AtBeginEnvironment{minted}{\dontdofcolorbox}
\def\dontdofcolorbox{\renewcommand\fcolorbox[4][]{##4}}
\makeatother

[Alexandre Rademaker]

Hi @Sebastian Ullrich , have you use minted with beamer? any sample I can see?

[Sebastian Ullrich]

@Alexandre Rademaker Nothing beamer-specific, but I recently documented everything I know in https://leanprover.github.io/lean4/doc/syntax_highlight_in_latex.html