coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Emilio Jesús Gallego Arias <e AT x80.org>
- To: Christian Doczkal <christian.doczkal AT ens-lyon.fr>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Parallel Proof Checking
- Date: Mon, 07 May 2018 12:44:22 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
- Ironport-phdr: 9a23:njeCVhTidjmdv7rxTRb9mdM6Kdpsv+yvbD5Q0YIujvd0So/mwa69YheN2/xhgRfzUJnB7Loc0qyK6/umATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfb1/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4rx1QxH0ligIKz858HnWisNuiqJbvAmhrAF7z4LNfY2ZKOZycqbbcNgHR2ROQ9xRWjRBDI2icoUPCOQBM+haoIf+qVQBogexCBKwBO/z0DJEmmP60Lc43uknDArI3BYgH9ULsHnMo9v1MaYSUeS0zKnP1TrNa+1Z2Szn8IjTah8voOuDXbZ0ccXPxkkvEBvKg0mKqYzkJTyVzfkGvm+F4Od7WuOiiHIrpxt2oji1ycchk4/EjZ8WxFDc7Sh13YU4KN6iREJlf9KpEYFcuzyYOodrWM8uXm9ltDgixrAEu5O3ZjUGxZQkyhLFdvCKcJSE7gj9WOuePTt1gm9udqiliBao60egz/XxVsmq31ZOqSpIitbNu3MR2xDJ7ciHUPR98l+g2TaJyQ/T9vlJLV03mKfYMZIt3KA8m5sJvUjeHCL6hV/6gLKYe0k64uSo7v7oYrTipp+SLY90jQT+P7wwlcGkDuU1MRQCU3Kc+eSm273v5Vf5T6lSjv0qjqnZt4jXKtgcpq6gGgNazoIj6wukADq9y9QZnXwHLEpfdx6djojpPUvOIPHiAvuljVSsimQj+/eTFb37A47RL3HF2JvmdqR+4koUnAEz19FE+5NdDPcNJ/nhWUb1nNHeFVo9Iguyhej9XoZTzIQbDE+KA6uYN5TwvEQa/dUAKu2IaYASjx/nKvE+r6rjpW9pwRkaZ6b/jshfU2yxAvkzexbRWnHrmNpUVD5S5lNvHtyvs0WLVHtoX1j3Wqs94j8hD4f3X5eTHsaqmrPThX7nTK0TXXhPDxW3KVmtb5+NCqUcOHrUJdVuwGRdCOqRDrQ53BTrjzfUjrpqKu2FqD1I7dTkztcnvuA=
- Organization: X80 Heavy Industries
Christian Doczkal
<christian.doczkal AT ens-lyon.fr>
writes:
> From my experiments, it appears that running "make -j8 quick" and then
> "make -j8 vio2vo J=8" (coq-8.8 on a 4 cores / 8 threads CPU) does
> generate all .vo files in parallel, but there appears to be no
> parallelism regarding the proofs within the files. That is, in a
> development with many .v files, but three large files each taking
> about 25% of the total compilation time, I quickly get to the point
> where there are only 3 processes running.
Maybe you are using sections? If so, then you'll have to add `Proof
using` annotations.
E.
- [Coq-Club] Parallel Proof Checking, Christian Doczkal, 04/28/2018
- Re: [Coq-Club] Parallel Proof Checking, Emilio Jesús Gallego Arias, 05/07/2018
Archive powered by MHonArc 2.6.18.