AIMXXWrapUp

 * Wrap up 14.10~
 ** Francesco Mazzoli
 - GHCi mode for Agda.
   - Easy to install via emacs package mech.
   - Would be integrated with cabal install Agda

 - Travis CI build
   - Build ok once, now there's some problem. Trying to find where the
     problem is.

 ** James Chapman
 - Quotients.agda in stdlib.
   - Quotients for Setoid etc.
   #+BEGIN_EXAMPLE
   record Quotient...(S : Setoid) : ... where
     field
       Q : Set c
       abs : S.Carrier → Q

   Quotients {c}{ℓ} = (S : Setoid c ℓ) → Quotient S 
   compat f = {a a' : A} → a ≈ a' → f a ≅ f a′
   #+END_EXAMPLE
   Examples would be added.
 - Category theory library: Categories.XXX. on jmchapman@github...
   - Modules organized like the toc of a textbook.
   - Initial, Terminal, ... Mono, Iso, ... Idems, Sections, ..., Pullbacks,...
     Functors, Naturals, Monads, Adjunctions, Monads.Kleisli, -.EM, ...
   - UN: Beware of module name crash at the toplevel (Categoies,
     Adunctions, Functors, ...)
     - May make sense to have a single top module.
     - Better structure it like stdlib.
       - .agda files under src subdirectory, Everything.agda outside of
         the src.

 ** Andreas Abel, Ulf Norell, Makoto Takeyama
 - Serialise.hs optimization sprint: 25% faster in total on (project organized
   like) the standard library. (40% of Serialise time gone.)

 ** Jesper Cockx
 - Making tactics work nicer
   - quoteContext
   - typedTac
     - arguments under contexts
     #+BEGIN_EXAMPLE
     -- phantom
     TypedTerm : ... → Set
     TypedTerm ctx goal = Term

     typedTac ... → TypedTerm ctx ty → Term
     typedTac ctx goal x = x

     test m n = tactic typedTac ?
                                ^ this instantiating ctx and goal
            -- (tactic typedTac) ?  is different and useless
     #+END_EXAMPLE

 ** Ulf Norell
 - Unquoting mutal defs with JCo
   - unquoteDef implemented.  Used by Nicolas.
 - Resurrecting the sharing data strucure for Term.
   - Working. Agda now has Call By Need evaluation.
   - Serialization faster, type checking slightly slower.
   - Not getting that much sharing.
     - Start to understanding why Agda is taking that much memory.
       - Lambda lifting of meta vars destroys sharing.
   - Looking at making some shortcuts for certain patterns of meta var
     uses, e.g. applying id subst.
   - Soon to be pushed.
   - (Suspension calculus need to be checked out?)

 ** MT
 - Manual instruction for installing Agda on Windows updated.
   - Hackage Agda-2.4.2 has severe problem on Windows.
   - Need 2.4.2.1 that turns off cpphs on Windows by default.

 ** Guillaume Brunerie
 - Solved performance problem in recursive instance search.
   - Getting a bit more of unsolved metas