Generation

All make commands are to be run from the directory that contains properdocs.yml, docs, and your Makefile.

Agda-Pages supports generation of websites from plain Agda and literate LaTeX (*.lagda, *.lagda.tex) or Markdown (*.lagda.md) Agda source files.

Agda-Pages also supports generation of websites from HTML files that were previously generated using Agda from plain Agda source files.

Generation from Agda

Command	Effect
`make check`	load the root module(s) and all imported modules
`make web`	generate hyperlinked highlighted web pages
`make serve`	browse the generated web pages using a local server
`make deploy`	deploy an unversioned website on GitHub Pages¹

To check your Agda source code, generate/update your local website, and browse² a preview of your website locally, run:

make check
make web
make serve

Then to publish the generated website on GitHub Pages, run:

make deploy

ProperDocs reports any broken internal links when serving or deploying the website. You can also check before deploying that all internal and external links are valid by installing linkcheck, serving your website locally, and running:

your-path-to-linkcheck/linkcheck -e :your-localhost-port --skip-file your-path-to-agda-pages/skip.txt

To avoid error reports arising from checking links to CSS files, the skip-file should include the line:

\.css$

The Agda-Pages repository provides skip.txt to use as a default skip-file.

Generation from HTML

Command	Effect
`make gen-pages`	generate web pages from HTML pages in `html`
`make gen-html`	generate HTML pages in `html` from Agda source code

To generate an Agda-Pages website from existing HTML pages that were previously generated from plain Agda source code using Agda, copy the HTML pages to the html directory, then run:

make gen-pages

This supports generation of Agda-Pages websites that correspond to old versions of Agda libraries, where generation from the Agda source code might require installing an outdated version of Agda.

The make web command simply combines gen-html with gen-pages.

Versioning

The mike utility makes it easy to deploy multiple versions of your website. It is enabled by the following setting in properdocs.yml:

extra:
  version:
    provider: mike

A version selector is then shown at the top of each deployed page.

Version identifiers that "look like" versions (e.g. 1.2.3, 1.0b1, v1.0) are treated as ordinary versions, whereas other identifiers, like devel, are treated as development versions, and listed above ordinary versions.

When deploying the generated website as a version, other versions of the website remain untouched. Deployed versions can however be subsequently updated or deleted.

If the specified version has already been deployed, redeployment updates the contents to the current generated website.

The Agda-Material make commands support a simple form of version management. For further version management commands, see the mike documentation.

Command	Effect
`make start-versioning`	clear any unversioned deployed website
`make deploy VERSION=...`	deploy version `...` of the website
`make default VERSION=...`	set the default version to `...`
`make delete VERSION=...`	remove deployed version `...`
`make list-versions`	display a list of all deployed versions

Danger

Deleting the default version can break existing links to your website!

To avoid that, first use make default VERSION=...' to change the default to a different version.

Miscellaneous

Command	Effect
`make clean`	remove `html` and unprotected `docs/*.md` files
`make clean-all`	remove all generated files
`make help`	show explanations of the main targets

Warning

make clean and make clean-all delete the local generated website! Regnerate before deploying.

In case of an RPC failed error, try running git config --global http.postBuffer 10g. ↩
By default, ProperDocs serves the website at localhost:8000. You can change that by setting SERVER to a different port number in your Makefile. ↩