Ralf Jung <j...@mpi-sws.org> writes: > (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.
Right. > 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. OK, sorry, then I misunderstood. I thought quick-and-vio2vo is what you were looking for. This option at least compiles some files to .vo while you can make some progress in your scripting buffer. What you want - compiling files unrelated to the current scripting buffer - is currently not available. I can only suggest the following workaround: Create a file that imports everything. After a change, do C-c C-b in that file. If quick compilation finds an error, that file is unlocked and you can go there and start fixing it (however, if you start scripting there, the keep going background compilation of the import everything will be aborted). If only vio2vo finds an error, the erroneous file is not unlocked and you need to select an ancestor looking mode that permits you to change the locked region. The assumption behind the current background compilation is that it is explicitly triggered by the user in a state where the file dependencies do not change. It is therefore fine to compute the dependencies only once at the beginning of the compilation. If the user triggers a second compilation after the first one has finished, the dependencies are computed again. If you have a continuously running background compilation process, then this process must be notified when some file changes on the disk because it then has to invalidate this file and everything depending on it. I can imagine that this would be useful for big projects, but it would be a lot of work. (Just imagine you switch git branches while the background compilation is in progress...) > 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 Do C-c C-b in a buffer that imports everything with quick-and-vio2vo, this will run vio2vo on all those files that don't have an up-to-date .vo. > * 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, Proof General runs vio2vo usually in the right order (but there are exceptions), but if B depends on A, vio2vo on B might start immediately after starting A and thus finish before A. It would be not too difficult to enforce that in case B depends on A, vio2vo on B only starts when A is finished. The dependency information is there, it is just not used for vio2vo. However, you might always run into the situation where B depends on A and where only the .vo file for A is missing. What do you want in this case? Run vio2vo on B again? > * 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. The make targets that coq_makefile generates are not very sophisticated, but I believe you would need quite a bit of makefile hacking to get the features that you want. Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
