Skip to content

Agda-Material

Agda-Material automates the steps that the Agda back-end leaves to the user when generating a website with highlighted, hyperlinked listings of Agda code.

This is the README page for the repository pdmosses/agda-material. It explains how to create a repository for using Agda-Material.

See the About page for an overview of motivation and features.

See the User Guide for a summary of how to generate websites with Agda-Material.

Repository contents

The repository contains the following files:

  • agda: directory for Agda source code
  • docs: directory for generating a website
    • docs/javascripts: directory for Javascript files
    • docs/stylesheets: directory for CSS files
    • docs/.nav.yml: configuration file for navigation panels
    • docs/about.md: Markdown source for the About page
    • docs/README.md: Markdown source for this README page
    • docs/Library/index.md: Markdown source for the Library page
    • docs/Test/index.md: Markdown source for the Test page
  • CHANGELOG.md: summary of significant bug-fixes and feature updates
  • Makefile: automation of website generation
  • mkdocs.yml: configuration file for the generated website
  • UNLICENSE: release into the public domain

The repository does not contain any generated files.

By default, Agda-Material creates generated files in the following directories:

  • docs/html: HTML pages
  • docs/md: Markdown pages
  • site: built website
  • temp: temporary files

The default directories for Agda source code and generated files can be changed by editing the Makefile. This affects the URLs of the generated web pages: by default, the URL of the HTML page generated from a module named A.B.C is of the form .../html/A.B.C.html, and that of the corresponding MD page is of the form .../md/A/B/C/, where ... is the website URL (including the version identifier, if any).

The location of the directory docs can be configured by setting docs_dir in mkdocs.yml; it does not affect the URLs.

Software dependencies

Agda-Material has been tested with the software versions listed below. It should produce similar results with other recent versions (although Material for MkDocs v9.7 has many more features than v9.6).

Tip

Starting in Material for Mkdocs 9.7.2, a warning is printed during a build about the upcoming MkDocs 2.0 changes. To disable this warning:

export NO_MKDOCS_2_WARNING=1

Platform dependencies

Agda-Material has been developed and tested on MacBook laptops with Apple M1 and M3 chips running macOS Tahoe (26.3) with CLI Tools.

Please report any issues with using Agda-Material on other platforms, including all relevant details. Pull requests for addressing such issues are welcome.

Installing Agda-Material

Check that you have installed all the relevant software dependencies.

Then:

Either create a fresh repository

On pdmosses/agda-material:

  • Click on the Use this template button (near the top of the page)

Locally:

  • Clone the resulting repository

Or copy files to your existing repository

On pdmosses/agda-material:

  • Click on <> Code then Clone or Download

Locally:

  • Copy/merge the following files and directories from agda-material to your repository:

    • Makefile
    • mkdocs.yml
    • agda/*
    • docs/*
    • .gitignore

Testing Agda-Material

  1. In a terminal from the root directory of your repository:

    make check
make web
make serve

  2. Then in a web browser:

    • Open localhost:8000/agda-material
    • Check that the local site corresponds to the Agda-Material website on GitHub Pages (apart from the version selector)

  3. In the terminal:

    make clean-all

    Check that the following generated directories do not exist:

    • docs/html
    • docs/md
    • site
    • temp

Preparing to use Agda-Material

Update the MkDocs settings

In mkdocs.yml, update the repository settings:

  • site_name
  • site_url
  • repo_name
  • repo_url

Replace the Agda modules

  • Remove the agda directory.
  • Add a directory containing your own Agda modules.

  • In Makefile:

    • set the value of DIR to the directory containing your Agda modules;
    • set the value of ROOT to the name of a module that imports all the other modules to be included in your website.

    Both DIR and ROOT can be a comma-separated list: web pages are generated for all modules in the ROOT list, and for all imported modules found either in the directories in DIR list or in libraries.

Update Markdown source files and navigation

Replace all docs/*.md files by your own Markdown file(s).

  • Your website home page should be named docs/index.md or docs/README.md.
  • Update docs/.nav.yml to create your desired navigation hierarchy.1

See the User Guide for a summary of how to generate websites with Agda-Material.

Upgrading to the latest version

Compare the current contents of the following files in the main branch with the copies in your fork or clone of this repository:

  • docs/javascripts/*.js
  • docs/stylesheets/*.css
  • Makefile
  • mkdocs.yml

Copy all changes that do not conflict with your own changes.

Contributing

Please report any issues with using Agda-Material, including all relevant details. Pull requests for addressing reported issues are welcome. Discussions may include queries, comments, and suggestions for improvement, announcements about Agda-Material, and links to websites generated using it.

Contact

Peter Mosses

p.d.mosses@tudelft.nl

pdmosses.github.io

  1. You may prefer to specify only the upper levels in docs/.nav.yml, leaving the lower levels to implicitly reflect your directory hierarchy (with pages listed in alphabetical order). See the Awesome-nav plugin documentation for details of the possibilities. ↩