coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq 8.5 is out!

From: Maxime Dénès <mail AT maximedenes.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq 8.5 is out!
Date: Tue, 26 Jan 2016 17:11:02 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mail AT maximedenes.fr; spf=Pass smtp.mailfrom=mail AT maximedenes.fr; spf=None smtp.helo=postmaster AT 3.mo5.mail-out.ovh.net
Ironport-phdr: 9a23:Xvi4/xZv/Kcb2t6rbOE1ZpL/LSx+4OfEezUN459isYplN5qZpc+/bnLW6fgltlLVR4KTs6sC0LqJ9fi4EjJaqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7/0o8WYPV8ArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5Jd2wGkx9FSyRE6pHhFsP0uyr+nu90yCifMMH7S70vHzq4ufQ4ACT0gTsKYmZquFrcjdZ92fpW

Separate compilation for native_compute is disabled by default. So unless you actually use native_compute (or pass the -native-compiler flag to coqc), it should not have any performance impact.

Maxime.

On 01/26/16 14:29, Jacques-Henri Jourdan wrote:

Another guess : it seems like most of the overhead is spent on IO. Have
you tried to deactivate native compilation, that can lead to quite a lot
of IOs ?

Le 26/01/2016 13:41, Pierre-Marie Pédrot a écrit :

On 26/01/2016 09:19, Frédéric Blanqui wrote:

I tried Jacques-Henri's patch and, indeed, I get a total compilation
time similar to the one of Coq 8.4pl6:

That's still somehow bad, because as 8.5 already should be quicker than
8.4, the universe patch should therefore really speed things up. It
means we have a complexity regression somewhere, although it may be
quite diffuse.

PMP

Re: [Coq-Club] Coq 8.5 is out!, (continued)
- Re: [Coq-Club] Coq 8.5 is out!, Clément Pit--Claudel, 01/22/2016