Coq Call 2020 02 05

• February 5th 2020, 4pm-5pm Paris Time
• How to join the call
• Add your topics below

Topics

• Gitlab's limits / plan
• remove fiat legacy from CI https://github.com/coq/coq/pull/11494 (we may converge before the call)
• Consolidate the standard library in its own directory https://github.com/coq/coq/pull/10003
• "Please release the documentation under a DFSG-compatible way" https://github.com/coq/coq/issues/8774
• Synthetizing our .plans and building a Coq Dev Team page (Matthieu)

Notes

Bedrock 2 broken on master

• Gitlab's limits / plan

  Changed open source policy, we need to apply for continued support.

• remove fiat legacy from CI https://github.com/coq/coq/pull/11494 (we may converge before the call)

  Emilio mentions we should have a better compatibility policy (maintained/active developments only?)

  Majority agrees about the cost of maintaining / investigating issues in f-c-l is too high w.r.t. the benefits (actually it's not even testing printing).

  Note for self: write a summary on the PR.

• Moving the .v files of plugins in stdlib/ https://github.com/coq/coq/pull/10003

  Current PR also moves the ML files, we would rather just keep them in plugins/. And move the plugins' .v files to theories/ Emilio will open a draft revision.

  Side question: can we move the plugins to -Q

• Coq Dev Team page and separately a page on current work topics We should review it and maintain it regularly (e.g. at Coq Working Groups)

  Théo will work on an update of the current draft Dev Team page.