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

Reply via email to