Agda Implementors' Meeting XXV progress summary

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