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