Coq Call 2022 11 16

• November 16nd 2022, 4pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics and Notes

• RM for 8.17 (Théo)

  Notes: Théo and Gaëtan will be the RMs, freeze soon.

  • We had a long, unplanned discussion about the CI and impact on release, some highlights:
    • Fiat-crypto failing for a long time, we can't afford to fix it
    • Maybe move to allow-failure, remove eventually?
    • If it is useful, test-cases should be made
    • How to test developments requiring large amounts of RAM?
    • To continue in next calls

• @CoqLang and #TwitterMigration (to Mastodon) (Théo)

  Notes:

  • Twitter under disarray, should Coq move to Mastodon? Many people has moved.
  • Situation far from stable tho (people go, then get back, etc...)
  • Emilio: we'd rather wait, follow what @inria institutional accounts plan to do.
  • Not a problem to make a Mastodon account to try (@CoqLang@types.pl) for example, if someone would like to do so.
  • Théo would like to see a directional bridge (Emilio wonders how well they work)

• Libobject refactoring:

  • https://github.com/coq/ceps/pull/65
  • https://github.com/coq/coq/pull/16484
  • https://github.com/coq/coq/pull/16261
  • Slides: https://docs.google.com/presentation/d/1-nM25BEeNdHmjO0gd0otu-KhP0Ge3fWT465UgLecOFE/edit?usp=sharing

  Notes:

  • Emilio presented the motivation and current design, many observations
  • PR can be seen as two different PRs (state, and meta-data)
  • Will clean up the current PR
  • API design not easy as due to lack of API there are few cases, Emilio did his best based on what he knows
  • We need to gather more use cases
  • Pierre-Marie makes a point about grouping of objects
  • Most recurrent FAQ is about the meta-data part.
    • Emilio thinks it makes things easy and the API uniform, would be interesting to see alternatives.
  • Another FAQ is why not to put the metadata in a Summary, Emilio sees as a principal downside code / summary duplication. If the data is in the libobject, why to add a pointless copy of it; allow direct access, and avoid having to deal with synchronizing the two databases.
  • Moreover, using a summary limits the API a lot, for example two different tables are needed for Notations and Declarations, etc...
  • In the end it is about a more uniform implementaton (for all objects) vs a more sealed setup.
  • In Emilio's use cases the choice favors current one strongly.

Rest of topics postponed to Dec 14th