[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