fix(util/memory): warning when compiling with clang++
feat(build): add IGNORE_SORRY cmake option

It allows us to perform nightly builds and avoid distracting warning
messages on CDASH.
fix(.travis.yml): (try to fix) random build failures at travis

At https://bitcointalk.org/index.php?topic=304389.0, people suggest
that the failure

    g++-4.8: internal compiler error: Killed (program cc1plus)

usually happens when the system does not have enough free memory.
A possible workaround is to disable parallel build, and compile file by
file. I added the option `-j1` to Ninja.
feat(build): add 'CROSS_COMPILE' cmake option

When CROSS_COMPILE=ON, the Lean standard library will not be compiled.
fix(frontends/lean/pp): do not invoke type checker on expressions
containing free variables.

This could happened when the pretty printer was used from Lua to print
nested subterms
fix(tests/lean/uni_bug1): make sure test does not produce a 'used sorry' warning.

Thus, the output behavior is the same when we compile lean with/without IGNORE_SORRY=ON
fix(library/match): memory leak that only happens with compiling with clang++
feat(frontends/lean): allow users to define "numeral notation"
fix(frontends/lean/server): must save the starting environment/options when reprocessing file, fixes #209
doc(make/msys2): instructions for building native windows Lean binary
doc(README.md): group build instructions by system
fix(.travis.yml): trying old configuration for TESTCOV
feat(library): add constructions of categories, some changes in eq, sigma and path

in eq, add theorem for proof irrelevance and congruence for binary functions
in sigma, add some support for triplets
in path, comment out two unneccesary definitions
in category, add Cat, slice, coslice, product and arrow categories, also add fully bundled approach
feat(library/data/int): remove duplicate theorem, fix one sorry
feat(library): changes in eq.lean sigma.lean and category.lean

in eq.lean, make rec_on depend on the proof, and add congruence theorems for n-ary functions with n between 2 and 5
in sigma.lean, finish proving equality of triples
in category.lean, define the functor category, and make the proofs of the arrow and slice categories easier for the elaborator
feat(emacs/lean-input): shortcut for long arrow
fix(.travis.yml): trying to fix failure at travis
fix(frontends/lean): add 'eval' command
fix(util/sexpr/option_declarations): default value in help message, fixes #212
feat(library/unifier): add 'on-demand' choice constraints, they are processed as soon as their type does not contain meta-variables anymore