Coq Call 2020 09 02 - coq/coq GitHub Wiki

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)