- 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.
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: 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: Artem: experimenting with shallow embedding of stack language.
- 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
Powered by PmWiki