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: Andrew Appel <appel AT CS.Princeton.EDU>
To: coq-club <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 07:47:23 -0400 (EDT)
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=appel AT CS.Princeton.EDU; spf=Pass smtp.mailfrom=appel AT cs.princeton.edu; spf=None smtp.helo=postmaster AT greenlight.cs.princeton.edu
Ironport-phdr: 9a23:Z520WBKVJJnkZssFS9mcpTZWNBhigK39O0sv0rFitYgRI/jxwZ3uMQTl6Ol3ixeRBMOHs6kC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwtFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhikHOTAn82/YiMJwgr9Urx29phxxxJLUbZqPO/ZiYqzQZ8kXSXZDU8tXSidPApm8b4wKD+cZIetYqZTyp0EQohqwGAKhGPvvyidWiX/ywKY31P4uERne3AM+G9IDq2rZosjvOKkIS+C1za/IwindYPNK3jf97pLEfB8vr/6CRL99d9fax0o3Fw7dk1mct4/oMymI2ugQrWSX9fdsWOyuhmI9qQx9vCCjytojh4XVnI4Z11PJ+TljzIorKtC1RlR3bcC4HJdMry2WKpV6T8A4T211pSo21KcKtYO1cSUI0pgqyAPTZvqaeIaS+B3jTvyeITJgiXJlZr2/gxGy/FCvyu3mSMa7zlBKri5EktnDtnANywbf5dScSvdn5kehwzeP1wbP5e5aPUA0kqzbJ4Q/zbEti5ofqUXDHinol0XqlKKaa1so9+uy5+j6f7nquIWQO5J6hwz/KKgjmNKzDfw9MgcUXmib/eq81Kfk/U38WLhFlOU2krHHv5DePskUurW5DxVN0oY56ha/CSup38oEnXkAKlJJYgyIgJX0O13WOvD3Ee+/g0iwkDds3/3JIrrhAozUInfflLfhYK1y5lVHyAszyNBf/4hbBqsAIPL1QE/xtcbXAgU3MwyukK7bD4B20ZpbUmaSCOfNO6TL9FSM++gHIu+WZYZTtiyreNY/4Pu7pHk1g1ICNYCxxZYTICSxBuxrJ22yWjzUmNYHGmoWuQx4YcDX3g7RGQVPbmq/CvpvrgowD5irWN+aF9KdxYeZ1SL+JaV4I2VPC1SCC3DtLtXWUOxKcDiTJMRsjjsCE7WtVt14jE38hErB07Nia9Hs1GgAr5u6hIpe3KvrjxA0/jFoCMLb/k2wHTktwzE4AgQu1aU6mnRTj1eO1a8i0q5XD9Fe4fdIXQcmc5XHifRgCtb5Vx7GeJGEREv0Gtg=

From: "Michael Soegtrop" <michael.soegtrop AT intel.com>

And I have a question: do you also make substantial use of parallelism in one coqc call (parallel proofs and/or parallel branches in one proof) or did you find that it is more optimal to run each coqc instance single threaded on a single core because the in file parallelism can have substantial peaks and lead to bad load balancing? Do you use different settings for batch and interactive mode?

I do not use parallelism within one coqc, mostly because parallelism has been unreliable on Windows in CoqIDE. (I am not sure whether the unreliability was only in CoqIDE, in which case it could be OK to use parallelism within coqc.) I use the same settings in batch and interactive mode. I have not done any real study or measurements of these tradeoffs.

Re: [Coq-Club] speed of Coq 8.8 vs 8.7, 32-bit vs 64-bit, Andrew Appel, 04/27/2018