[Agda] Disappearing unicode in Literate Agda - XeLatex

[Andreas Abel]

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

How did \bN become a lambda?

On 30.12.2017 20:39, Matthew Daggitt wrote:
> 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
> 
> 
> On Sat, Dec 30, 2017 at 5:15 PM, Nils Anders Danielsson <nad at cse.gu.se 
> <mailto:nad at cse.gu.se>> wrote:
> 
>     On 2017-12-30 14:47, Matthew Daggitt wrote:
> 
>         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
>     <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.)
> 
>     -- 
>     /NAD
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/