Coq Call 2020 01 29 - coq/coq GitHub Wiki

Topics

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.