Hi, Now that the "make quick"-mode is all set up correctly and that I succeeded with my Makefile hackery, I got a very significant speed-up already for lots of my daily work. :) Not having to wait for all the proofs in the dependencies to be checked makes a huge difference, up to multiple minutes. Thanks a lot for all your work on PG!
>> 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. > > OK, lets call this the compile-everything thingy. What do you > want when > > - you start scripting in file A (for instance to fix a proof) > while compile-everything is still in progress? Have 2 > compilations in parallel or abort compile-everything? Aborting when the active file is changed sounds fine. I guess that's what vio2vo also does in background? > - while fixing B you realize you want to change the imports of A? > Restart compile-everything automatically after you saved A to > disk? See above. > - you decide to do a git pull to get the patch that fixed the > problem in some file from you colleague? Sounds like I'd be asking for trouble, just like if I would do git pull while the dependencies of a file are compiled by PG. If this could be safely cancelled, I think that's all I can hope for. > Note that in all these cases you might end up with inconsistent > vo files on disk if you just let compile-everything continue. Generally, I'd be fine with compile-everything being cancelled whenever it can't be safely continued -- even more so if there was a user action that triggered this abort. The motivation for this is to save time. Right now, when I change a file in our prelude (which is the folder containing a lot of basic definitions, essentially an extended standard library; everything depends in it), I then go to the console and do "make -j4". I see which is the first file to break (that may take 1 minute or two), navigate to that file in PG, and fix it. While I think about how to fix this, the CPU is idling. Once I fixed this file, I go to the console, do "make -j4" again, wait another minute or two for the next issue to come up, and repeat until the build works. Sometimes of course I have to go back to the prelude and change something there because I made a mistake, then the entire thing starts over. (Compiling everything from scratch takes ~6 minutes, but the sum of the waiting times here is larger because fewer things are compiled at once, so less parallelism is used.) My hope would be that the time it takes me to fix a file can be used better. Right now, all or all but one CPU core will be idle during that time; sometimes, I even manually do another "make -j4" in background to make sure I find the next mistake. I only today learned about "make -k" from your changes, that will be very useful indeed and may already be enough -- it will tell me which other files need fixing. This is a case of suddenly learning about a feature I didn't even know I longed for all the time. Of course it's not as convenient as having this in PG as I have to navigate to the file manually, but it should still help a lot. Next time this comes up, I'll see whether this feels sufficiently efficient. If I'm the only one wishing for such a feature, it's probably not worth the effort. I've just been dreaming a little here ;) Kind regards, Ralf _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
