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

Reply via email to