latex help

Stream: general

[Alexandre Rademaker]

I am getting an error below with French quotes in a beamer presentation. Actually, I was not able to make the \mid for definitions using pattern matching working too. I am using the code from https://github.com/leanprover-community/lean/tree/master/extras/latex.

ERROR: LaTeX Error: Command \guilsinglleft unavailable in encoding OT1.

--- TeX said ---

See the LaTeX manual or LaTeX Companion for explanation.
Type  H <return>  for immediate help.
 ...

l.10   (assume : B, show B, from ‹
                                    B›)

any idea?

[Rob Lewis]

This is impossible to diagnose without the full tex file and maybe your tex setup, but see https://tex.stackexchange.com/questions/35451/using-inputenc-package-for-cp1252-encoding and check your inputenc/font settings maybe?

[Rob Lewis]

I just tried that symbol in a couple files and it worked, so it's not a limitation of lstlean.tex

[Alexandre Rademaker]

Hi @Rob Lewis , now I got the french quotes but they are displayed before the argument, like ‹›B. My preambule is like

\documentclass{beamer}

\usepackage[utf8x]{inputenc}
\usepackage[LGR,T1]{fontenc}
% \usepackage{lmodern}

\usepackage{fancybox}
\usepackage{url}
\usepackage{multirow}
\usepackage[makeroom]{cancel}
\usepackage{ulem}
\usepackage{ifthen}
\usepackage{pgf}
% \usepackage{times}
% \usepackage[T1]{fontenc}
\usepackage{amsthm,amsmath}
\usepackage{etex}
\usepackage{ulem}
\usepackage{tabularx}
\usepackage{listings}
\usepackage{bussproofs}

\usepackage{cmap}
% \usepackage{fontspec}

\usepackage[Bjarne]{fncychap}

\usepackage{../latex/unixode}
\usepackage{../latex/mylogic}


\usepackage{tikz}
\usetikzlibrary{shapes,backgrounds,arrows,automata,positioning,calc}
\tikzset{
  modal/.style={>=stealth',shorten >=1pt,shorten <=1pt,auto,node distance=1.5cm,
    semithick},
  world/.style={circle,draw,minimum size=0.5cm,fill=gray!15},
  point/.style={circle,draw,inner sep=0.5mm,fill=black},
  reflexive above/.style={->,loop,looseness=7,in=120,out=60},
  reflexive below/.style={->,loop,looseness=7,in=240,out=300},
  reflexive left/.style={->,loop,looseness=7,in=150,out=210},
  reflexive right/.style={->,loop,looseness=7,in=30,out=330}
}


\hypersetup{
    colorlinks=true,
    linkcolor=blue,
    filecolor=magenta,
    urlcolor=cyan}

\lstdefinelanguage{plist}{
  columns=fullflexible,
  upquote=true,
  basicstyle=\rmfamily,
  commentstyle=\ttfamily\itshape\color{green!50!black},
  morestring=[s]{"}{"},
  stringstyle=\color{blue},
  keywords={:pos,:tokens,\:gloss},
  inputencoding=utf8,
  keywordstyle=\bfseries\color{violet}}

\definecolor{ceruleanblue}{rgb}{0.16, 0.32, 0.75}

\usepackage{color}
\definecolor{keywordcolor}{rgb}{0.7, 0.1, 0.1}   % red
\definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4}   % grey
\definecolor{symbolcolor}{rgb}{0.0, 0.1, 0.6}    % blue
\definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1}      % green
\definecolor{errorcolor}{rgb}{1, 0, 0}           % bright red
\definecolor{stringcolor}{rgb}{0.5, 0.3, 0.2}    % brown

\usepackage{listings}
\def\lstlanguagefiles{../latex/lstlean.tex}
\lstset{language=lean}

\title{Dedução Natural de LP em Lean \\ Matemática Discreta}
\author{Alexandre Rademaker}

\newcommand{\rl}[1]{\RightLabel{\small #1}}

\begin{document}
...
\end{document}

[Rob Lewis]

Oh, they're missing from lstlean.tex completely. Add these lines somewhere in the middle of lstlean.tex:

{‹}{{\guilsinglleft}}1
{›}{{\guilsinglright}}1

[Alexandre Rademaker]

Rob Lewis said:

This is impossible to diagnose without the full tex file and maybe your tex setup, but see https://tex.stackexchange.com/questions/35451/using-inputenc-package-for-cp1252-encoding and check your inputenc/font settings maybe?

If you give me your github username I can give you access to the repo with the full latex code...

[Alexandre Rademaker]

Perfect!! It worked!! Wonderful! Thank you so much!

[Alexandre Rademaker]

Hi @Rob Lewis , it looks like the command https://github.com/leanprover-community/lean/blob/master/extras/latex/sample.tex#L15 makes listlisting environment in the document ONLY accepting Lean. I want to mix Lean and Haskell code in the same document, that is, having environments with language=Haskell and environments with language=Lean. Any idea how to make it happen?

[Sebastian Ullrich]

\begin{lstlisting}[language=Haskell]

[Alexandre Rademaker]

I didn’t work. The error says that Haskell is not a valid language.

[Sebastian Ullrich]

Then I guess it's haskell

[Alexandre Rademaker]

No I also tried it

[Alexandre Rademaker]

But I moved to minted

[Fangming Li (John)]

Hello! Right now I am writing a report. I want to enter the symbol ⨆ in the report but failed. Is there any method to enter this symbol?

[Shreyas Srinivas]

In math mode the symbol is \sqcup

[Jireh Loreaux]

Do you want it as a unicode symbol for inclusion in a code block? In that case, using LuaLaTeX with an appropriate font is likely what you want to do instead.

[Floris van Doorn]

In pdflatex I used \bigsqcup in the package MnSymbol. (The package stmaryrd also has it, but is ugly/wrong)

[Kevin Buzzard]

@FMLJohn if you just want to quote lean code in latex then you can cut and paste it directly and use minted.

[Jireh Loreaux]

You still need to use a font that includes the glyphs you need though.

[Shreyas Srinivas]

For code listings you could try this : https://tex.stackexchange.com/questions/63729/how-to-use-mathematical-symbols-in-listing

[Fangming Li (John)]

Shreyas Srinivas said:

For code listings you could try this : https://tex.stackexchange.com/questions/63729/how-to-use-mathematical-symbols-in-listing

Yeah I am using code listings, and it works! Thank you so much!

[Fangming Li (John)]

Thank you all!

[Shreyas Srinivas]

One disadvantage with my suggestion is that it will render the math parts in the math font which might differ from what your lean code looks like.

[Fangming Li (John)]

Oh I see the issue. Is there any way to use code listing and at the same time avoid the issue?

[Shreyas Srinivas]

Jireh's suggestion is ideal

[Eric Wieser]

One downside of LuaLatex is that arXiv doesn't accept it, but you can fix that by mangling the resulting PDF a little (renaming its fonts!) to thwart its LaTeX detection

[Fangming Li (John)]

I have managed to enter the symbol as a unicode symbol, without using mathmode.

[Kevin Buzzard]

That arxiv hack had been announced on the Xena Discord some time ago but now it's out in the open!