Coq Call 2022 11 16 - coq/coq GitHub Wiki

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 (@[email protected]) 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:

    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