Literate Agda: How do I change the size of the displayed code?

Question

I am making Beamer slides for a talk about an Agda formalisation of mine.

In order to make the code fit onto the slide, I need to scale the font size. One would think that this might not be so hard, but the previous 20 tricks that I've tried all fail in the sense that, post compilation with agda --latex, the relevant tricks simply disappear from the output file.

I tried setting the global document font size to the smallest possible option (and then using \Huge for all remaining text), but 8pt on a Beamer project is still quite large and doesn't quite give me the room that I need.

Has anybody here ever been able to successfully change the code output size in a Literate Agda project?

P.S. There exists at least one absolutely unpalatable solution: hand modifying the output latex files.

Answer 1

This is more of a LaTeX question. All the generated code will typically end up in a code environment and so you can use a LaTeX solution to patch that environment.

Using this answer, I get the following file:

\documentclass[9pt]{article}
\usepackage{agda}

\makeatletter
\g@addto@macro{\code}{\fontsize{15}{18}}\selectfont
\makeatother

\begin{document}

This is not in a code environment

\begin{code}
module LaTeX where
-- this is in a code environment
\end{code}

And we're back out of the code environment

\end{document}

and this is what the output looks like:

The first argument to fontsize is the actual size, the second is the distance between the bottom of 2 consecutive lines in a paragraph so should probably be ~20% bigger than the first one.