RegressionTest
= Status quo = Systems currently running some sort of benchmarking, regression testing for Coq.
|| label || URL || access || tests what || comment || || lix-bench || http://www.lix.polytechnique.fr/coq/bench/ || lix || contribs (from git) || || || lix-newbench || http://www.lix.polytechnique.fr/coq/pylons || lix || - || 404 || || inria-ci || https://ci.inria.fr/coq/ || inria || coq (from git) || || || opam-bench || http://coq-bench.github.io/ || jobs on gihub, infrastructure ??? || opam packages || ||
= Problems = The problems we have w.r.t. regression testing, that apply to one or many
- 4 systems, overlap, which is the reference? Maybe 5, wasn't pyrolis intended to be the bench system?
- access: we need to be able to access the compilation logs
- access: we need to be able to fix the bench system, at least for trivial errors (like it picks the wrong branch, coq_makefile refresh)
- reproducibility: understand why it fails (access to logs, maybe more), replicate on more hardware
- too slow (wait 24h for a run)
- are the tests representative?
- only 1 big test (all contribs), all or nothing
- test a personal experiment without impacting the other developers
- single point of failure (only 1 gatekeeper)
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.