Coq Call 2020 01 29

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

Topics

• enable combining .vio and .vos files in CI regression proving "from scratch" (cf. discussion in https://github.com/coq/coq/issues/11471)
• coqdoc plans/status (cf. problems pointed out in https://github.com/coq/coq/pull/11394#pullrequestreview-342173454)
• dune switch schedule
• omega plans/status
• protect master branch even for admins (~ core developers)?

Notes

• vio / vos interaction Should be doable to check some files with vos and other with vio It is mostly about relaxing the option to load files with a given extension, so we have a mode where both are ok.

• coqdoc status Questions on the design of coqdoc: putting more info in glob files or reviving the coqdoc 2 effort which seems to go the way we want, reusing the parsing and globalization from Coq. Same as the beautifier ?

  https://github.com/thethirdman/coqdoc/

  TODO: Build a list of requirements for coqdoc on the wiki.

• dune switch schedule Dune retreat 3 to 10 of february: should be the time for merge of PRs (support for native compute and co, some feedback might be needed)

  Dune Coq Language doc by Emilio and Théo to come

  • Legacy mode (in contribs)
  • Separate installation of contribs/user packages

  We wait for the upcoming feature-complete dune, should be in time for 8.12 Might be difficult with Debian compatibility.

• omega deprecation? Is it for 8.12? Maybe some performance issues and the spec of lia might not match exactly (η question?) Still a few incompleteness problems and maybe inadequate test-suite especially for perf testing.

  PMP points the ML code is far from easy to port to univ poly and proper evar-map handling. We should write guidelines first on plugin writting and then distribute the port.

  Maxime is still on it but hard to predict when it will end.

• Note for self: unsafe_type_of in coercion.ml should be retyping's

• About master branch protection, everyone agrees, so Théo can go implement it. Note once need to push each merged PR separately.