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
