Agda Implementors' Meeting XXXIV Wrapup meetings

Agda2Hs codesprint

  • 2020-06-08: Jesper, Ulf, James, Orestis: Brainstorm design for default implementations of type class functions (see
  • 2020-06-09: Ulf, Orestis, James, Jesper, Bohdan: Further work on default methods. New solution with separate record for each minimal complete definition.
  • 2020-06-10: Ulf, Orestis, James, Bohdan: Working on actually implementing default methods in the backend. Still a couple of minor flaws in translation of default bodies.
  • 2020-06-11: Ulf, Orestis, James, Bohdan, Jesper: Compiling class definitions with default implementations is now finished, working on compiling instances.

Standard library codesprint

  • 2020-06-08: Guillaume: adding bindings for getting current time and running external commands. Goal: implement golden test framework.
  • 2020-06-09: Guillaume: Added FilePaths and Directories, finished golden test framework (PR: Next step: compile the code and actually write some tests.
  • 2020-06-10: Guillaume: Tests are being run! Golden files are being created! Next step: run it on CI & get it to run tests in parallel.
  • 2020-06-10: Guillaume: Working on adding more test cases for modules in the standard library.

MusicTools codesprint

  • 2020-06-08: John, Orestis: Figuring out MuseScore format. Current version calls an Agda function for each individual note, each note is annotated by pitch class. (First user of --erased-cubical!)

GHC Backend

  • 2020-06-08: Nisse: working on making sure all generated names are valid Haskell names, work on --strict and --strict-data flags.

Agda extractor

  • 2020-06-09: Artem: experimenting with shallow embedding of stack language.

Cubical codesprint

  • 2020-06-09: Evan: Working on making Path types fibrant
  • 2020-06-09: Anders: Working on integers in cubical library, using non-higher integers as default implementation (PR:
  • 2020-06-10: Evan, Andrea: Adding sort for interval
Page last modified on June 11, 2021, at 03:43 pm
Powered by PmWiki