Tuesday 9 May
- Jesper, Andreas, Youyou, John, Paul: started a paper specification of core Agda; syntax, conversion.
- Victor: started to merge the two meanings of literate Agda latex code blocks.
- Guillaume, Fredrik: serialising warnings; trying to find the part of the state that needs to be kept.
- Guillaume: getting the detection of useless `open import`s to work
- Anton, Stephan: thinking about components.
- Wolfram, Ulf: looked at the case optimisations in treeless
Wednesday 10 May
- Victor, Paul: playing with cubical Agda; formalising paths of sigma types.
- Wolfram: continued pattern floating in GHC backend.
- Jesper, Andreas, Youyou, John: more typing rules.
- Andrea: fixed bug with univalence for lists from this morning.
- Fredrik: isolated state needed for serialising warnings. Lots of EmbPrj` instances.
- Guillaume: highlighting for detecting useless imports working.
- Anton: Would like cubical primitives not to be in Primitive.agda unless `--cubical` is activated.
- Jonathan: started on `agda-pkg` library manager a la Python `pip`.
- Ulf: started refactoring free variable analysis to allow taking advantage of explicit substitutions.
Thursday 11 May
- Ulf: finished free variable refactoring and changed explicit substitution case to not apply the substitution
- Fredrik: Merging of highlighting in emacs now working.
- Jesper, Andreas, Youyou, John: formalisation of the spec in Agda.
Friday 12 May
- Wolfram: continued debugging.
- John: worked on agda-spec, specifically the formalisation in Agda
- Jesper: Added a specific constructor for absurd matches, thus recovering some proof irrelevance
- Andreas, Youyou, Fredrik: Failed to exploit the termination checker not knowing about parameters to break Agda. Also size assignments for ind-ind types.
- Anton: discussion about name choice for coinductive types: `force` vs `unfold` vs `inspect`.
Saturday 13 May
- Wolfram: not quite done yet.
- Andrea, Victor: cubical documentation.
- Fredrik: serialisation of warnings finished.
- Jesper: absurd pattern match on records containing empty fields.
- Jesper, Andreas, John: spec implementation.
- Ulf, Stephan, Anton: talked about deadlock freedom of user interfaces.
Monday 14 May
- Guillaume: used typeclass magic to refactor the deserialisation combinators. ~9% faster on the stdlib
- Victor: made sure code blocks are handled in the same way between the frontend and the latex backend
- Jonathan: worked on the bot tasked with accepting pull-requests on the package repository
Powered by PmWiki