coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] speed of Coq 8.8 vs 8.7, 32-bit vs 64-bit

From: Clément Pit-Claudel <cpitclaudel AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] speed of Coq 8.8 vs 8.7, 32-bit vs 64-bit
Date: Fri, 27 Apr 2018 11:08:35 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=cpitclaudel AT gmail.com; spf=Pass smtp.mailfrom=cpitclaudel AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f173.google.com
Ironport-phdr: 9a23:AYFTExZkUSratbe1SrGNY1r/LSx+4OfEezUN459isYplN5qZr8y9bnLW6fgltlLVR4KTs6sC17KN9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCazbL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjAk7m/XhMx+gqFVrh2vqBNwwZLbbo6OOfpifa7QZ88WSXZPU8tTUSFKH4Oyb5EID+oEJetVsY39oEELrRSgAwmsGPvgxCVJhn/qxKE3zeAhHhvb3AM9Ad0OtGnfodLpO6cKUOC10LXHzTHZYPNLxDjy9ozIfwsuofGJR71wcM7RxVMzGAPCi1WdsIroNC6W2OQVq2WX8fZsWOa1h2Mkqwx9uCajytoth4XTm44YyF7J+T1nzIs0OdG0VUt2bcOnHZZfsiyXOJZ6T8A+T2xtuSs3y6MJtJy+cSUJyJkqyB7SZvmJc4WG4x/uUOOcLDlmiHJrZb2ygha//Va6xeD+UMS/zUxEoTBfktbWs3AAzxzT5daDSvt65kqh3CyA1wHX6u1dOEA0ibbXJ4cvwrItlJcev17PHiDxmEXxg6+Wclsr9vK05OTgZ7Xqvp6cN4lqhQHiKqkihNCzDOAiPgUNX2WX4/qw2KDi8EHjXblHjPM7nrHcsJ/AJMQboqC5AxVS0oYm8xuwEy+m0NUEnXYbKFJKYg+HgJX3NFHKO/34AvK/jE6tkDdv3fzJIrrhApDVInjZjLjhZap961JbyAcr0d9f4ItUBqgdL/L3R0/+r8fVDgQ5Mgyx2+boEs9x1oIYWWKVA6+WKrnesVGS5rFnH+7Zb4gM/T35NvIN5vj0jHZ/l0VOU7Ou2M48bPG9E/J6FH2YfT/Hht4cHWoO9l41VO32g1mLTDJeY169Wqs94ncwD4fwXtSLfZyknLHUhHTzJZZRfG0TUgndQ0etTJ2NXrI3UAzXJ8ZgljIeUr34Et0u0BivsEnxzL81d7OIqB1djorq0Z1O38OWjQs7rGUmAMGU0mXLRGZxzDtRGm0GmZtnqEk48W+tlKh1h/sCS45W7vJNFx4mbdvSlrMhTd/1XQ3Fc5GCT1P0Gtg=

On 2018-04-26 14:57, Andrew Appel wrote:
> *Coq 8.8.0 is 14% faster than Coq 8.7.2 * (this measurement was made
> on Travis-CI, whatever hardware they are running).

14% looks great :) But are you sure it's not noise?

Looking at VST's build history on Travis-CI, the average build of the master
branch seems to last about 2 hours, with a standard deviation of 15 minutes
(close to 13%). Am I looking at the wrong data?

Clément.

[Coq-Club] speed of Coq 8.8 vs 8.7, 32-bit vs 64-bit, Andrew Appel, 04/26/2018
- RE: [Coq-Club] speed of Coq 8.8 vs 8.7, 32-bit vs 64-bit, Soegtrop, Michael, 04/27/2018
- Re: [Coq-Club] speed of Coq 8.8 vs 8.7, 32-bit vs 64-bit, Emilio Jesús Gallego Arias, 04/27/2018
- Re: [Coq-Club] speed of Coq 8.8 vs 8.7, 32-bit vs 64-bit, Xavier Leroy, 04/27/2018
- Re: [Coq-Club] speed of Coq 8.8 vs 8.7, 32-bit vs 64-bit, Ralf Jung, 04/27/2018
  - Message not available
    - Re: [Coq-Club] speed of Coq 8.8 vs 8.7, 32-bit vs 64-bit, Jim Fehrle, 04/27/2018
- Re: [Coq-Club] speed of Coq 8.8 vs 8.7, 32-bit vs 64-bit, Clément Pit-Claudel, 04/27/2018
- Re: [Coq-Club] speed of Coq 8.8 vs 8.7, 32-bit vs 64-bit, Clément Pit-Claudel, 04/28/2018
- Re: [Coq-Club] speed of Coq 8.8 vs 8.7, 32-bit vs 64-bit, Jim Fehrle, 04/28/2018
  - Re: [Coq-Club] speed of Coq 8.8 vs 8.7, 32-bit vs 64-bit, Clément Pit-Claudel, 04/28/2018
    - Re: [Coq-Club] speed of Coq 8.8 vs 8.7, 32-bit vs 64-bit, Adam Chlipala, 04/28/2018
- <Possible follow-up(s)>
- RE: [Coq-Club] speed of Coq 8.8 vs 8.7, 32-bit vs 64-bit, Soegtrop, Michael, 04/27/2018