Note that .vio files are often 10x larger than .vo files. Bedrock, for
example, produces around 1-2 GB of .vo files, and around 20 GB of.vio
files. So .vio should definitely be optional.
I usually use the "quick" target of the Makefile generated by
coq_makefile. If I want just one file, I build the target foo .vio.
On Fri, Oct 28, 2016, 3:23 PM Hendrik Tews <hend...@askra.de> wrote:
> 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
ProofGeneral-devel mailing list