README.md

coq-performance-tests

A library of Coq source files testing for performance regressions on Coq

Contributing

Please add tests to this repository.

Each test should go in its own .v file in src/, and each .v file should be targeted to take around 1 minute, so that all tests get roughly equal weight.

PerformanceExperiments

The PerformanceExperiments folder contains a number of tests based on a test harness file which allow automatic generation of plots, as displayed below. The plots are updated on each run of GitHub Actions. To contribute to this folder, please add your test to Makefile.variables.kinds and follow the format of the existing tests. You can use make update-README to regenerate the tables for this README.

PerformanceExperiments plots

• Reify/BaselineStats

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• Reify/CanonicalStructures

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• Reify/Ltac2

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• Reify/LtacVariants

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• Reify/OCaml

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• Reify/Parametricity

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• Reify/QuoteFlat

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• Reify/TypeClasses

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• destruct_large_context

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• n_polymorphic_universes

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• pattern

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• repeat_setoid_rewrite_under_binders

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• repeat_setoid_rewrite_under_binders_noop

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• rewrite_lift_lets_map

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• rewrite_plus_0_tree

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• rewrite_repeated_app_autorewrite

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• rewrite_repeated_app_autorewrite_noop

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• rewrite_repeated_app_fast_rewrite

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• rewrite_repeated_app_fast_rewrite_ltac2

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• rewrite_repeated_app_fast_rewrite_no_abstract

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• rewrite_repeated_app_rewrite_strat

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• rewrite_repeated_app_ssrrewrite

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• rewrite_repeated_app_ssrrewrite_noop

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• rewrite_strat_under_binders

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• rewrite_under_lets_plus_0

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• sieve_of_eratosthenes

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• typeclass_reification_let_in_HOAS

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• typeclass_reification_let_in_PHOAS

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8

• zify_large_context

  dev	8.19	8.18	8.17	8.16	8.15	8.14	8.13	8.12	8.11	8.10	8.9	8.8