During the code sprints I focused on porting some Haskell code to Agda with the aim to use (and find bugs in) the tool agda2hs. The idea is that if I stick to the supported subset of Agda for the "runnable" part I can extract working Haskell code, and also formalize some proofs about the code. The code I worked on porting is for a paper on Level-p-complexity of boolean functions (with a case study on iterated two-level majority).
One session I had a good time exploring the BNFCAgda backend together with Phil Wadler. We started from earlier Haskell code using BNFC-meta (stackage). (A longer term dream would be to have BNFC-meta-like embedded language definitions including quoting in Agda...)
I also got the opportunity to hear several other presentations and discussions about hot topics in the Agda world and what needs to be done next.
Practical things include Agda library management, support for continuous integration, and improving Agda's editor integration.
An interesting historical detail is that I was also in the very first Agda meeting in 2004 when I was PhD advisor of Ulf Norell and Nils Anders Danielsson, two of the main Agda developers. Time flies!