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: > Hi, > > 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 > version. > > 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 > checking. > > Opinions? > > Bye, > > Hendrik > _______________________________________________ > ProofGeneral-devel mailing list > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel >
_______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
