Over the Christmas break, I decided to play a bit with Travis, a continuous integration platform building, testing and deploying software. Here are the various projects that benefited from it.
The first thing I set out to do was run a test build of the projects hosted on my vart repository where, inspired by Jenn Schiffer's var t; experiments, I try to write programs which generate artsy things using haskell. Mondrian generates and exports (using JuicyPixels) images in this style whilst ExquisiteCorpse is pretty self-explanatory. Getting this to work was as simple as registering on the travis website, flipping a switch for this repo, creating a .cabal file for each project and adding a really simple .travis.yml file to the tree.
Building and testing is all fine and dandy until we want to produce some artefacts from the built software and share them. Well, one solution to such a problem is to use personal access tokens on github and simply host the content on Github pages.
This website used to be hosted by ENS Lyon but, not being a student there anymore, it was finally taken down in October 2014. It used to be written in php which our personal pages' server does not support so I figured it was as good an excuse as any to rewrite the whole thing from scratch. I settled for jaspervdj's Hakyll mainly because it is written in haskell and I figured I could extend it to meet my needs rather easily. As it turned out, getting travis to build and deploy the pages was probably the least painful step in the whole process; in comparison figuring out how to parse the flavour of BBCode I use for these posts was hell [1].
The .travis.yml file is sligtly more complicated this time given that I need to push the generated html pages to the master branch of the repository. To do so, one needs to generate personal access tokens on github and then encrypt them using travis. If you look closely at the file, that's the ${GH_TOKEN} I use when pushing.
As soon as I understood how to get it to work, I put together the reciptacle website. A bunch of us, uni friends from Lyon, have been sharing recipes we enjoy cooking on a github repository for quite a while. With a bit of bash scripting magic, the markdown files are now turned into html ones, are listed in an index and added to different categories based on the #hashtags they contain.
All of this was made possible by this relatively simple .travis.yml file. I should add that the whole process has been made more secure by Hugo using ShellCheck, yet another really cool haskell project, to detect typical caveats in our various scripts.
Once you know how to upload content to github pages, it is rather easy to figure out how to generate and push the documentation produced e.g. by Agda when typechecking a project. This is why we now have travis generating the standard library's documentation.
If a github repository is ideal to host text files, it is rather different when you want to distribute binaries where you do not care about the previous versions. This is where Dropbox comes into play in this little series of experiments: Andrea Fabrizi's Dropbox-Uploader makes interacting with Dropbox very easy! And using travis' hability to encrypt files, we can safely upload our credentials to a public repository.
The way the documentation for Agda's standard library was generated by my first script was not very robust: we would fetch the current master branch of Agda and compile it (which may fail) before starting the real work. But why should the documentation generation fail if the master branch does not compile at the precise time where the build was started? Well, it should not. Why should we spend some time recompiling Agda at every change in the standard library? Well, we should not.
I could not rely on the ubuntu package as it was clearly too old for the standard library which tends to rely on "newly" (as in "in the last few months") introduced features. The obvious solution was to, somehow, get travis to generate a static binary when compiling and testing Agda and upload it on Dropbox. This is the purpose of my build-binary branch.
Compiling static haskell executables is not a process well documented online. It is pretty hard to stay sane when facing stackoverflow answers pointing you at a blog now defunct, toy examples not dealing with e.g. data directories (hint: Agda has some!), and invalid information about permission escalation in order to run some of the install as root (typically: creating the data directories in /usr/share/).
After quite a bit of poking around, I finally managed to find the right set of flags (at least for linux, it's not tested on windows). I could not fix the permission escalation problem (yes, I have tried root-cmd) so I ended up adopting a solution I am not proud of: manually creating the directories I need with the permissions I want. If someone knows the right way to do it, please do share [2]!
Once you have travis-compatible Agda executables lying around and a draft paper which is actually a literate Agda file, there is one obvious thing to do: get travis to typecheck your development, build your paper and the documentation for the whole project and host all of this on github pages. This is precisely what Conor and I have done with our Certified Proof Search for Intuitionistic Linear Logic draft. This is surely not the final answer to How to review formalized mathematics but it might be a step in the right direction.
To access the tarballs hosted on Dropbox using the command-line, I have the impression that one needs my credentials. However they are available for all to download so there may be a way to automate that. If you have suggestions with respect to alternative hosting solutions making it easier for other people's scripts to pull the tarballs, please contact me!