About Agda-Material #

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

Examples of use #

The Agda-Material website is generated using different releases of the [agda-material repository]. Each version of the website correponds to a minor release of the repository, updated to reflect the latest patches.

Denotational semantics in Agda #

The XDS-Agda website includes experimental Agda embeddings of three separate denotational definitions. The different versions of the website show how the embeddings have evolved.

Agda standard library #

The Agda-StdLib website is a prototype generated using the same Makefile as the Agda-Material website. The different versions of the website correspond to released versions of the library, and show how the library has evolved.

TypeTopologyDocs #

The TypeTopologyDocs website is a prototype of an alternative rendering of the official TypeTopology website, and is unversioned. The Makefile used to generate it currently differs slightly from the Makefile used for the Agda-Material website.