Benchmark nocturne de Coq

Les benchmark ci-dessous tournent (depuis peu) sous Osiris. Pour avoir un historique des temps de compilation sur un plus long terme, vous pouvez vous référer aux benchmarks effectués par Khepri (cf cette page).

Résultats pour la branche développement

Résultats pour la branche v8.4

Résultats pour la branche v8.3

Résultats pour la branche 8.2 des contribs compilée avec la branche 8.3 de Coq

Résultats pour la branche v8.2

Performances

Les données affichées sont calculées ainsi. On commence par choisir un jour de référence, qui maximise le nombre de contributions qui compilent. Ensuite, pour chaque jour, on représente le rapport entre le total des temps CPU (resp. de la taille des .vo) des contributions compilées avec succès ce jour là et le total des temps CPU (resp. de la taille des .vo) de ces mêmes contributions au jour de référence.
graphe PostScript (Coq trunk)
graphe PostScript (Coq v8.3)
graphe PostScript (Coq v8.2)