Pierre Courtieu <pierre.court...@gmail.com> writes:

> Do we support vio compilation?

No. I started to think about it and I would like to hear about
your opinion here.

I've only done a few experiments so far with -quick,
-schedule-vio2vo and -schedule-vio-checking. Therefore, if you
made different observations, please tell.

For files that don't use Proof using, vio compilation is
noticeably slower then vo compilation. Therefore, vio compilation
should be optional.

It will be quite easy to change background compilation to use
-quick, depending on some user option. How do people enable
-quick currently? Via putting -quick into _CoqProject?

The main question is whether and how Proof General should support
vio2vo and vio-checking. Ideally, I would like to have one vio2vo
instance, that only uses those cores that are not needed for vio
compilation and that dynamically reschedules another module as
soon as vio compilation finishes.

For instance, consider a project where B depends on A and all of
C, D, E and F depend on B. When I compile this on 4 cores, I
would like to do vio2vo on 3 cores while I am compiling B.
However, when B finishes, I want to be able to tell vio2vo to
immediately stop such that I can do coqc -quick for C, D, E and
F. As soon as the first of it finishes, vio2vo should commence on
1 core, but now schedule all remaining tasks from A, B and the
one that just finished.

As far as I understand this is not possible with the current Coq

Therefore I thought the background compilation should create 
one vio2vo or vio-checking task for each module when its vio
compilation finishes. As long as vio compilation is not finished,
these tasks are only started when the number of free cores
exceeds a certain threshold. When vio compilation finishes, Proof
General should continue with the current scripting buffer and use
all the remaining cores for vio2vo or vio-checking. This means
errors from vio2vo could show up when Proof General is processing
stuff far below the Require that triggered recompilation.

Finally, when vio2vo checking finishes there should be a
notification such that the user can decide to re-assert the
Require lines in order to get proper universe constraint



ProofGeneral-devel mailing list

Reply via email to