[Agda] Disappearing unicode in Literate Agda - XeLatex

[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


On Sat, Dec 30, 2017 at 5:15 PM, Nils Anders Danielsson <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
>
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20171230/259a4bb6/attachment-0001.html>