Coq Working Group 15 06 2022 Notes

Platform

MS: How inclusion process in the platform should work? It impacts:

• build time (today 2 hours)
• installer size (today approx 700M)

ALI: How bout installer which download more stuff?

• we need .vo files which are portable across systems or it gets nasty
• easy to do on windows, hard on Max, Enrico does not know how to do it on Snap

Numbers:

• Linux 800 users on snap
• Win/Mac 5K maybe

More about the download size:

• when it gets too large, it is too late (since we don't want to remove stuff)

MS: thinks there should be an editorial board, formally stated

• with people knowledgeable about all the parts (eg Prog Lang, Math...)

About the editorial board:

• should also take care of handling removals, so far never happened, but will
• statistics would help this work
• so far no rejection, but additions to the "extended part" of the platform
• maybe cover multiple networks (US / Europe)
• Names in the air: Yves Bertot and Andrew Appel with freedom to delegate or ask others, like Karl Palmskog

We like the idea of the board.

Technical issues are discussed separately, we hope dune will help on windows, we need some form of caching and possibly modular installers, but that won't happen in less than 2 years.

Platform and release timing

• Usually easy, but in 8.16 more problems (many break):
  • renaming primitive int library
  • ring changes?

Coq Users Survey

Questions raised during Theo's talk:

• Little feedback in Japan => probably because no translation in Japanese
• Isn't Rust a functional language? => Not according to the poll makers (or Enrico for what that matters)
• Private sector = Industry? yes
• Industrial application in the graph = Industrial application OR industrial research
• No result made public yet? Not yet, only about UI used
• How many result had X-survey? 750 ocaml, 800 elm, 1000 nixos, (466 coq)
• Repeat the survey to identify trends? A lot of work, but a good idea. We'd need a recurring WG. More surveys should be more light weight (same questions, python analysis tool is reusable).
• feedback about the tooling provided by inria:
  • they lost a few days of data once, seemed unreliable ... but the promised to not touch the system while the survey was running
  • good having the inria branding
  • limesurvey is a bit hard but powerful, Theo would reuse it
  • GPDR compliant
  • gitlab.inria.fr also GPDR compliant (for data post processing)