- One sentence per line, it makes merging contributions easier.
- Please aim to make commits self contained. Ideally one thing at a time.
- GitHub pull requests only. It might sound harsh but in future we aim to look at leveraging travis to provide CI testing of the tutorial.
- Campfire Rules, try and leave the files you work on in a better state than when you found them.
- We do not store binary builds of the tutorial here.
- Before submitting try and run your contribution through: Style-Check.rb. Style-Check.rb is a simple tool to check for bad phrases, and nominal bad LaTeX. The output is given in compiler format.
- Version of English used...this has yet to be decided upon.
idrislang.sty is used to type set idris code within the tutorials.
To keep things DRY this style file has been hard linked with the original kept in idris-dev.
Normally, this file should live in the your local texmf tree, but if we want auto-generation of PDFs then the style file needs to be distributed alongside...
The tutorial is written in LaTeX and the build tool latexmk will be used to manage the compilation process.
latexmk comes with the default texlive installation.
A nominal Makefile is provided that abstracts over the use of latexmk.
Emacs with AucTeX-mode is used during writing.
The auto generated by AucTeX should be taken care of with the .gitignore.
Ditto goes with those pesky .DS_Store files generated by Mac OS X.
However, do not be surprised to see several AucTeX related code in LaTeX comments at the bottom of several files.
Useful bash aliases for working with LaTeXmk instead of a Makefile are:
alias latexBuild='latexmk -gg -pdf -pvc -bibtex'
alias latexQBuild='latexmk -gg -pdf -bibtex'
alias latexClean='latexmk -c'
alias latexClobber='latexmk -C'