Coq Call 2020 09 16

• September 16th 2020, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Upcoming limit on the number of minutes of CI/CD on pipeline (cf. https://forum.gitlab.com/t/ci-cd-minutes-for-free-tier/40241). Any news on the open source program application?
• Bench status / roadmap ?
  • New strategy was adopted without discussion
  • Missing some convenience [in particular opening a PR for each bench]
• Opportunity to apply for a specific funding about the mathematical applications of Coq? (HH)

Notes

• CUDW.

  • Maybe not whole days
  • Need for fast interaction channels (zulip? dungeon interface?)

• Limit on CI/CD pipelines. I (Matthieu) am waiting for their answer after asking for 30 seats. Théo warns that getting enough minutes of CI might require the OSS program support in the future. Inria might provide additional computational power. Maxime is working on expanding the power for the benches (on pendulum). Shall we ask for more ressources like runners at Inria (Gaëtan might provide us numbers to argue for such support).

• Théo mentions that OS X signing is no longer enough in OS X 10.15 to open the app without a dialog. Notarization is required now https://developer.apple.com/documentation/xcode/notarizing_macos_software_before_distribution but we can't make Inria sign the developer program to have a developer id. Maybe we could use Michael's contacts to solve this (Maxime will ask him)

• Emilio reflects on moving from GitLab actions to a coqbot based framework?

  • Having two levels of testing / large and small tests.
  • The build system could benefit from caching and Emilio questions if the CI infrastructure is adapted to take advantage of this? A meeting between CI maintainers would help to establish a roadmap and anticipate needs we could communicate to Inria. Maxime, Emilio and Gaëtan.

• Hugo mentions a project on use of Coq for mathematicians at pi.r2 (with the idea to start an ANR project).

  • Type Theory as a foundation instead of ZFC
  • How to explain Lean's success and react to it in some way? General free-form discussion ensued