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 https://github.com/agda/agda2hs/issues/64)
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.

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: https://github.com/agda/agda-stdlib/pull/1518). 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.

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!)

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

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: https://github.com/agda/cubical/pull/566).
2020-06-10: Evan, Andrea: Adding sort for interval

Edit | History | Recent Changes (all) | Search

Page last modified on June 11, 2021, at 03:43 pm