Skip to content

An Alternative Website

This website was generated from the Agda source files in a FORK of the TypeTopology repository using a Makefile (copied from the Agda-Material template, with minor adjustments).

Info

This website was deployed from the gen-website-indexes branch of the fork.

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.

The theme Material for MkDocs with the Awesome-Nav plugin generates the hierarchical navigation menus from the directory structure of the repository and the nav specification in the file docs/.nav.yml.

The Modules section lists an index module that imports the index for for each part of the TypeTopology library. The section also includes AllModulesIndex, which is the main index, in the sense of being the only one which imports everything else recursively, while index is the index of --safe things which strictly use the philosophy of TypeTopology.

This website was generated from a fork of the TypeTopology repository after copying the following files from the Agda-Material template:

  • Makefile
  • mkdocs.yml
  • docs/*

Makefile, mkdocs.yml, and docs/.nav.yml required minor editing. The docs/*.md files were replaced by the docs/about.md file containing the source for the current page. The shell script docs/updatehtml was copied from admin-utilities/updatehtml.

The shell commands used to check the Agda sources, then generate and browse this website, were:

make check
make web
make serve

The following command was used to deploy the generated website to GitHub Pages:

make deploy

(Further commands can be used to deploy a versioned website.)

The approximate times taken by the above commands were:

  • make check: 15 seconds
  • make web: 100 seconds
  • make serve: 75 seconds
  • make deploy: 100 seconds

Note

The 900+ Agda modules in the repository fork had previously been checked.

Running linkcheck:

TypeTopology: ~/Applications/linkcheck/linkcheck -e localhost:8010 --skip-file skip.txt
Perfect. Checked 3104882 links, 1868 destination URLs (1 ignored).

Agda-Material

The Agda-Material template supports generation of websites with highlighted, hyperlinked listings of (plain or literate) Agda source code. See the Agda-Material website for how to install and use the template, and for some test modules.