Skip to content

About Agda-Pages

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-Pages provides make commands to automate the steps that Agda leaves to the user. The User Guide explains how to use Agda-Pages to generate and publish a website with highlighted listings of your (plain and/or literate) Agda source files. The Agda-Pages Demo website illustrates the appearance of a website produced using Agda-Pages; the repository illustrates how to organize the required files and configure the website navigation.

Features

Agda-Pages generates websites with the following features.

  • Navigation: each page has a navigation panel for browsing the module hierarchy, and shows the path from the root module to the current page.

  • Hyperlinks: in the listing of an Agda module, clicking on any name jumps to its declaration.

  • Highlighted occurrences: hovering over a name highlights all its occurrences in the listing.

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

  • Responsive: the page layout adjusts to support browsing on 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: entering a word in the search box displays potential completions, and lists links to all pages that contain the word.

Examples

The Agda-Pages Demo website illustrates and tests use of Agda-Pages. The Demo section lists the Agda files included in the repository; the Library section lists the many files imported by the included modules.

The Agda-Pages repository supersedes the Agda-Material template. When it is added as a submodule, a simple Git command updates all its files to the latest commit.

The following websites were originally generated using the Agda-Material template. Their development involved editing a large Makefile copied from the template, with manual updates of the copied Makefile for new releases of Agda-Material. They have now been refactored to use Agda-Pages instead of Agda-Material.

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 from the HTML files deployed on the official Standard Library website. The different versions show how the library has evolved.

TypeTopology Pages

The TypeTopology Pages website is a prototype of an alternative rendering of the official TypeTopology website, and is unversioned.