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,
ProofGeneral-devel mailing list

Reply via email to