The Coq mailing list

["Paul A. Steckler" <steck AT stecksoft.com>]

At the Working Group meeting on Friday, I suggested that it would be a
good idea to have benchmarks for individual tactics. My original
thought was to have timing benchmarks, and others suggested space
benchmarks would be useful as well. Such benchmarks could be used as
the basis of regression tests. The attendees seemed to agree that
benchmarks would be a good idea. I hope others agree.

It would be useful to have short scripts that exercise individual
tactics, so I'm soliciting those from the mailing list. During the
meeting, it was suggested to have goals of varying sizes, so that we
can examine time/space complexity. That means we'd have more than one
benchmark per tactic.

I don't yet know what the testing infrastructure will look like, but
it may involve the Jenkins tool we have. The tests could be run on
commits, or a nightly basis. If significant variation in time and
space is found, the author of the responsible commit would be notified
(in the case of improvement, the notification would be congratulatory
:-) ).

The first order of business is to gather the scripts needed for the
benchmarks. I'm soliciting from the readers of this list the scripts
to instantiate the tests. You can send them directly to me, or to the
list.

I'll create a page on Cocorico to track the progress of this project.

-- Paul