Zulip Chat Archive

Stream: general

Topic: Latex


view this post on Zulip 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

view this post on Zulip Chris Hughes (Jun 18 2020 at 05:56):

Are you using the lstlean file?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 18 2020 at 06:54):

Those 's are not the best either

view this post on Zulip 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

view this post on Zulip Billy Price (Jun 18 2020 at 06:58):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Alexandre Rademaker (Feb 10 2021 at 23:37):

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

view this post on Zulip 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: May 13 2021 at 18:26 UTC