[Agda] Writing a paper in Literate Agda

Alan Jeffrey ajeffrey at bell-labs.com
Fri Nov 29 16:10:10 CET 2013

Ah, that's a good idea. I'll give it a shot...


On 11/29/2013 04:57 AM, Nils Anders Danielsson wrote:
> On 2013-11-28 16:51, Alan Jeffrey wrote:
>> In terms of tool support, the one thing I did sorely miss is the
>> ability to run LaTeX from emacs's Agda mode. Does anyone know of an
>> easy way to do this?
> Perhaps you can use latexmk -pvc. From the man page:
>     The second previewing option is the powerful -pvc option (mnemonic:
>     "preview continuously"). In this case, latexmk runs continuously,
>     regularly monitoring all the source files to see if any have changed.
>     Every time a change is detected, latexmk runs all the programs
>     necessary to generate a new version of the document. A good previewer
>     (like gv) will then automatically update its display. Thus the user
>     can simply edit a file and, when the changes are written to disk,
>     latexmk completely automates the cycle of updating the .dvi (and
>     possibly the .ps and .pdf) file, and refreshing the previewer's
>     display. It's not quite WYSIWYG, but usefully close.

More information about the Agda mailing list