[Agda] Disappearing unicode in Literate Agda - XeLatex

[Matthew Daggitt]

I've been trying to get literate agda up and running as per the
instructions in the documentation
<https://agda.readthedocs.io/en/v2.5.3/tools/generating-latex.html>
and I'm having problems getting unicode symbols to appear inside code
blocks. I've run "agda --latex code.lagda" to get the following
"code.tex" file below .



\documentclass{article}



\usepackage{agda}



\begin{document}



ℕ



\begin{code}%

%

\>[4]\AgdaKeyword{data}\AgdaSpace{}%

\AgdaDatatype{ℕ}\AgdaSpace{}%

\AgdaSymbol{:}\AgdaSpace{}%

\AgdaPrimitiveType{Set}\AgdaSpace{}%

\AgdaKeyword{where}\<%

\end{code}



\end{document}

When I compile it using XeLatex (or LuaLatex) everything compiles without
errors and it all appears fine (including the first ℕ symbol outside of the
code block) except that the ℕ symbol inside the \AgdaDatatype{} command
doesn't appear. The same problem occurs when I place any unicode character
inside the \AgdaDatatype{} command. I've tried adding in various
combinations of the following package imports (even though according to the
documentation they shouldn't be necessary in XeLatex):

\usepackage{bbm}

\usepackage[greek,english]{babel}

\usepackage{ucs}

\usepackage[utf8x]{inputenc}

\usepackage{autofe}

Does anyone have any suggestions?

Thanks,
Matthew

[Andrés Sicard-Ramírez]

Agda, XeLaTeX and LuaLaTeX versions?

Also attach `code.lagda` please.

I've been trying to get literate agda up and running as per the instructions
in the documentation and I'm having problems getting unicode symbols to
appear inside code blocks. I've run "agda --latex code.lagda" to get the
following "code.tex" file below .
\documentclass{article}
\usepackage{agda}
\begin{document}
ℕ
\begin{code}%
%
\>[4]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaDatatype{ℕ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\end{code}
\end{document}
When I compile it using XeLatex (or LuaLatex) everything compiles without
errors and it all appears fine (including the first ℕ symbol outside of the
code block) except that the ℕ symbol inside the \AgdaDatatype{} command
doesn't appear. The same problem occurs when I place any unicode character
inside the \AgdaDatatype{} command. I've tried adding in various
combinations of the following package imports (even though according to the
\usepackage{bbm}
\usepackage[greek,english]{babel}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{autofe}
Does anyone have any suggestions?
Thanks,
Matthew
La información contenida en este correo electrónico está dirigida únicamente
a su destinatario y puede contener información confidencial, material
privilegiado o información protegida por derecho de autor. Está prohibida
cualquier copia, utilización, indebida retención, modificación, difusión,
distribución o reproducción total o parcial. Si usted recibe este mensaje
por error, por favor contacte al remitente y elimínelo. La información aquí
contenida es responsabilidad exclusiva de su remitente por lo tanto la
Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The
information contained in this email is addressed to its recipient only and
may contain confidential information, privileged material or information
protected by copyright. Its prohibited any copy, use, improper retention,
modification, dissemination, distribution or total or partial reproduction.
If you receive this message by error, please contact the sender and delete
it. The information contained herein is the sole responsibility of the
sender therefore Universidad EAFIT is not responsible for what the message
contains.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

--
Andrés
La información contenida en este correo electrónico está dirigida únicamente a su destinatario y puede contener información confidencial, material privilegiado o información protegida por derecho de autor. Está prohibida cualquier copia, utilización, indebida retención, modificación, difusión, distribución o reproducción total o parcial. Si usted recibe este mensaje por error, por favor contacte al remitente y elimínelo. La información aquí contenida es responsabilidad exclusiva de su remitente por lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The information contained in this email is addressed to its recipient only and may contain confidential information, privileged material or information protected by copyright. Its prohibited any copy, use, improper retention, modification, dissemination, distribution or total or partial reproduction. If you receive this message by error, please contact the sender and delete it. The information contained herein is the sole responsibility of the sender therefore Universidad EAFIT is not responsible for what the message contains.

[Nils Anders Danielsson]

Post by Matthew Daggitt
When I compile it using XeLatex (or LuaLatex) everything compiles
without errors and it all appears fine (including the first ℕ symbol
outside of the code block) except that the ℕ symbol inside the
\AgdaDatatype{} command doesn't appear.

This is a known problem:

LaTeX backend + XeLaTeX/LuaLaTeX ⇒ no lambda
https://github.com/agda/agda/issues/2225

I assume that the output from XeLaTeX includes something like the
following:

Missing character: There is no ℕ in font cmss10!

This can be handled in different ways. I've used newunicodechar, but
this solution does not play well together with microtype, which is used
by acmart. For my latest paper I decided to use pdfLaTeX instead. (I
used \DeclareUnicodeCharacter, and gave the nofontsetup and
noinputencodingsetup options to agda.sty.)

[Matthew Daggitt]

Thank you very much for the link to the issue. I'm only trying to typeset a
small amount so the \newunicodechar workaround is fine for now. It might be
worth splicing it into the documentation as it seems it's been open for a
while.

I am getting slightly different symptoms as I'm getting no errors at all in
the log, so there is no

Missing character: There is no ℕ in font cmss10!

error appearing. My code.lagda file is as follows:

\documentclass{article}

\usepackage{agda}


\begin{document}


\begin{code}

data ℕ : Set where

\end{code}


\end{document}


And my code.tex is file is:


\documentclass{article}

\usepackage{agda}

\begin{document}

\begin{code}%

%

\>[4]\AgdaKeyword{data}\AgdaSpace{}%

\AgdaDatatype{λ}\AgdaSpace{}%

\AgdaSymbol{:}\AgdaSpace{}%

\AgdaPrimitiveType{Set}\AgdaSpace{}%

\AgdaKeyword{where}\<%

\end{code}


\end{document}


My tex version is:

XeTeX 3.14159265-2.6-0.99992 (TeX Live 2015/Debian)
kpathsea version 6.2.1

Post by Matthew Daggitt
When I compile it using XeLatex (or LuaLatex) everything compiles
without errors and it all appears fine (including the first ℕ symbol
outside of the code block) except that the ℕ symbol inside the
\AgdaDatatype{} command doesn't appear.

LaTeX backend + XeLaTeX/LuaLaTeX ⇒ no lambda
https://github.com/agda/agda/issues/2225
I assume that the output from XeLaTeX includes something like the
Missing character: There is no ℕ in font cmss10!
This can be handled in different ways. I've used newunicodechar, but
this solution does not play well together with microtype, which is used
by acmart. For my latest paper I decided to use pdfLaTeX instead. (I
used \DeclareUnicodeCharacter, and gave the nofontsetup and
noinputencodingsetup options to agda.sty.)
--
/NAD

[Andreas Abel]

data ℕ : Set where
\AgdaDatatype{λ}\AgdaSpace{}%

How did \bN become a lambda?

Thank you very much for the link to the issue. I'm only trying to
typeset a small amount so the \newunicodechar workaround is fine for
now. It might be worth splicing it into the documentation as it seems
it's been open for a while.
I am getting slightly different symptoms as I'm getting no errors at all
in the log, so there is no
  Missing character: There is no ℕ in font cmss10!
\documentclass{article}
\usepackage{agda}
\begin{document}
\begin{code}
data ℕ : Set where
\end{code}
\end{document}
\documentclass{article}
\usepackage{agda}
\begin{document}
\begin{code}%
%
\>[4]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaDatatype{λ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\end{code}
\end{document}
XeTeX 3.14159265-2.6-0.99992 (TeX Live 2015/Debian) kpathsea version 6.2.1
When I compile it using XeLatex (or LuaLatex) everything compiles
without errors and it all appears fine (including the first ℕ symbol
outside of the code block) except that the ℕ symbol inside the
\AgdaDatatype{} command doesn't appear.
  LaTeX backend + XeLaTeX/LuaLaTeX ⇒ no lambda
https://github.com/agda/agda/issues/2225
<https://github.com/agda/agda/issues/2225>
I assume that the output from XeLaTeX includes something like the
  Missing character: There is no ℕ in font cmss10!
This can be handled in different ways. I've used newunicodechar, but
this solution does not play well together with microtype, which is used
by acmart. For my latest paper I decided to use pdfLaTeX instead. (I
used \DeclareUnicodeCharacter, and gave the nofontsetup and
noinputencodingsetup options to agda.sty.)
--
/NAD
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Andrés Sicard-Ramírez]

Post by Matthew Daggitt
I am getting slightly different symptoms as I'm getting no errors at all in
the log, so there is no
Missing character: There is no ℕ in font cmss10!
\documentclass{article}
\usepackage{agda}
\begin{document}
\begin{code}
data ℕ : Set where
\end{code}
\end{document}
XeTeX 3.14159265-2.6-0.99992 (TeX Live 2015/Debian)
kpathsea version 6.2.1

Using the same version of XeLaTeX (but not installed via Debian)

$ xelatex --version
XeTeX 3.14159265-2.6-0.99992 (TeX Live 2015)
kpathsea version 6.2.1

I see the missing character warning:

$ grep Missing code.log
Missing character: There is no ℕ in font cmss10!
Missing character: There is no ℕ in font cmss10!
Missing character: There is no ℕ in font cmss10!

--
Andrés
La información contenida en este correo electrónico está dirigida únicamente a su destinatario y puede contener información confidencial, material privilegiado o información protegida por derecho de autor. Está prohibida cualquier copia, utilización, indebida retención, modificación, difusión, distribución o reproducción total o parcial. Si usted recibe este mensaje por error, por favor contacte al remitente y elimínelo. La información aquí contenida es responsabilidad exclusiva de su remitente por lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The information contained in this email is addressed to its recipient only and may contain confidential information, privileged material or information protected by copyright. Its prohibited any copy, use, improper retention, modification, dissemination, distribution or total or partial reproduction. If you receive this message by error, please contact the sender and delete it. The information contained herein is the sole responsibility of the sender therefore Universidad EAFIT is not responsible for what the message contains.