Hi, all right, I'm back from reading the docs. Sorry again for not doing this earlier.
Most of my questions have been answered, including some I didn't even pose (like why I keep getting "A makes inconsistent assumptions over B", even though I don't even run the vio2vo-mode -- turns out that bug hits me because I did a plain "make -j4" in background on a console). However, I don't see any hint of the feature I am requesting. "Keep Going" *sounds* right, but it's not what I mean -- according to the docs (and from what I see it do), "Keep Going" is about compiling more of the dependencies of the current file even if other dependencies failed. What I am looking for is something that compiles more of the current *project* (i.e., things listed in the _CoqProject), even if everything that the current file depends on is already compiled. So say I have three files, A B C, and B C depend on A. I do a change in A, switch to B to fix things there that broke. What I am looking for is something that compiles C in background so that, if that file happens to still work, I don't need to wait later for it to finish compiling. This could save me enormous amounts of time if the breakage is somewhere in the leafs of the development, because all the intermediate files would be compiled while I am fixing some breakage, instead of being compiled only *after* I fixed the breakage and look for the next. Furthermore (and maybe not entirely related), when using one of the quick modes, is there a good way to incrementally check that the entire development compiles before pushing to git? Note that "compiles with vio2vo" is good enough; we have CI set up to catch the unlikely event of a universe inconsistency missed by vio2vo. I currently see two options: * Right before push, I do "make -j4". That will however recompile many files that PG already created with vio2vo, because the .vo files' timestamps do not match their dependency order when created by vio2vo. * Right before push, I do "make quick -j4 ; make vio2vo J=4". That will however always re-check all proofs because vio2vo is not incremental. Am I missing something here? Is it maybe possible to make vio2vo incremental? I feel like currently, the problem is just that the make target is too simplistic. A smarter "make vio2vo" could filter the list of .vo files for those that are older than their respective .v files, and only compile those -- is that correct? If yes, I may try to write such a make target. (Something even smarter would run "make quick" and "make vio2vo" in parallel, i.e., add .vio files to th schedule as they are created and already start producing the .vo files before all .vio files are done. I don't have a good idea though for how to implement that.) Kind regards, Ralf On 06.01.2017 17:39, Hendrik Tews wrote: > Ralf, > > your first email got through and thanks for you positive > feedback! > > I have the impression that you have not read any documentation > about the quick compilation feature. The CHANGES file is > unfortunately not the place to describe a complex feature > completely, but it contains a pointer: "See the option > `coq-compile-quick' or the subsection "11.3.3 Quick compilation > and .vio Files" in the Coq reference manual." May I ask that you > follow one of these links? I believe all your questions are > answered there and you will also find the documentation about the > feature that you are requesting! > > Best regards, > > Hendrik > _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
