Hi again, (I don't know if my previous mail got through, as I didn't get the mail myself via the list -- and I cannot access the list subscriber options to check whether I enabled getting my own mails, because the website is not working properly either. I informed the list owner about this.)
> 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". The tooltips of the menu actually document that feature better than the CHANGES file does: "ensure vo" will refuse to import .vio files, but otherwise behaves like "no quick". The reason I asked for "compile vo files in background" is that I want to check that everything compiles before pushing things to the git repository. This check should re-use the work already done by PG because otherwise things just take too long. I could do "make quick ; make vio2vo", but the problem is that vio2vo is not incremental, this will always re-check everything. Just saying "make" seems to ignore the .vo files created by vio2vo (or rather, it gets confused by the fact that the .vo files' timestamps do not correspond to their dependency structure any more, so it will re-compile files that are perfectly up-to-date). That's why I was looking for a mode that does "-quick" to quickly get the interactive mode started, but then creates .vo files the "normal" way so that one can incrementally compile the remaining .vo files before pushing. Kind regards, Ralf _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
