How to debug missing unicode characters errors when compiling literate agda files?

409 views Asked by At

How does one get certain unicode characters to compile with .lagda files. For instance, when I add certain unicode characters manually to the tex file, like \phi, \forall, etc. but when I add < or == it yields the below error. Should I change font packages? Are there any repositories with example .lagda files, relevantly installed font packages, and commands so that I can get it to work out of the box for say, anything written in the standard library? I'm following the exact instructions for ad hoc workarounds on

https://agda.readthedocs.io/en/v2.6.1.1/tools/generating-latex.html

Here is the relevant clipping from my main.tex

\usepackage{unicode-math}
\setmathfont{XITS Math}

\usepackage{newunicodechar}
\newunicodechar{λ}{\ensuremath{\mathnormal\lambda}}
\newunicodechar{ℓ}{\ensuremath{\mathnormal\ell}}
\newunicodechar{η}{\ensuremath{\mathnormal\eta}}
\newunicodechar{∀}{\ensuremath{\mathnormal\forall}}
\newunicodechar{ϕ}{\ensuremath{\mathnormal\phi}}
%% \newunicodechar{⟨}{\ensuremath{\mathnormal\<}}
%% \newunicodechar{⟩}{\ensuremath{\mathnormal\>}}
\newunicodechar{≡}{\ensuremath{\mathnormal\==}} %error when uncommented

and the error

$ ./compile.sh 
Latexmk: This is Latexmk, John Collins, 26 Dec. 2019, version: 4.67.
Latexmk: applying rule 'xelatex'...
Rule 'xelatex': File changes, etc:
   Changed files, or newly in use since previous run(s):
      'latex/Cubical/Algebra/Group/Morphism.aux'
------------
Run number 1 of rule 'xelatex'
------------
------------
Running 'xelatex -no-pdf -recorder  "main.tex"'
------------
This is XeTeX, Version 3.14159265-2.6-0.999991 (TeX Live 2019/Debian) (preloaded format=xelatex)
 restricted \write18 enabled.
entering extended mode
(./main.tex
LaTeX2e <2020-02-02> patch level 2
L3 programming layer <2020-02-14>
(/usr/share/texlive/texmf-dist/tex/latex/base/article.cls
Document Class: article 2019/12/20 v1.4l Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size10.clo))
(/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty) (./latex/agda.sty

LaTeX Warning: You have requested package `latex/agda',
               but the package provides `agda'.

(/usr/share/texlive/texmf-dist/tex/generic/iftex/ifxetex.sty
(/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty))
(/usr/share/texlive/texmf-dist/tex/generic/iftex/ifluatex.sty)
(/usr/share/texlive/texmf-dist/tex/latex/xifthen/xifthen.sty
(/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty)
(/usr/share/texlive/texmf-dist/tex/latex/base/ifthen.sty)
(/usr/share/texlive/texmf-dist/tex/latex/ifmtarg/ifmtarg.sty))
(/usr/share/texlive/texmf-dist/tex/latex/xcolor/xcolor.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/color.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/graphics-def/xetex.def))
(/usr/share/texlive/texmf-dist/tex/latex/polytable/polytable.sty
(/usr/share/texlive/texmf-dist/tex/latex/lazylist/lazylist.sty)
(/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty))
(/usr/share/texlive/texmf-dist/tex/latex/etoolbox/etoolbox.sty)
(/usr/share/texlive/texmf-dist/tex/latex/environ/environ.sty
(/usr/share/texlive/texmf-dist/tex/latex/trimspaces/trimspaces.sty))
(/usr/share/texlive/texmf-dist/tex/latex/l3packages/xparse/xparse.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-xdvipdfmx.def)))
(/usr/share/texlive/texmf-dist/tex/latex/xkeyval/xkeyval.sty
(/usr/share/texlive/texmf-dist/tex/generic/xkeyval/xkeyval.tex
(/usr/share/texlive/texmf-dist/tex/generic/xkeyval/xkvutils.tex
(/usr/share/texlive/texmf-dist/tex/generic/xkeyval/keyval.tex)))))
(/usr/share/texlive/texmf-dist/tex/latex/unicode-math/unicode-math.sty
(/usr/share/texlive/texmf-dist/tex/latex/unicode-math/unicode-math-xetex.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3packages/l3keys2e/l3keys2e.sty)
(/usr/share/texlive/texmf-dist/tex/latex/fontspec/fontspec.sty
(/usr/share/texlive/texmf-dist/tex/latex/fontspec/fontspec-xetex.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/fontenc.sty)
(/usr/share/texlive/texmf-dist/tex/latex/fontspec/fontspec.cfg)))
(/usr/share/texlive/texmf-dist/tex/latex/base/fix-cm.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/ts1enc.def))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/unicode-math/unicode-math-table.tex)))
(/usr/share/texlive/texmf-dist/tex/latex/newunicodechar/newunicodechar.sty)
(./main.aux (./latex/Cubical/Algebra/Group/Morphism.aux)) [1]
(./latex/Cubical/Algebra/Group/Morphism.tex
! Extra }, or forgotten $.
\PT@scanend ->\PT@post@preamble \egroup 
                                        
l.594 \end{code}
                
? 
0

There are 0 answers