Coq Call 2021 02 10 - coq/coq GitHub Wiki

Topics

  • native compute on the bench (Gaëtan)
  • requirements for a project to be in CI (Enrico)
  • merge CEP #52 and PR #13823.

Notes

  • native compute on the bench.

    Stack overflows when vm_compute is used to switch back from native_compute. What prevents benching native_compute?

    • Loss of precision in the bench, as we would test native + Coq compilation
    • But with separate compilation of vos to native code we could regain that. Pierre-Marie has some issues with (all) the build system(s) to make the separate compilation work (and plans for the future, e.g. caching. But that's not for today :). It seems we can have a single *-native package per opam package, covering multiple versions, to allow getting the natively compiled version.
    • 10% increase on overage, 20-30% on some devs, like CompCert if we enable native everywhere.

    4 new machines for benching being setup by Gaëtan. Green light to enable them and try native by default.

  • Requirements for a project to be in CI (Enrico)

    https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/CI.20and.20perennial

    Problems with vendoring and the amount of work it incurs on our maintainance. We can ask for more "polished" developments that avoids this issue. We advise towards using a "stable" coq-master branch in their repos and let the developers forward port our fixes/overlays to their actual master branches. We can try to discourage vendoring, but that happens sadly a lot in nature :)