[Agda] Literate Agda bit rot

[Philip Wadler]

The example of Literate Agda in the 2.4.0 CHANGELOG appears not to work.
See below. Can someone please suggest a fix?

By the way, the example in the change log is much more helpful than the one
in the documentation at


https://agda.readthedocs.io/en/v2.5.4/tools/literate-programming.html?highlight=literate
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.LiterateAgda

May I suggest the latter two be updated? Cheers, -- P


bruichladdich$ more test.lagda
\documentclass{article}
\usepackage{agda}
\begin{document}

\begin{code}
data αβγΎεζΞικλΌΜΟρστυφχψω : Set₁ where

postulate
→⇒⇛⇉⇄↩⇹↠⇀⇁ : Set
\end{code}

\[
∀X [ ∅ ∉ X ⇒ ∃f:X ⟶ ⋃ X\ ∀A ∈ X (f(A) ∈ A) ]
\]
\end{document}
bruichladdich$ agda --latex test.lagda
bruichladdich$ cd latex/
bruichladdich$ pdflatex test
This is pdfTeX, Version 3.14159265-2.6-1.40.17 (TeX Live 2016) (preloaded
format=pdflatex)
restricted \write18 enabled.
entering extended mode
(./test.tex
LaTeX2e <2016/03/31>
Babel <3.9r> and hyphenation patterns for 83 language(s) loaded.
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/article.cls
Document Class: article 2014/09/29 v1.4h Standard LaTeX document class
(/Users/wadler/Library/texmf/tex/latex/size10.clo)) (./agda.sty
(/usr/local/texlive/2016/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
(/usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/ifluatex.sty)
(/usr/local/texlive/2016/texmf-dist/tex/latex/xifthen/xifthen.sty
(/usr/local/texlive/2016/texmf-dist/tex/latex/tools/calc.sty)
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/ifthen.sty)
(/usr/local/texlive/2016/texmf-dist/tex/latex/ifmtarg/ifmtarg.sty))
(/usr/local/texlive/2016/texmf-dist/tex/latex/xcolor/xcolor.sty
(/usr/local/texlive/2016/texmf-dist/tex/latex/graphics-cfg/color.cfg)
(/Users/wadler/Library/texmf/tex/latex/pdftex.def))
(/usr/local/texlive/2016/texmf-dist/tex/latex/polytable/polytable.sty
(/usr/local/texlive/2016/texmf-dist/tex/latex/lazylist/lazylist.sty)
(/usr/local/texlive/2016/texmf-dist/tex/latex/tools/array.sty))
(/usr/local/texlive/2016/texmf-dist/tex/latex/etoolbox/etoolbox.sty)
(/usr/local/texlive/2016/texmf-dist/tex/latex/environ/environ.sty
(/usr/local/texlive/2016/texmf-dist/tex/latex/trimspaces/trimspaces.sty))
(/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/ucs.sty
(/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/data/uni-global.def))
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/inputenc.sty
(/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/utf8x.def))
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/fontenc.sty
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/t1enc.def))
(/usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/amsfonts.sty)
(/usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/amssymb.sty)
(/usr/local/texlive/2016/texmf-dist/tex/latex/tipa/tipa.sty
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/fontenc.sty
(/usr/local/texlive/2016/texmf-dist/tex/latex/tipa/t3enc.def
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/t1cmss.fd))
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/t1enc.def))))
(./test.aux)
(/usr/local/texlive/2016/texmf-dist/tex/latex/tipa/t3cmr.fd)
(/Users/wadler/Library/texmf/tex/latex/supp-pdf.tex
[Loading MPS to PDF converter (version 2006.09.02).]
) (/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/ucsencs.def
fontencoding T3 patched
) (/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/data/uni-3.def)
! Undefined control sequence.
\u-default-945 #1->\textalpha

l.20 \end{code}

?


. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Too brief? Here's why: http://www.emailcharter.org/

[Nils Anders Danielsson]

Post by Philip Wadler
The example of Literate Agda in the 2.4.0 CHANGELOG appears not to
work. See below. Can someone please suggest a fix?

The changelog states that the example was tested using TeX Live 2012.
Perhaps it still works using an older version of TeX Live.

If you are willing to use LuaLaTeX or XeLaTeX, then the following code
seems to work:

\documentclass{article}

\usepackage{agda}
% Support for sans-serif Greek. Note that loading this package might
% lead to changes in the appearance of some non-Greek characters as
% well.
\usepackage[scale=0.9]{FiraSans}

\begin{document}

\begin{code}
data αβγδεζθικλμνξρστυφχψω : Set₁ where

postulate
→⇒⇛⇉⇄↦⇨↠⇀⇁ : Set
\end{code}

\[
∀X [ ∅ ∉ X ⇒ ∃f:X ⟶ ⋃ X\ ∀A ∈ X (f(A) ∈ A) ]
\]

\end{document}