↓Skip to main content
  1. Software Projects/

Agda-Material

Table of Contents

About Agda-Material #

Agda-Material supports generation of websites with highlighted, hyperlinked 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 with Agda-Material.

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-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 with highlighted, hyperlinked listings of the root module and all its imported modules, and publish the website on GitHub Pages – optionally with multiple versions.

Main features #

After adjusting the parameter settings in the Makefile to specify the root module and the source directory, you can run the following commands to generate, browse, and deploy a website.

  • Automatic regeneration: make web generates or updates a website.

  • Local preview: make serve lets you browse the generated website locally.

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

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.

  • Highlighted occurrences: hovering over a name highlights all the occurrences of that name 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.

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

  • Versioning: when multiple versions of a website have been published, users can switch between them 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 \). ↩︎