Skip to content

About Agda Standard Library Pages

This website illustrates and tests use of Agda-Pages to generate websites with module navigation between highlighted, hyperlinked listings of Agda code.

Website

The README section was generated from plain Agda files in the doc directory.

The Library section was generated from plain Agda files created by GenerateEverything.hs, which import modules from the src directory. The Library home page is also the website home page.

When deployed, the website displays a version selector on all pages. Currently, only the master version has been deployed; it was generated from a fork of the Agda StdLib repository after the release of version 2.4.

Warning

The Agda code in the master version of the standard library may have been updated since the master version of the present website was generated. For the definitive listings of the master branch, see the official Agda StdLib website.

See the Agda-Pages About page for an overview of the features of the generated website, and for links to further examples.

Generation

The Agda-Pages User Guide explains how to generate a website listing Agda code in any GitHub repository.

See the Agda-Pages README for how to install Agda-Pages, and for a list of its main software dependencies.

The following files were added to the fork of the standard library repository to support website generation using Agda-Pages:

.
├─  ...
└─  pages/
    ├─  agda-pages/
    │   └─ ...
    ├─  docs/
    │   ├─ About.md
    │   └─ .nav.yml
    ├─  Makefile
    └─  properdocs.yml

The pages directory includes all the required files:

  • agda-pages was added as a Git submodule referring to the Agda-Pages repository.
  • docs/About.md is the source file for the present webpage.
  • docs/.nav.yml configures the main navigation of the website.
  • Makefile configures the location of the Agda source files and a non-generated Markdown file.
  • properdocs.yml configures the name and location of the website and the repository.

Running the following shell commands in the pages directory generated the present website:

make index
make check
make web
make serve

While serving the website, running the linkcheck application reports:

agda-stdlib: .../linkcheck/linkcheck -e :8020 --skip-file ../agda-pages/skip.txt

Perfect. Checked 1935439 links, 1209 destination URLs (1 ignored).

The generated website was initially deployed at https://pdmosses.github.io/agda-stdlib/pages/ by:

make start-versioning
make deploy VERSION=master
make default VERSION=master

An update can be deployed at the same URL by:

make deploy VERSION=master