* 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