Coq Call 2023 12 04

• December 4th (Monday!), 4pm UTC+2 (Paris time zone offset)
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Reflection on CEP #73, useful for small inversion and for the parametricity plugins (HH, 5-10 min)
• what to do with https://github.com/coq/coq/pull/17920 (ssrbool: reenable overwriting-delimiting-key) (Gaëtan, 10min)
• #18349 Fix #18193 don't trigger file deprecation transitively (Pierre Roux, 5-10 min)
• take a decision on syntax for trigerring warnings other than deprecation #18248 (Pierre Roux, 15 min)

Roles

• Chairman: PMP
• Secretary: none (notes below from proux, from memory)

Notes

Attending: Yves Bertot, Emilio Jesus Gallego, Gaëtan Gilbert, Hugo Herbelin, Pierre-Marie Pédrot, Pierre Roux, Théo Zimmerman, ?

• Reflection on CEP #73, useful for small inversion and for the parametricity plugins (HH, 5-10 min)

  • natively adding an as alias for the term being filtered in match
  • agreement to separate the feature as an extension of matcht or of recursors and the implications it has on the guard
  • in either case, PMP asking for some kind of proof that it behaves well / doesn't break the guard condition
  • post-call comment: such proof has been provided by Gaëtan using a "generalization"/"convoy pattern" (i.e. a non-commutative beta-expansion across the match)

• what to do with https://github.com/coq/coq/pull/17920 (ssrbool: reenable overwriting-delimiting-key) (Gaëtan, 10min)

  • no way to do it perfectly, offered fix sounds reasonable enough, merging

• #18349 Fix #18193 don't trigger file deprecation transitively (Pierre Roux, 5-10 min)

  • want two warnings
    • transitive: current implem in master, warns as soon as a file is loaded, even indirectly
    • non transitive: changed offered by the PR, only warn on explicit Require of the file
  • EJG: beware not to flood the user with warning, will add pointers to litterature on the subject
  • proux: will try to readd transitive warning to the PR, silenced by default and documented, with a diferent name so that it can be trigerred independently

• take a decision on syntax for trigerring warnings other than deprecation #18248 (Pierre Roux, 15 min)

  • three differents things (all interesting)

    1. warninrgs that are not deprecation (EJG: in LSP, warning and deprecation are two different things)
    2. trigerring information messages that are not warning
    3. docstring (on demand)

    we are discussing a. here, need a syntax for the attribute, warning already taken, settled on warn(note="bla", categories="cata,catb,catc")