[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/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180704/25fab591/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180704/25fab591/attachment.ksh>