- Anders: making library typecheck faster
- Andrea: exposing problem with incompatability between positivity checker and cubical
- Andreas: backported 3 packages to support Stackage
More control over reduction:
- Jesper & co: added new primitives `onlyReduceDefs` and `dontReduceDefs`, needs more testing
- Artem: testing out new primitives, working great so far
- Ulf: Started to think about what we can write in current Agda. Demo with `!` operator for antiquotation. Magic weakening for variables. Does not work yet on the LHS.
Integrating erasure with univalence:
- Andrea: currently all types are checked in erased context, but this is unsound with univalence. Found bug with erasure (independent of univalence), see #4986.
Instances in stdlib:
- Jesper: proposed list of possible instances that could be added
- John: Fixed inconsistent terminology in cubical library (section and retraction). After discussion with Anders, replaced sec and ret in HalfAdjoint.agda with linv and rinv to be consistent with Isomorphism.agda. Note that this may break code depending on isHAEquiv.
- James: trying to update manual, discovering new things about nix
Jesper: working on issue #4727
Ulf: using instance arguments to ensure absense of antiquotes outside of any quote.
Andrea: fixed two bugs with erasure
- Andreas: We had discussion on sized types, try to find solution for current inconsistencies by getting closer to theory from ICFP 2013 paper.
- Jesper: trying to find the cause of #4995 (see analysis on github)
Producing readable Haskell
- Ulf, James, Jesper: First prototype of Agda2Hs backend to compile Agda to readable Haskell code (see https://github.com/agda/agda2hs).
- Andreas, Manuel: Had another discussion, outcome unclear (?)
Inductive families in cubical
- Andrea: trying to make termination checker accept more definitions --without-K, fixing #4527.
- Ulf: Enforcing well-formedness of quasiquotes using InsideQuote` tactic argument, now works --safe.
Artem: Working on fixing the `reconstructParameters` function and exposing it to reflection API
- Ulf: made some PR for annotated reflected syntax (usable by Schmitty the Solver)
- Wen & Thomas: looking at CVC proof rules for Schmitty
- Andrea: working on indexed families
- Anders: merged a bunch of PRs, made draft of naming convention
- Ulf: generating haskellSrcExt instead of plain strings
- Ulf: added support for lambdas
- James: extending the backend with support for type classes
- Andrea: Still not clear if there's a design that guarantees consistency + subject reduction. There should be a paper to study combination of sized + dependent types. Maybe we can take inspiration from "Practical sized types for Coq" paper?
- Andreas: re-activated SizeUniv
- Ulf: Another demo of the same thing as yesterday
Improving of support for erasure:
- Nisse, Andrea: fixed issue with erased parameters of data/record types
- Nisse: identified problem with compiling functions with erased identifiers in their type
Clause telescopes in reflected syntax (code sprint from previous meeting):
- Jesper: implemented checking of types in the telescope when unquoting a clause
Interleaving constructors and clauses
- Guillaume: made a PR https://github.com/agda/agda/pull/5001, desugars to new-style mutual blocks