Make totality a warning until compiling

Now, totality errors will not prevent loading a file. This means that
features such as :missing and :addmissing can be used to fix the
problem.

However, the compiler will fail if there are totality errors, just as it
does with metavariables.
Show more errors

The totality warnings mean that elaboration doesn't stop when it sees a
totality issue. Allow both issues to be reported in this test.
Update for totality warnings

Now, totality discrepancies prevent compilation. Add partial annotations
to totality005 to make it compile.
Don't try to compile a test that doesn't have `main`

Instead, just --check it.
Update test for totality warnings

Now, all totality problems are shown. Update test accordingly.
Add totality warnings to CHANGELOG
Added a proof that (x ++ (y ++ z)) = ((x ++ y) ++ z) for Vects
Merge pull request #1210 from DanielWaterworth/vect_append_associative

Added a proof that (x ++ (y ++ z)) = ((x ++ y) ++ z) for Vects
Merge pull request #1204 from david-christiansen/totality-warning

Make totality a warning until compiling
incremented blaze markup version
Stop building packages if there are totality mismatches

This is to stop libraries from preventing executables to build later.
Merge pull request #1215 from david-christiansen/totality

Stop building packages if there are totality mismatches
Merge pull request #1216 from jeffersoncarpenter/blaze-markup-version

incremented max allowed blaze markup version
Move interactive commands to their own module
Propagate bound implicits to record updates

Fixes setter warning when building Control.Monad.Writer
Add Data.List to base

Currently just includes 'Elem' and 'isElem' to decide membership.
Remove spurious error from 'setter' warning
Move 'mkNo' to a where