Hi, > I opend a PR for comments with a first version of -quick support, > see the quick branch on g...@github.com:hendriktews/PG.git. The > solution has advantages over using make because the quick options > accept an up-to-date .vo file for prerequisites (make insists on > producing .vio files for all files). Further, it does not suffer > from the consistency issue that make has: Proof General will > delete outdated .vo when compiling or relying on a .vio.
I may be a little late to the party here, but this is pretty cool! (And it's in master by now.) One question remains though: What exactly does "ensure vo" do? The CHANGES file says it "ensures a sound development", but that does not explain what is the difference to "no quick". My expectation was that it would do "-quick" for all files imported, so that I can edit the current file ASAP, and then in background do a full "make" to create the .vo files. But that doesn't seem to be what happens, if I look at what ProofGeneral does, I cannot notice any difference between "no quick" and "ensure vo". Btw, while we talk about doing things in background -- what I would find useful is if PG could compile "as many files as possible" to .vo in background. So say I change a file that's imported everywhere, then I switch to some other file and want to work interactively. Of course I have to wait until PG compiled everything up until here. It would be cool if, once that's done, PG could *go on* compiling the rest of the development (it could even use "nice" to ensure this doesn't steal many cycles from the more important interactive proof) so that, if I later switch to some third file, I don't have to wait again for the remaining dependencies to be compiled. What I will often do manually to achieve this is just start a "make -j2" in a console somewhere in background. Not sure if that makes any sense, I am just dumping some thoughts here. Kind regards, Ralf _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
