Coq-HoTT icon indicating copy to clipboard operation
Coq-HoTT copied to clipboard

Get travis to run timing scripts

Open Alizter opened this issue 4 years ago • 5 comments

Can we create a travis job that can run the timing scripts? When we create a PR one of the things we would like to do is to see how it compares with master. Currently we have to run the script manually, which can change deepening whose machine it is running on. Getting travis to do this would standardize the timing changes somewhat and make it less work for us.

I would suggest comparing the timing of master with the timing of the PR merged. We should be able to pop into the travis job and quickly see the table generated.

Alizter avatar Oct 27 '19 15:10 Alizter

I can have Travis display the timing table for the current PR if it doesn't already, but the Travis machines aren't reliable enough, in my experience, to see accuracy of more than +- 10% or 20%. And although the absolute timing changes depending on the machine, I expect relative timing to be roughly the same across machines.

JasonGross avatar Oct 27 '19 19:10 JasonGross

@JasonGross This has been done now right?

Alizter avatar Feb 21 '20 15:02 Alizter

Pull requests do not compare timing against master. We could have them do this though.

JasonGross avatar Feb 21 '20 16:02 JasonGross

However, they do display the timing tables without any comparison

JasonGross avatar Feb 21 '20 16:02 JasonGross

@JasonGross It would be nice if we can have a job for PRs that compare their build against master. What would need to be done?

Alizter avatar Feb 21 '20 16:02 Alizter