Minutes September 09 2020 - math-comp/math-comp GitHub Wiki

  • About #501: intro pattern /[! inE]

    • syntax?
      • Reynald finds /[rw !inE] and /[rw inE] less cryptic, Enrico concurs
      • Cyril:
        • the best would be /[inE] and /[mxE] but it is not possible to implement it, because we need "late binding" (Enrico can look if it is implementable, not easy)
    • drop Coq <= 8.10
      • Enrico, Reynald, Cyril are OK
      • Reynald: we can then also fix
    • final decision postponed or we make a poll on the mailing list/zulip

  • About MCZIFY:

    • CI: one can use the the .travis from analysis, or use the coq-community template that now supports the docker image with MC in it
    • looks like the coq-community stuff is great

  • About ambiguous path in Analysis:

    • 3 paths to follow in order of priority/feasibility/risk:
      1. #546 fixes it via surgery
        • Kazuhiko: not good idea to merge it as is, since the PR also removes Pack notation for fieldExt. class_of of fieldExt is reimplemented but the structure had 2 Pack notations (one to change the base field on the fly). It can be re-added but requires more work.
      2. making classes primitive records (with eta conversion) would fix it as well (also helps in order)
      3. "flat packed classes" don't exhibit the problem (this requires Hierarchy Builder, since writing flat classes by hand is daunting)

  • The golden rule about spaces in rewrite foo// over rewrite foo //:

    • syntactically optional spaces can be removed only if they prevent a line break and if breaking the line would result in a less readable script.
    • rule of thumb: Put the spaces, if you get to 80 chars think about this possibility.