[Agda] Generating pretty HTML listings of Agda repos using travis and jlimperg/agda-stdlib

[Andreas Abel]

On my quest how to automatically generate up-to-date HTML listings of my
Agda code in a github repo, Google found me the docker image

jlimperg/agda-stdlib

by Jannis Limperg. Works like a charm in connection with travis, which
has docker integration by default. Thanks Jannis!

An example repo with listing is here:

https://github.com/andreasabel/lambda-definability

https://andreasabel.github.io/lambda-definability/stlc/html/Everything.html

This is my summary how to set things up:


How to create documentation on github.io with travis.ci

Synopsis: a travis script can push-force to the gh-pages branch
of a repo, whose contents can be displayed on

https://<user>.github.io/<repo>

1. In git repo

- Add a Makefile that generates content of "docs" subdirectory

- Add a suitable .travis.yml e.g.

sudo: required
language: generic

services:
- docker

before_install:
- docker pull jlimperg/agda-stdlib

script:
- make docs

deploy:
provider: pages
local_dir: ./docs
project_name: "Fancy name of your Agda project"
skip_cleanup: true
target_branch: gh-pages
github_token: $GITHUB_TOKEN
on:
branch: master

- Create a branch gh-pages

2. In github.com repo settings

- Settings, section GitHub Pages: select source "gh-pages branch"
(note: can only be selected if branch exists)
- Create a token in Settings / Developer settings
- Save the token somewhere secure

3. On travis-ci.org

- Switch on repo
- In Settings for the repo, add environment variable
GITHUB_TOKEN with content the secret token you generated

4. Finally

- push or trigger a travis build manually
- if things do not show up on github.io,
alternate between http and https access
(workaround a bug)