Coq Call 2021 02 10
- February 10th, 2021, 4pm-5pm Paris Time
- https://rdv2.rendez-vous.renater.fr/coq-call
- native compute on the bench (Gaëtan)
- requirements for a project to be in CI (Enrico)
- merge CEP #52 and PR #13823.
-
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)
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 :)
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.