[Agda] Generating pretty HTML listings of Agda repos using travis and jlimperg/agda-stdlib
Andreas Abel
abela at chalmers.se
Tue Jul 24 09:41:55 CEST 2018
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)
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/
More information about the Agda
mailing list