Zulip Chat Archive

Stream: general

Topic: Latex


Billy Price (Jun 18 2020 at 03:34):

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 (Jun 18 2020 at 05:56):

Are you using the lstlean file?

Chris Hughes (Jun 18 2020 at 05:58):

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 (Jun 18 2020 at 06:52):

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

Kevin Buzzard (Jun 18 2020 at 06:54):

Those 's are not the best either

Billy Price (Jun 18 2020 at 06:58):

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 (Jun 18 2020 at 06:58):

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

Billy Price (Jun 18 2020 at 07:08):

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 (Jun 18 2020 at 07:53):

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 (Feb 10 2021 at 23:37):

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

Sebastian Ullrich (Feb 11 2021 at 08:24):

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


Last updated: Dec 20 2023 at 11:08 UTC