Coq Call 2020 09 02

• September 2th 2020, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• post-summer synchronization of our directions?

• Induction-induction status (Matthieu, 15min)

Notes

• Ongoing work:

  • PMP: cleaning of hints, Ltac2 bugfixes and features (contact with Derek Dreyer and Malecha) Weird behavior of hnf and discrimination nets behavior or meta/evar-closed terms. Maxime suggests commenting the hints code also when we don't understand some pieces of code.

    CUDW doodle to be sent.

  • Maxime and Gaëtan: fixing apply and shelf manipulation. 2 directions: continuing on unifall (close to closing 7825) "or" moving goals to the evar_map (solving the advance problem)

  • Hugo: working on Notations.

    • Deactivation of notations. PR #12324 RFC for syntax and features also
    • Plan to work on closing PRs:
      • about implicit argument naming
      • Arguments Needs for time to discuss these (CUDW should help here)

  • Emilio:

    • Finalizing the work on dune

    • SerAPI and Notations work

    • Later on: document model and scheduling

  • Matthieu:

    • Working on ind-ind types. Issue: representation of partial fixpoints during type-checking. If using option body this would naturally give rise to daimon-like values... https://github.com/coq/coq/pull/12464
  • Moving to github actions and applying for open-source Gold group-level support (submitted)