Skip to content

About Agda-Material

Info

This version was deployed from the main branch of the repository.

Agda-Material supports generation of websites with highlighted, hyperlinked listings of (plain or literate) Agda source code, optionally with versioning.

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

See the User Guide for a summary of how to use Agda-Material.

Background

Agda can generate highlighted, hyperlinked HTML 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-Material automates the steps that Agda leaves to the user. After creating a GitHub repository from the Agda-Material template and adding Agda source files, some simple make commands generate a website with highlighted, hyperlinked listings of one or more root modules and their imported modules, and publish the website on GitHub Pages – optionally with multiple versions.

Main features

After adjusting the argument default settings in the Makefile to specify one or more root modules and source directories with your Agda code, you can generate, browse, and deploy a website using simple make comamnds:

  • Automatic regeneration: make web generates or updates web pages from Agda source code.

  • Local preview: make serve builds the website and lets you browse it.

  • Automatic publication: make deploy publishes or updates the built website.

  • Optional versioning: make deploy VERSION=... publishes or updates the specified version.

Generated websites

The websites have the following features.

  • Navigation menu: a generated hierarchical menu with links to all imported Agda modules. Each page shows the path to the current page (so-called breadcrumbs).

  • 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.

    If the website includes plain HTML pages generated by Agda, clicking on the module name in a page with navigation jumps to the corresponding HTML page, and vice versa.

  • Highlighted occurrences: hovering over a name highlights all its occurrences on the page.

  • 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.

  • Versioning: when multiple versions of a website have been published, a version can be set as the default, and users can switch between versions in the browser.

  • Search: the browser displays all files that contain occurrences of any of the words specified in the search field.1

  1. Search works best for websites where each page is divided into small sections. It is currently of limited use for websites generated from large Agda modules. Moreover, it appears that some ASCII characters do not produce the expected results (even when escaped by \). ↩