Hi again, > 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?
To follow-up on this: I guess what I am asking for is some command in PG to say "now please compile everything", that command should be as smart about compilation as the compilation on import. It should behave just as if I would step over a file that "Require"s everything in _CoqProject, including all the magic to be able to jump to where the error was and everything. That'd be tremendously useful to make sure the entire project compiles, and to quickly fix issues that could come up. Ideally, this could work in background (after being started manually) so that I can keep working on one file while other files are compiled -- once the issue in the current file is fixed, it will already have found the next file that's broken, so I don't have to wait. For now, in case someone is interested, I implemented "incremental vio2vo" via Makefile hackery, see <https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/Makefile#L27> and <https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/awk.Makefile>. This essentially implements the "build all remaining files of the project" I asked for above, but outside PG. I will move this part of the discussion to coq-club since it's just about coq_makefile. Kind regards, Ralf _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
