Skip to content

About Agda-Material

Agda-Material supports generation of websites and PDFs with highlighted listings of (plain or literate) Agda source code.

See the README page for how to create a repository for using Agda-Material.

See the user guide for a summary of how to generate websites and PDFs with Agda-Material.

Warning

This version of the website was generated rom the gen-pdf branch.

Background

Agda can generate highlighted, hyperlinked web pages from a root module, automatically generating a separate page for each imported module. But it is left to the user to incorporate the generated pages in a website, and to publish the website.

Agda can also generate LaTeX code for highlighting the source code from a literate Agda module; LaTeX code for imported modules has to be generated separately. It is left to the user to include the generated code in a complete LaTeX document, and to compile the document to produce a PDF.

Agda-Material automates the steps that Agda leaves to the user. After creating a GitHub repository from the Agda-Material template and adding Agda code, some simple commands generate a website and a PDF with highlighted listings of the root module and all its imported modules, and publish the website on GitHub Pages -- optionally with multiple versions.

Main features

  • Automatic regeneration: make all generates or updates a website and PDF with highlighted listings.

  • Local preview: make serve lets you browse the updated website and PDF locally.

  • Automatic publication: make deploy publishes the website on GitHub Pages.

Generated websites

  • Navigation menu: a generated hierarchical menu with links to all imported Agda modules.

  • Hyperlinks: clicking on a name in a generated web page jumps to its declaration and shows the location of the module in the navigation hierarchy.

  • Light or dark: users can toggle between light, dark, and automatic color palettes.

  • Responsive page layout: for browsing on tablets and mobile devices as well as desktop displays.

  • Options: a generated website can include the ordinary HTML pages generated by Agda, and the generated PDF.

  • Versioning: when multiple versions of a website have been published, users can switch between them in the browser.

Generated PDFs

  • Generated LaTeX document: inputs the LaTeX files generated by Agda from the root module and the local imported modules.

  • Plain or literate Agda sources: plain Agda files are highlighted by wrapping them in a code environment.

  • Good Unicode support: commonly-used Unicode characters are translated to LaTeX.

  • Table of contents: the listing of each included module is in a separate section.

  • Adjustable highlighting style: options supported by the LaTeX package agda.sty can be selected.