The Coq mailing list

[Hendrik Tews <hendrik AT askra.de>]

Hi,

I started some experiments with -quick. After using ``Proof
using'' everywhere, I see an overall speed improvement of 20%
with -quick and about 40% when I run on a ramdisk. For a few
files, -quick is much faster (up to 6 times) but for about 30% of
the files, -quick is actually slower.

I have a few questions:

- When coqc or coqtop process a Require command and there is both
  a vio and a vo file on the disk, which one does it load? Or,
  the other way round, if one of vio and vo is outdated and one
  is up-to-date, do I have to remove the outdated one before I
  process a Require?

- What happens if there is a schedule-vio2vo for module A
  running, while another coq process processes a Require that
  directly or recursively requires A. Is there a chance that this
  latter process will die because of a partial .vo file on disk?

- It is quite obvious, that separate schedule-vio-checking
  processes can be started regardless of the dependencies of the
  files. Is this also true for schedule-vio2vo? More precisely,
  if b.v requires a.v, can I start vio2vo for b before I start
  vio2vo for a?

- Again, it is obvious, that vio-checking also for just one
  module may profit from multiple cores. For vio2vo, it looks
  like it is processing each module one one core only.

- Is there a way to disable the ``Checking task'' lines?

- Is it right, that the aux file is written by a full batch
  compilation only? The aux file records the overall batch
  compilation time in the last line. But it does not contain the
  overall -quick compilation time, right? The latter would be
  useful for scheduling a quick recompilation.

Thanks,

Hendrik