Skip to content

An Alternative TypeTopology Website

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

About the website

The website was generated from the Agda source files in the add-pages branch of a fork of the TypeTopology repository.

Warning

The current definitive TypeTopology website is generated directly from the Agda files in the TypeTopology repository. Some of the Agda files in the fork from which the present website was generated may be outdated, resulting in outdated webpages.

The Modules section includes the index webpage generated from the top-level Agda module that imports --safe modules which strictly use the philosophy of TypeTopology. The Modules section also includes the AllModulesIndex webpage generated from the Agda module which imports everything else recursively.

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 TypeTopology 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 generates the present website:

make check
make web
make serve

While serving the website, running the linkcheck application reports:

TypeTopology: .../linkcheck/linkcheck -e :8010 --skip-file pages/agda-pages/skip.txt

Perfect. Checked 2180685 links, 1016 destination URLs (1 ignored).

The generated website is deployed at https://pdmosses.github.io/TypeTopology/ by:

make deploy